proposition: Lemma CReal_of_DReal_bound : forall (x : DReal), QBound (CReal_of_DReal_seq x) (CReal_of_DReal_scale x).
proof: Proof. intros x n. unfold CReal_of_DReal_scale. apply (Qlt_trans_swap_hyp _ _ _ (Qbound_lt_ZExp2_spec _)). apply (Qplus_lt_l _ _ (-Qabs (CReal_of_DReal_seq x (-1)))%Q); ring_simplify. assert(forall r s : Q, (r + -1*s == r-s)%Q) as Aux by (intros; lra); rewrite Aux; clear Aux. apply (Qle_lt_trans _ _ _ (Qabs_triangle_reverse _ _)). apply (Qle_lt_trans _ 1%Q _). 2: lra. apply CReal_of_DReal_seq_bound. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra