proposition: Theorem mZlist_correct_rev2 : forall p q r : Z, In r (mZlist p q) -> (r <= q)%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. rewrite <- (Zplus_minus p q). rewrite <- inject_nat_convert with (1 := H'). apply mZlist_aux_correct_rev2; auto. intros p0 H' H'0; elim H'0. Qed.
imports: Reals ZArith List PeanoNat Psatz