R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p < n
⊢ coeff (q + p) n = coeff q n
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p < n
⊢ coeff (p + q) n = coeff q n
rw [add_comm]
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p < n
⊢ coeff (q + p) n = coeff q n
exact coeff_add_eq_left_of_lt pn