proposition: Lemma lem_insert_sorted' : forall l x, sortedb l -> sortedb (insert l x).
proof: Proof. destruct l; hauto brefl!: on use: lem_insert_sorted_hlp db: arith ctrs: Sorted. Qed.
imports: Hammer(Tactics) Hammer(Reflect) Arith Lia Bool