English
For any list s, Shortlex r s [] is false; i.e., no list is strictly smaller than the empty list under Shortlex.
Русский
Для любого списка s Shortlex r s [] ложно; то есть ни один список не меньше пустого списка по Shortlex.
LaTeX
$$$ \\forall s : List \\alpha, \\neg \\mathrm{Shortlex} \\ r \\ s \\ [].$$$
Lean4
@[simp]
theorem not_shortlex_nil_right {s : List α} : ¬Shortlex r s [] :=
by
rw [shortlex_def]
rintro (h1 | h2)
· simp only [List.length_nil, not_lt_zero'] at h1
· exact List.not_lex_nil h2.2