no goals
ι : Type ?u.126707
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : n ≤ length l
⊢ n < length (insertNth n x l)
rwa [length_insertNth _ _ hn, Nat.lt_succ_iff]