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