English
A head-elimination induction along a concatenated list yields the value at the head of the concatenation.
Русский
Индукция по голове на конкатенацию списка даёт значение головы конкатенации.
LaTeX
$$$IsChain\\, R\\, (l \\ ++ [b]) \\Rightarrow Eq ((l ++ [b]).head ...) a \\Rightarrow (\\forall i, p i) \\Rightarrow p a$$$
Lean4
theorem cons_of_le [LinearOrder α] {a : α} {as m : List α} (ha : List.IsChain (· > ·) (a :: as))
(hm : List.IsChain (· > ·) m) (hmas : m ≤ as) : List.IsChain (· > ·) (a :: m) := by
cases m with
| nil => grind
| cons b bs =>
apply hm.cons_cons
cases as with
| nil =>
simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas
exact (List.not_lt_nil _ hmas).elim
| cons a' as =>
rw [List.isChain_cons_cons] at ha
refine lt_of_le_of_lt ?_ ha.1
rw [le_iff_lt_or_eq] at hmas
rcases hmas with hmas | hmas
· by_contra! hh
rw [← not_le] at hmas
apply hmas
apply le_of_lt
exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel hh)
· simp_all only [List.cons.injEq, le_refl]
