proposition: Theorem mZlist_aux_correct_rev1 : forall (n : nat) (p q : Z), In q (mZlist_aux p n) -> (p <= q)%Z.
proof: Proof. intros n; elim n; clear n; simpl in |- *; auto. intros p q H'; elim H'; auto with zarith. intros n H' p q H'0; elim H'0; auto with zarith. intros H'1; apply Zle_succ_le; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz