English
If L is (m+1)-admissible and a ≤ m and a < L[0], then the list a :: L is m-admissible.
Русский
Если L является (m+1)-допустимым и a ≤ m, а также a < L[0], то список a :: L является m-допустимым.
LaTeX
$$$\\\\text{If } L \\,\\text{is } (m+1)\\text{-admissible and } a \\le m \\text{ and } a < L_0, \\\\text{then } (a :: L) \\\\text{is } m\\text{-admissible.}$$$
Lean4
/-- If `L` is a `(m + 1)`-admissible list, and `a` is natural number such that a ≤ m and a < L[0],
then `a::L` is `m`-admissible -/
theorem cons (L : List ℕ) (hL : IsAdmissible (m + 1) L) (a : ℕ) (ha : a ≤ m) (ha' : (_ : 0 < L.length) → a < L[0]) :
IsAdmissible m (a :: L) := by
cases L with
| nil => constructor <;> simp [ha]
| cons head
tail =>
simp only [List.length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.lt_one_iff, pos_of_gt, or_true,
List.getElem_cons_zero, forall_const] at ha'
simp only [IsAdmissible, List.sorted_cons, List.mem_cons, forall_eq_or_imp]
constructor <;> repeat constructor
· exact ha'
· rw [← List.forall_getElem]
intro i hi
exact ha'.trans <| (List.sorted_cons.mp hL.sorted).left tail[i] <| List.getElem_mem hi
· exact List.sorted_cons.mp hL.sorted
· rintro ⟨_ | _⟩ hi
· simp [ha]
· haveI := hL.le _ <| Nat.lt_of_succ_lt_succ hi
rw [List.getElem_cons_succ]
cutsat
