obtain rfl : m = 1 := by linarith
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
m : ℕ
hm1 : m < 2
hm2 : 0 < m
⊢ x ^ m ≠ 1
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
hm1 : 1 < 2
hm2 : 0 < 1
⊢ x ^ 1 ≠ 1