English
For any relation r, append_right states that if s1 is related to s2 by Lex r, then for any t the concatenation s2++t preserves the Lex relation from s1 to s2++t.
Русский
Для любой связи r, append_right утверждает, что если s1 связано с s2 через Lex r, то для любого t конкатенация s2++t сохраняет отношение Lex между s1 и s2++t.
LaTeX
$$$\\forall r:\\alpha\\to\\alpha\\to\\mathrm{Prop},\\forall \\{s_1,s_2\\}:\\mathrm{List}\\ \\alpha,\\forall t:\\mathrm{List}\\ \\alpha,\\ \\mathrm{Lex}\\ r\\ s_1\\ s_2 \\Rightarrow \\mathrm{Lex}\\ r\\ s_1\\ (s_2\\;\\;\\; t).$$$
Lean4
theorem append_right (r : α → α → Prop) : ∀ {s₁ s₂} (t), Lex r s₁ s₂ → Lex r s₁ (s₂ ++ t)
| _, _, _, nil => nil
| _, _, _, cons h => cons (append_right r _ h)
| _, _, _, rel r => rel r
