proposition: Lemma CR_cv_max : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (l a : CRcarrier R), CR_cv R un l -> CR_cv R (fun n : nat => CRmax (un n) a) (CRmax l a).
proof: Proof. intros. intro p. specialize (H p) as [n H]. exists n. intros. apply (CRle_trans _ _ _ (CRmax_contract _ _ a)). exact (H i H0). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile