case inl
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : natDegree (eraseLead f) < natDegree f
⊢ natDegree (eraseLead f) ≤ natDegree f - 1

case inr
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : eraseLead f = 0
⊢ natDegree (eraseLead f) ≤ natDegree f - 1
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natDegree (eraseLead f) ≤ natDegree f - 1
rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)
no goals
case inl
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : natDegree (eraseLead f) < natDegree f
⊢ natDegree (eraseLead f) ≤ natDegree f - 1
exact Nat.le_pred_of_lt h
no goals
case inr
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : eraseLead f = 0
⊢ natDegree (eraseLead f) ≤ natDegree f - 1
simp only [h, natDegree_zero, zero_le]