proposition: Lemma Qarchimedean_le : forall q : Q, { p : positive | q <= Z.pos p # 1 }.
proof: Proof. intros. destruct q as [a b]. destruct a. - exists xH. discriminate. - exists p. unfold Qle; simpl. apply Pos.mul_le_mono_l, Pos.le_1_l. - exists xH. discriminate. Defined.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon