case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : f = 0
⊢ natTrailingDegree (reverse f) = 0

case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree (reverse f) = 0
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natTrailingDegree (reverse f) = 0
by_cases hf : f = 0
no goals
case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : f = 0
⊢ natTrailingDegree (reverse f) = 0
rw [hf, reverse_zero, natTrailingDegree_zero]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree (reverse f) ≤ 0
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree (reverse f) = 0
rw [← le_zero_iff]
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff (reverse f) 0 ≠ 0
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree (reverse f) ≤ 0
apply natTrailingDegree_le_of_ne_zero
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ leadingCoeff f ≠ 0
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff (reverse f) 0 ≠ 0
rw [coeff_zero_reverse]
no goals
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ leadingCoeff f ≠ 0
exact mt leadingCoeff_eq_zero.mp hf