rcases Nat.lt_trichotomy i.1 j.1 with hlt | heq | hgt
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
⊢ sign (transpos i j) = true
case inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hlt : ↑i < ↑j
⊢ sign (transpos i j) = true

case inr.inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ sign (transpos i j) = true

case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos i j) = true