proposition: Lemma lem_insert_sorted (l : list nat) (x : nat) : Sorted l -> Sorted (insert l x).
proof: Proof. destruct l as [|y l]. - simpl; auto using Sorted. - intro H. simpl. destruct (Nat.leb_spec x y); auto using Sorted, lem_insert_sorted_hlp with arith. Qed.
imports: Hammer(Tactics) Arith Lia