R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469198
hp : p ≠ 0
h : degree p < degree q
⊢ natDegree p < natDegree q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469198
hp : p ≠ 0
⊢ degree p < degree q → natDegree p < natDegree q
intro h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469198
hp : p ≠ 0
h : degree p < degree q
hq : q ≠ 0
⊢ natDegree p < natDegree q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469198
hp : p ≠ 0
h : degree p < degree q
⊢ natDegree p < natDegree q
have hq : q ≠ 0 := ne_zero_of_degree_gt h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469198
hp : p ≠ 0
h : ↑(natDegree p) < ↑(natDegree q)
hq : q ≠ 0
⊢ natDegree p < natDegree q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469198
hp : p ≠ 0
h : degree p < degree q
hq : q ≠ 0
⊢ natDegree p < natDegree q
rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_withBot, Nat.cast_withBot] at h
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469198
hp : p ≠ 0
h : ↑(natDegree p) < ↑(natDegree q)
hq : q ≠ 0
⊢ natDegree p < natDegree q
exact_mod_cast h