English
The sublists of length n+1 for a list a :: l equal the concatenation of sublists of length n+1 for l with the sublists of length n for l prepended by a.
Русский
Подсписки длины n+1 для списка a :: l равны конкатенации подсписков длины n+1 для l и подсписков длины n для l, к которым добавляется a впереди.
LaTeX
$$$\\operatorname{sublistsLen}(n+1, a :: l) = \\operatorname{sublistsLen}(n+1, l) ++ (\\operatorname{sublistsLen}(n, l)).map (\\text{cons } a)$$$
Lean4
@[simp]
theorem sublistsLen_succ_cons (n) (a : α) (l) :
sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ (sublistsLen n l).map (cons a) := by
rw [sublistsLen, sublistsLenAux, sublistsLenAux_eq, sublistsLenAux_eq, map_id, append_nil]; rfl
