proposition: Theorem mZlist_correct_rev1 : forall p q r : Z, In r (mZlist p q) -> (p <= r)%Z.
proof: Proof. intros p q r; unfold mZlist in |- *; CaseEq (q - p)%Z. intros H' H'0; elim H'0; auto with zarith. intros H'1; elim H'1. intros p0 H' H'0. apply mZlist_aux_correct_rev1 with (n := nat_of_P p0); auto. intros p0 H' H'0; elim H'0. Qed.
imports: Reals ZArith List PeanoNat Psatz