fact: Definition DRealRepr (x : DReal) : CReal := {| seq := CReal_of_DReal_seq x; scale := CReal_of_DReal_scale x; cauchy := CReal_of_DReal_cauchy x; bound := CReal_of_DReal_bound x |}.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra