no goals
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n = (X n - ∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n)
rw [xInTermsOfW, ← Fin.sum_univ_eq_sum_range]