proposition: Lemma lem_insert_sorted_2 : forall l x, Sorted l -> Sorted (insert l x).
proof: Proof. induction l as [|y l IH]. - sauto. - intros x H. simpl. destruct (Nat.leb_spec x y) as [H1|H1]. + constructor; assumption. + qauto use: lem_lelst_sorted, lem_lelst_insert, Nat.lt_le_incl. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation