R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.651623
h : degree p < degree q
this : coeff p (natDegree q) = 0
⊢ leadingCoeff (p + q) = leadingCoeff q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.651623
h : degree p < degree q
⊢ leadingCoeff (p + q) = leadingCoeff q
have : coeff p (natDegree q) = 0 := coeff_natDegree_eq_zero_of_degree_lt h
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.651623
h : degree p < degree q
this : coeff p (natDegree q) = 0
⊢ leadingCoeff (p + q) = leadingCoeff q
simp only [leadingCoeff, natDegree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h), this,
  coeff_add, zero_add]