proposition: Theorem mZlist_aux_correct : forall (n : nat) (p q : Z), (p <= q)%Z -> (q <= p + Z_of_nat n)%Z -> In q (mZlist_aux p n).
proof: Proof. intros n; elim n; clear n; auto. intros p q; try rewrite <- Zplus_0_r_reverse. intros H' H'0; simpl in |- *; left. apply Zle_antisym; auto. intros n H' p q H'0 H'1; case (Zle_lt_or_eq _ _ H'0); intros H'2. simpl in |- *; right. apply H'; lia. simpl in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz