∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] (n : ℕ) (x y : WittVector p k),
  (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) =
    WittVector.peval (WittVector.polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i]