R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.529420
h : degree q < degree p
⊢ coeff p (natDegree p) ≠ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.529420
h : degree q < degree p
⊢ coeff (p + q) (natDegree p) ≠ 0
rw [coeff_add, coeff_natDegree_eq_zero_of_degree_lt h, add_zero]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.529420
h : degree q < degree p
⊢ coeff p (natDegree p) ≠ 0
exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)