induction h with
| refl => exact sign_transposAdj i hj
| @step j hij IH =>
  let s := transpos ⟨i,hi⟩ ⟨j, Nat.lt_of_succ_lt hj⟩
  have : transpos ⟨i,hi⟩ ⟨j+1,hj⟩ = transposAdj j hj * s * (transposAdj j hj).inv := by
    simp only [transpos_conj]
    rw [get_transposAdj_of_lt hij, get_transposAdj_self]
  rewrite [this]; simp only [sign_conj]
  exact IH _
case mk.mk
m n i : Nat
hi : i < n
j : Nat
hj : j < n
h : i < j
⊢ sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
no goals