proposition: Lemma lem_lelst_insert : forall l n m, n <= m -> LeLst n l -> LeLst n (insert l m).
proof: Proof. induction l; sauto. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation