R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ (if natDegree (↑C c) = 0 then 0 else coeff (↑C c) (natDegree (↑C c) - 1)) = 0
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ nextCoeff (↑C c) = 0
rw [nextCoeff]
no goals
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ (if natDegree (↑C c) = 0 then 0 else coeff (↑C c) (natDegree (↑C c) - 1)) = 0
simp