proposition: Lemma lem_lelst_app {A} {dto : DecTotalOrder A} : forall l1 l2 x, LeLst x l1 -> LeLst x l2 -> LeLst x (l1 ++ l2).
proof: Proof. induction 1; sauto. Qed.
imports: Hammer(Tactics) Hammer(Reflect) Arith Lia Sorting.Permutation Program