rewrite [transpos_comm]
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ Nonempty (Inversion (transpos i j))
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ Nonempty (Inversion (transpos j i))