proposition: Lemma lem_insert_sortedb_hlp : forall l y z, y <= z -> sortedb (y :: l) -> sortedb (y :: insert l z).
proof: Proof. induction l; sauto brefl: on inv: - ctrs: - db: arith. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation