proposition: Lemma lem_insert_sortedb : forall l x, sortedb l -> sortedb (insert l x).
proof: Proof. destruct l; hauto brefl: on use: lem_insert_sortedb_hlp db: arith. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation