fact: Definition CReal_opp (x : CReal) : CReal := {| seq := CReal_opp_seq x; scale := CReal_opp_scale x; cauchy := CReal_opp_cauchy x; bound := CReal_opp_bound x |}.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra