proposition: Lemma Qpositive_in_Q_Archimedean_inf:forall qp:Qpositive, {z:Z | (Qpos qp)<=z /\ (z-(Qpos qp))<= Qone}.
proof: Proof. induction qp as [qp [z [Hz1 Hz2]]|qp [z [Hz1 Hz2]]|]; simpl. exists (z+1)%Z; split;rewrite Qpos_nR; rewrite Z_to_Qplus; qZ_numerals. apply Qle_plus_plus; trivial. stepl (z-Qpos qp); [assumption|ring]. exists (1)%Z; split; rewrite Qpos_dL; fold (Qdiv (Qpos qp) (Qpos qp + Qone)); qZ_numerals. apply Qmult_pos_Qdiv_Qle; auto; stepr (Qpos qp+Qone); [|ring]; apply Qle_Zero_Qminus; stepr Qone; [auto|ring]. stepl (Qone/(Qpos qp + Qone)); [|field; auto]; apply Qmult_pos_Qdiv_Qle; auto; stepr (Qpos qp+Qone); [|ring]; apply Qle_Zero_Qminus; stepr (Qpos qp); [auto|ring]. exists (1)%Z; split; auto. Qed.