proposition: Lemma CReal_abs_upper_bound (x : CReal) : { n : positive & CReal_abs x < inject_Q (Z.pos n # 1) }.
proof: Proof. intros. destruct (Rup_pos x) as [np Hnp]. destruct (Rup_pos (-x)) as [nn Hnn]. exists (Pos.max np nn). apply Rabs_def1. - apply (CReal_lt_le_trans _ _ _ Hnp), inject_Q_le. unfold Qle, Qnum, Qden; ring_simplify. lia. - apply (CReal_lt_le_trans _ _ _ Hnn), inject_Q_le. unfold Qle, Qnum, Qden; ring_simplify. lia. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra