R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
dg : natDegree (-q) < n
⊢ coeff (p - q) n = coeff p n
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
dg : natDegree q < n
⊢ coeff (p - q) n = coeff p n
rw [← natDegree_neg] at dg
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
dg : natDegree (-q) < n
⊢ coeff (p - q) n = coeff p n
rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]