case hg
n : ℕ
i : ZMod n
⊢ sr i ^ 2 = 1

case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1
n : ℕ
i : ZMod n
⊢ orderOf (sr i) = 2
apply orderOf_eq_prime
no goals
case hg
n : ℕ
i : ZMod n
⊢ sr i ^ 2 = 1
rw [sq, sr_mul_self]
case hg1

⊢ ∀ {n : ℕ} (i : ZMod n), sr i ≠ 1
case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1
revert n
no goals
case hg1

⊢ ∀ {n : ℕ} (i : ZMod n), sr i ≠ 1
simp_rw [one_def, ne_eq, forall_const]