English
If t1 is Shortlex-smaller than t2, then s ++ t1 is Shortlex-smaller than s ++ t2 for any s.
Русский
Если t1 меньше t2 по Shortlex, то при добавлении одинакового префикса s порядок сохраняется: s ++ t1 < s ++ t2.
LaTeX
$$$ \\forall t_1\\, t_2\\, s,\\ Shortlex\\ r\\ t_1\\ t_2 \\Rightarrow Shortlex\\ r\\ (s\\ ++\\ t_1)\\ (s\\ ++\\ t_2). $$$
Lean4
theorem append_left {t₁ t₂ : List α} (h : Shortlex r t₁ t₂) (s : List α) : Shortlex r (s ++ t₁) (s ++ t₂) :=
by
rcases shortlex_def.mp h with h1 | h2
· apply of_length_lt
rw [List.length_append, List.length_append]
cutsat
cases s with
| nil =>
rw [List.nil_append, List.nil_append]
exact h
| cons head tail =>
apply of_lex
· simp only [List.cons_append, List.length_cons, List.length_append, add_left_inj, add_right_inj]
exact h2.1
exact List.Lex.append_left r h2.2 (head :: tail)
