English
If l1 is a sublist of l2, then for any n, sublistsLen n l1 is a sublist of sublistsLen n l2.
Русский
Если l1 является подсписком l2, то для любого n подспискиLen n l1 являются подсписком подсписков Len n l2.
LaTeX
$$$\\forall n\\ {l1\\ l2} : List(\\alpha),\n l1 <+ l2 \\Rightarrow \\operatorname{sublistsLen}(n, l1) <+ \\operatorname{sublistsLen}(n, l2)$$$
Lean4
theorem sublistsLen_sublist_of_sublist (n) {l₁ l₂ : List α} (h : l₁ <+ l₂) : sublistsLen n l₁ <+ sublistsLen n l₂ :=
by
induction n generalizing l₁ l₂ with
| zero => simp
| succ n IHn => ?_
induction h with
| slnil => rfl
| cons a _ IH =>
refine IH.trans ?_
rw [sublistsLen_succ_cons]
apply sublist_append_left
| cons₂ a s IH => simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)
