proposition: Lemma CSUC_transport_high : forall {R : ConstructiveReals} (f g : PartialFunction (CRcarrier R)) (fL : Is_CSUC_func f) (pEq : PartialFunExtEq f g), CSUC_high _ fL = CSUC_high _ (Lext ElemCSUC f g pEq fL).
proof: Proof. intros. destruct pEq, p, f, g, fL; reflexivity. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets