suffices ∀ (i j : Fin n), i < j → (transpos i j).sign = true by
  rcases Nat.lt_trichotomy i.1 j.1 with hlt | heq | hgt
  . exact this i j hlt
  . exfalso; exact h <| Fin.eq_of_val_eq heq
  . rewrite [transpos_comm]; exact this j i hgt
m n : Nat
i j : Fin n
h : i ≠ j
⊢ sign (transpos i j) = true
m n : Nat
i j : Fin n
h : i ≠ j
⊢ ∀ (i j : Fin n), i < j → sign (transpos i j) = true