n : ℕ
i : ZMod (2 * n)
⊢ a (↑n + ↑n) = 1
n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 4 = 1
rw [pow_succ, pow_succ, sq, xa_mul_xa, xa_mul_a, xa_mul_xa, add_sub_cancel, add_sub_assoc,
  add_sub_cancel']
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(n + n) = 1
n : ℕ
i : ZMod (2 * n)
⊢ a (↑n + ↑n) = 1
norm_cast
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(2 * n) = 1
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(n + n) = 1
rw [← two_mul]
no goals
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(2 * n) = 1
simp [one_def]