rewrite [transpos_comm]
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
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 j i) = true