proposition: Lemma lem_lelst_sorted : forall l x, Sorted (x :: l) <-> LeLst x l /\ Sorted l.
proof: Proof. induction l; sauto use: Nat.le_trans. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation