English
The list Ico n m forms a chain where each element is the successor of the previous one.
Русский
Список Ico n m образует цепочку: каждый следующий элемент является преемником предыдущего.
LaTeX
$$$\operatorname{IsChain}(\lambda a,b.\ b = a+1)(\operatorname{Ico}(n,m))$$$
Lean4
theorem isChain_succ (n m : ℕ) : IsChain (fun a b => b = succ a) (Ico n m) :=
by
by_cases h : n < m
· rw [eq_cons h]
unfold List.Ico
exact isChain_range' _ (_ + 1) 1
· rw [eq_nil_of_le (le_of_not_gt h)]
exact .nil