Theorem: Permutation.get_transAdj_succ (Fifteen/Data/Permutation/Basic.lean)

State before:
n i : Nat
h : i + 1 < n
⊢ (transposAdj i h)[i + 1] = { val := i, isLt := (_ : i < n) }
Tactic:
simp only [transposAdj, get_transpos, if_pos]
State after:
no goals