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