rcases j with ⟨j,hj⟩
case mk
m n : Nat
j : Fin n
i : Nat
hi : i < n
h : { val := i, isLt := hi } < j
⊢ sign (transpos { val := i, isLt := hi } j) = true
case mk.mk
m n i : Nat
hi : i < n
j : Nat
hj : j < n
h : { val := i, isLt := hi } < { val := j, isLt := hj }
⊢ sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true