proposition: Lemma Q_Archimedean_nat_inf:forall q:Q, {n:nat | q<=n }.
proof: Proof. intro q. destruct (Q_le_lt_dec q Zero). exists O; qnat_zero. exists (Z.abs_nat (up_Q q)). destruct (up_Q_property q) as [H1 H2]. stepr (up_Q q); trivial. assert (H3:(0<=(up_Q q))%Z). assert (H4:Zero<Z_to_Q (up_Q q));[apply Qlt_le_trans with q; auto|]; generalize (Q_to_Z_monotone _ _ H4); simpl; rewrite Q_to_Z_to_Q; trivial. rewrite (Z_of_nat_Zabs_nat_pos _ H3); reflexivity. Qed.