fact: Record IntervalExtension {R : ConstructiveReals} {x y : CRcarrier R} : Set := { ext_eta : CRcarrier R; left_ordered : 0 < x - ext_eta < x; right_ordered : y < y + ext_eta; }.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia