no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (↑(succAbove i) k)
⊢ insertNth i x p j = Eq.recOn (_ : ↑(succAbove i) (pred j (_ : j ≠ 0)) = j) (p (pred j (_ : j ≠ 0)))
rw [insertNth, succAboveCases, dif_neg h.ne', dif_neg h.not_lt]