List.length_insertNth

theorem List.length_insertNth : ∀ {α : Type u} {a : α} (n : ℕ) (as : List α), n ≤ as.length → (List.insertNth n a as).length = as.length + 1 := by sorry

The theorem `List.length_insertNth` states that for any type `α`, given an element `a` of type `α`, a natural number `n`, and a list `as` of type `α`, if `n` is less than or equal to the length of the list `as`, then the length of the list obtained by inserting `a` at the `n`-th position in `as` using the function `List.insertNth` is equal to the length of the original list plus one. This highlights that the operation of inserting an element at a certain position in a list increases the length of the list by one.

More concisely: For any type `α` and list `as : α-- list`, if `n ≤ length as`, then `length (List.insertNth α a n as) = length as + 1`.