proposition: Lemma Rup_pos (x : CReal) : { n : positive & x < inject_Q (Z.pos n # 1) }.
proof: Proof. intros. destruct (CRealArchimedean x) as [p [maj _]]. destruct p. - exists 1%positive. apply (CReal_lt_trans _ 0 _ maj). apply CRealLt_0_1. - exists p. exact maj. - exists 1%positive. apply (CReal_lt_trans _ (inject_Q (Z.neg p # 1)) _ maj). apply (CReal_lt_trans _ 0). + apply inject_Q_lt. reflexivity. + apply CRealLt_0_1. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra