English
If s1 is Shortlex-smaller than s2, then s1 stays smaller when any tail t is appended to the right of s2, i.e., s2 ++ t is larger in the same relation.
Русский
Если s1 меньше s2 по Shortlex, то добавление хвоста t справа к s2 сохраняет порядок.
LaTeX
$$$ \\forall s_1\\, s_2\\, t,\\ Shortlex\\ r\\ s_1\\ s_2 \\Rightarrow Shortlex\\ r\\ s_1\\ (s_2\\ ++\\ t). $$$
Lean4
theorem append_right {s₁ s₂ : List α} (t : List α) (h : Shortlex r s₁ s₂) : Shortlex r s₁ (s₂ ++ t) :=
by
rcases shortlex_def.mp h with h1 | h2
· apply of_length_lt
rw [List.length_append]
cutsat
cases t with
| nil =>
rw [List.append_nil]
exact h
| cons head tail =>
apply of_length_lt
rw [List.length_append, List.length_cons]
cutsat
