have := h2 1 one_lt_two one_pos
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
this : x ^ 1 ≠ 1
⊢ x ≠ 1