case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : p ≠ 0
hpq : degree p < degree q
hq : q = 0
⊢ natDegree p < natDegree q

case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : p ≠ 0
hpq : 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 p q : R[X]
hp : p ≠ 0
hpq : degree p < degree q
⊢ natDegree p < natDegree q
by_cases hq : q = 0
no goals
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : p ≠ 0
hpq : degree p < degree q
hq : ¬q = 0
⊢ natDegree p < natDegree q
rwa [degree_eq_natDegree hp, degree_eq_natDegree hq,
  Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe] at hpq
no goals
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : p ≠ 0
hpq : degree p < degree q
hq : q = 0
⊢ natDegree p < natDegree q
exact (not_lt_bot <| hq ▸ hpq).elim