proposition: Lemma lem_lelst_sorted {A} {dto : DecTotalOrder A} : forall l x, Sorted (x :: l) <-> LeLst x l /\ Sorted l.
proof: Proof. time (induction l; sauto). Undo. induction l; sintuition. Undo. induction l; qsimpl. Undo. time (induction l; sauto use: lem_lelst_trans). Undo. time (induction l; sauto use: lem_lelst_trans inv: Sorted, List.Forall ctrs: Sorted). Undo. time (induction l; sauto lazy: on use: lem_lelst_trans inv: Sorted, List.Forall ctrs: Sorted). Qed.
imports: Hammer(Tactics) Hammer(Reflect) Arith Lia Sorting.Permutation Program