proposition: Lemma lem_insert_sorted_hlp : forall l y z, y <= z -> sortedb (y :: l) -> sortedb (y :: insert l z).
proof: Proof. time (induction l; sauto brefl: on db: arith). Undo. time (induction l; sauto brefl: on inv: - ctrs: - db: arith). Qed.
imports: Hammer(Tactics) Hammer(Reflect) Arith Lia Bool