cases Nat.lt_or_ge i.1 j.1 with
| inl hlt => exact ⟨transposInversion i j hlt⟩
| inr hge =>
  rewrite [transpos_comm]
  refine ⟨transposInversion j i ?_⟩
  exact Nat.lt_of_le_of_ne hge fun hcntr =>
    h <| Fin.eq_of_val_eq hcntr.symm
n : Nat
i j : Fin n
h : i ≠ j
⊢ Nonempty (Inversion (transpos i j))
no goals