proposition: Lemma CSUC_bound_ext : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b c d : CRcarrier R) (cont_mod : forall x:CRcarrier R, 0 < x -> CRcarrier R), a == c -> b == d -> CSUC f a b cont_mod -> CSUC f c d cont_mod.
proof: Proof. intros. destruct H1. split. exact u. intros. destruct H1. apply c0. left. apply (CRlt_le_trans _ _ _ c1). apply H. apply c0. right. apply (CRle_lt_trans _ d). apply H0. exact c1. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets