R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ card (Finset.erase (support f) (natDegree f)) < card (support f)
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ card (support (eraseLead f)) < card (support f)
rw [eraseLead_support]
no goals
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ card (Finset.erase (support f) (natDegree f)) < card (support f)
exact card_lt_card (erase_ssubset <| natDegree_mem_support_of_nonzero h)