fact: Definition CReal_from_cauchy_scale (xn : nat -> CReal) (xcau : Un_cauchy_mod xn) : Z := Qbound_lt_ZExp2 (Qabs (CReal_from_cauchy_seq xn xcau (-1)) + 2)%Q.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax