proposition: Lemma CReal_from_cauchy_bound : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn), QBound (CReal_from_cauchy_seq xn xcau) (CReal_from_cauchy_scale xn xcau).
proof: Proof. intros xn xcau n. unfold CReal_from_cauchy_scale. apply (Qlt_trans_swap_hyp _ _ _ (Qbound_lt_ZExp2_spec _)). apply (Qplus_lt_l _ _ (-Qabs (CReal_from_cauchy_seq xn xcau (-1)))%Q); ring_simplify. assert(forall x y : Q, (x + -1*y == x-y)%Q) as Aux by (intros x y; lra); rewrite Aux; clear Aux. apply (Qle_lt_trans _ _ _ (Qabs_triangle_reverse _ _)). apply (Qle_lt_trans _ 1%Q _). 2: lra. apply CReal_from_cauchy_seq_bound. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax