English
If a list is sorted by ≥ and is nodup, then it is sorted by > (strict).
Русский
Если список отсортирован по ≥ и не содержит повторов, то он отсортирован по >.
LaTeX
$$$ h: l.\\text{Sorted}(\\ge) \\land l.\\text{Nodup} \Rightarrow l.\\text{Sorted}(>) $$$
Lean4
protected theorem gt_of_ge [PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≥ ·)) (h₂ : l.Nodup) : l.Sorted (· > ·) :=
h₁.imp₂ (fun _ _ => lt_of_le_of_ne) <| by simp_rw [ne_comm]; exact h₂