R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝² : Nontrivial R
inst✝¹ : Semiring R
inst✝ : Semiring S
c : S
✝ : Nontrivial S
⊢ nextCoeff (X + ↑C c) = c
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝² : Nontrivial R
inst✝¹ : Semiring R
inst✝ : Semiring S
c : S
⊢ nextCoeff (X + ↑C c) = c
nontriviality S
no goals
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝² : Nontrivial R
inst✝¹ : Semiring R
inst✝ : Semiring S
c : S
✝ : Nontrivial S
⊢ nextCoeff (X + ↑C c) = c
simp [nextCoeff_of_pos_natDegree]