proposition: Lemma lem_lelst_sorted {A} {dto : DecTotalOrder A} : forall l x, Sorted (x :: l) <-> LeLst x l /\ Sorted l.
proof: Proof. induction l; sauto l: on use: lem_lelst_trans inv: Sorted, List.Forall ctrs: Sorted. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation Program.Equality Recdef Program