proposition: Theorem mZlist_aux_correct_rev2 : forall (n : nat) (p q : Z), In q (mZlist_aux p n) -> (q <= p + Z_of_nat n)%Z.
proof: Proof. intros n; elim n; clear n; auto. intros p q H'; elim H'; auto with zarith. intros H'0; elim H'0. intros n H' p q H'0; elim H'0; auto with zarith. intros H'1; rewrite inj_S; rewrite <- Zplus_succ_comm; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz