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