Conj Aut Xpow eq neg

theorem conjAut_Xpow_eq_neg (α : ℕ) {e : ℕ} (he0 : 0 < e) (heα : e < 2 ^ α) :    conjAut α (Xpow (powTwoCyclotomic (R := R) α) e)      = - Xpow (powTwoCyclotomic (R := R) α) (2 ^ α - e) := by  have hc : conjExp α + 1 = 2 ^ (α + 1) := Nat.sub_add_cancel Nat.one_le_two_pow  have h2 : (2 : ℕ) ^ (α + 1) = 2 * 2 ^ α := by rw [pow_succ]; ring  rw [conjAut_Xpow]  have hper : (e * conjExp α) % 2 ^ (α + 1) = (2 ^ α + (2 ^ α - e)) % 2 ^ (α + 1) := by    have harith : 2 ^ α + (2 ^ α - e) = 2 ^ (α + 1) - e := by omega    rw [harith]    have hmod : e * conjExp α ≡ 2 ^ (α + 1) - e [MOD 2 ^ (α + 1)] := by      apply Nat.ModEq.add_right_cancel' e      rw [Nat.sub_add_cancel (by omega : e ≤ 2 ^ (α + 1))]      have hsum : e * conjExp α + e = e * 2 ^ (α + 1) := by rw [← hc]; ring      rw [hsum]      exact (Nat.modEq_zero_iff_dvd.mpr ⟨e, by ring⟩).trans        (Nat.modEq_zero_iff_dvd.mpr (dvd_refl _)).symm    exact hmod  rw [Xpow_congr_mod α hper, Xpow_add, Xpow_natDegree, neg_one_mul]