case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p = 0
⊢ natTrailingDegree p ≤ natDegree p

case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : ¬p = 0
⊢ natTrailingDegree p ≤ natDegree p
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ natTrailingDegree p ≤ natDegree p
by_cases hp : p = 0
no goals
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p = 0
⊢ natTrailingDegree p ≤ natDegree p
rw [hp, natDegree_zero, natTrailingDegree_zero]
no goals
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : ¬p = 0
⊢ natTrailingDegree p ≤ natDegree p
exact le_natDegree_of_ne_zero (mt trailingCoeff_eq_zero.mp hp)