fact: Definition Rle (x y : DReal) := forall q:Q, proj1_sig x q = true -> proj1_sig y q = true.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra