proposition: Lemma lem_insert_sorted_hlp : forall l y z, y <= z -> Sorted (y :: l) -> Sorted (y :: insert l z).
proof: Proof. intro l. induction l as [|a l IH]. - intros; simpl; auto using Sorted. - intros x y H1 H2. simpl. destruct (Nat.leb_spec y a) as [H|H]. + repeat constructor; auto. inversion H2; auto. + inversion_clear H2. auto using Sorted with arith. Qed.
imports: Hammer(Tactics) Arith Lia