fact: Definition BinarySubdiv {R : ConstructiveReals} (a b : CRcarrier R) (n i : nat) : CRcarrier R := a + CR_of_Q R (Z.of_nat i # 1) * (b-a) * CRpow (CR_of_Q R ((/2))) n.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia