proposition: Theorem Q_Archimedean_inf:forall q:Q, {z:Z | q<=z /\ (z-q)<= Qone}.
proof: Proof. intros [|qp|qp]. exists (0)%Z; split; auto. destruct (Qpositive_in_Q_Archimedean_inf qp) as [z Hz]; exists z; assumption. destruct (Qpositive_in_Q_Archimedean_inf qp) as [z [Hz1 Hz2]]; exists (-(z-1))%Z; rewrite Z_to_Qopp; rewrite (Z_to_Qminus); qZ_numerals; split; apply Qle_opp; apply Qle_Zero_Qminus; rewrite Qopp_Qpos. stepr (Qone-(z - Qpos qp)); [|ring]; apply Qle_Qminus_Zero; assumption. stepr (z-(Qpos qp));[|ring]; apply Qle_Qminus_Zero; assumption. Qed.