R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ nextCoeff (p * q) = nextCoeff p + nextCoeff q
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
⊢ nextCoeff (p * q) = nextCoeff p + nextCoeff q
nontriviality
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ coeff (reverse (p * q)) 1 = coeff (reverse p) 1 + coeff (reverse q) 1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ nextCoeff (p * q) = nextCoeff p + nextCoeff q
simp only [← coeff_one_reverse]
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ coeff (reverse (p * q)) 1 = coeff (reverse p) 1 + coeff (reverse q) 1
rw [reverse_mul] <;>
  simp [coeff_mul, Nat.antidiagonal, hp.leadingCoeff, hq.leadingCoeff, add_comm,
    show Nat.succ 0 = 1 from rfl]