no goals
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n * ↑C (↑p ^ n) = X n - ∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
rw [xInTermsOfW_eq, mul_assoc, ← C_mul, ← mul_pow, invOf_mul_self,
  one_pow, C_1, mul_one]