proposition: Theorem mZlist_correct : forall p q r : Z, (p <= r)%Z -> (r <= q)%Z -> In r (mZlist p q).
proof: Proof. intros p q r H' H'0; unfold mZlist in |- *; CaseEq (q - p)%Z; auto with zarith. intros H'1; rewrite (Zle_antisym r p); auto with datatypes. auto with zarith. intros p0 H'1; apply mZlist_aux_correct; auto. rewrite inject_nat_convert with (1 := H'1); auto with zarith. intros; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz