R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (Finset.sum (Finset.range (Nat.succ (natDegree p + natTrailingDegree p))) fun k =>
      coeff p (k, natDegree p + natTrailingDegree p - k).fst *
        coeff (mirror p) (k, natDegree p + natTrailingDegree p - k).snd) =
    sum p fun n x => x ^ 2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ coeff (p * mirror p) (natDegree p + natTrailingDegree p) = sum p fun n x => x ^ 2
rw [coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
no goals
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (Nat.succ (natDegree p + natTrailingDegree p))
⊢ coeff p (n, natDegree p + natTrailingDegree p - n).fst *
      coeff (mirror p) (n, natDegree p + natTrailingDegree p - n).snd =
    coeff p n ^ 2
rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]