proposition: Lemma lem_lelst_trans {A} {dto : DecTotalOrder A} : forall l y, LeLst y l -> forall x, leb x y -> LeLst x l.
proof: Proof. induction 1; sauto. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation Program.Equality Recdef Program