fact: Definition CReal_from_cauchy (xn : nat -> CReal) (xcau : Un_cauchy_mod xn) : CReal := {| seq := CReal_from_cauchy_seq xn xcau; scale := CReal_from_cauchy_scale xn xcau; cauchy := CReal_from_cauchy_cauchy xn xcau; bound := CReal_from_cauchy_bound xn xcau |}.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax