proposition: Lemma lem_sorted_concat_1 {A} {dto : DecTotalOrder A} : forall (l l1 l2 : list A) x y, Permutation l (l1 ++ y :: l2) -> Sorted (x :: l1) -> leb x y -> Sorted (y :: l2) -> Sorted l -> Sorted (x :: l).
proof: Proof. intros. rewrite lem_lelst_sorted in *. sauto use: lem_lelst_trans, lem_lelst_perm_rev, lem_lelst_app inv: -. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation Program.Equality Recdef Program