rw [sub_eq_add_neg, add_pow_prime_eq hpri, (hpri.odd_of_ne_two hp).neg_pow, one_pow,
  mul_pow, ← C.map_pow, add_comm, add_comm (_ * _), ← add_assoc, ← add_assoc,
  add_right_neg, zero_add]
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X - 1) ^ p + 1
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ C (a ^ p) * X ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)