fact: Definition CReal_abs (x : CReal) : CReal := {| seq := CReal_abs_seq x; scale := CReal_abs_scale x; cauchy := CReal_abs_cauchy x; bound := CReal_abs_bound x |}.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra