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