proposition: Lemma lem_insert_sorted' (l : list nat) (x : nat) : Sorted l -> Sorted (insert l x).
proof: Proof. time (destruct l; sauto use: lem_insert_sorted_hlp db: arith). Undo. time (destruct l; sauto use: lem_insert_sorted_hlp inv: - ctrs: Sorted db: arith). Qed.
imports: Hammer(Tactics) Arith Lia