proposition: Theorem Q_is_archemaedian : forall x : Q_as_COrdField, {n : nat | x [<] nring n}.
proof: Proof. intros x. destruct (Q_is_archemaedian0 x) as [n Pn]. exists (nat_of_P n). simpl in *. rewrite nring_Q. rewrite <-Zpos_eq_Z_of_nat_o_nat_of_P. assumption. Qed.
imports: CoRN.model.fields.Qfield CoRN.algebra.COrdFields CoRN.stdlib_omissions.Q