no goals
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
n : ℕ
H : degree p ≤ ↑n
H1 : degree p < ↑(n + 1)
⊢ coeff (X ^ (n + 1) + p) (n + 1) = 1
rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H1, add_zero]