English
If r is well-founded, then Shortlex r on lists is well-founded.
Русский
Если r хорошо основан, то Shortlex r на списках хорошо основан.
LaTeX
$$$ \\forall r,\\, WellFounded\\ r \\Rightarrow WellFounded\\ (Shortlex\\ r). $$$
Lean4
theorem wf (h : WellFounded r) : WellFounded (Shortlex r) :=
.intro fun a => by
induction len_a : a.length using Nat.caseStrongRecOn generalizing a with
| zero =>
rw [List.length_eq_zero_iff] at len_a
rw [len_a]
exact Acc.intro _ <| fun _ ylt => (not_shortlex_nil_right ylt).elim
| ind n ih =>
obtain ⟨head, tail, rfl⟩ := List.exists_of_length_succ a len_a
rw [List.length_cons, add_left_inj] at len_a
apply Acc.shortlex (WellFounded.apply h head) (ih n le_rfl tail len_a)
intro l ll
apply ih l.length _ _ rfl
rw [← len_a]
exact Nat.le_of_lt_succ ll
