fact: Definition CSUCposPointApproxStep (n : nat) (currStep : CSUCposPointApprox) : { nextApprox : CSUCposPointApprox | x currStep <= x nextApprox /\ y nextApprox <= y currStep /\ y nextApprox - x nextApprox == (y currStep - x currStep) * CR_of_Q R (1#2) }.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets