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]
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
⊢ sign (transpos { val := i, isLt := hi } { val := Nat.succ j, isLt := hj }) = true
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
this : transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transposAdj j hj * s * inv (transposAdj j hj)
⊢ sign (transpos { val := i, isLt := hi } { val := Nat.succ j, isLt := hj }) = true