proposition: Lemma insert_keeps_smaller x y ys : smaller y ys ---> (y <=? x) ---> smaller y (insert x ys).
proof: Proof. induction ys as [ |z zs IHzs]. - simpl. smt. - simpl. case (x <=? z). + simpl. assert (H:forall a, (y <=? z) && a ---> (y <=? x) ---> (y <=? x) && ((y <=? z) && a)) by smt. apply H. + simpl. revert IHzs. rewrite impl_implb. assert (H:forall a b, (a ---> (y <=? x) ---> b) ---> (y <=? z) && a ---> (y <=? x) ---> (y <=? z) && b) by smt. apply H. Qed.
imports: SMTCoq.SMTCoq ZArith List Bool