proposition: Lemma is_sorted_cons x xs : (is_sorted (x::xs)) <---> (is_sorted xs && smaller x xs).
proof: Proof. induction xs as [ |y ys IHys]. - reflexivity. - change (is_sorted (x :: y :: ys)) with ((x <=? y)%Z && (is_sorted (y::ys))). change (smaller x (y :: ys)) with ((x <=? y)%Z && (smaller x ys)). generalize (is_sorted_smaller x y ys). revert IHys. rewrite !impl_implb. assert (H:forall a b c d, (a <---> b && c) ---> ((x <=? y) && d ---> a) ---> ((x <=? y) && d <---> d && ((x <=? y) && c))) by smt. apply H. Qed.
imports: SMTCoq.SMTCoq ZArith List Bool