proposition: Lemma insert_keeps_sorted x l : is_sorted l -> is_sorted (insert x l).
proof: Proof. induction l as [ |y ys IHys]. - reflexivity. - intro H. simpl. case_eq (x <=? y); intro Heq. + change ((x <=? y)%Z && (is_sorted (y::ys))). rewrite Heq, H. reflexivity. + rewrite eq_false in Heq. rewrite (eqb_prop _ _ (is_sorted_cons _ _)) in H. rewrite (eqb_prop _ _ (is_sorted_cons _ _)). generalize (insert_keeps_smaller x y ys). revert IHys H Heq. rewrite !impl_implb. assert (H: forall a b c d, (a ---> b) ---> a && c ---> negb (x <=? y) ---> (c ---> (y <=? x) ---> d) ---> b && d) by smt. apply H. Qed.
imports: SMTCoq.SMTCoq ZArith List Bool