fact: Definition CReal_plus (x y : CReal) : CReal := {| seq := CReal_plus_seq x y; scale := CReal_plus_scale x y; cauchy := CReal_plus_cauchy x y; bound := CReal_plus_bound x y |}.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra