rewrite [dif_pos h]
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = if h : i < n then Fin.castAdd m x[i] else { val := i, isLt := hi }
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = Fin.castAdd m x[i]