proposition: Lemma UC_right_bound_cv : forall {R : ConstructiveReals} (a b : CRcarrier R) (bn : nat -> CRcarrier R) (f : CRcarrier R -> CRcarrier R) (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f cont_mod) (leab : a <= b) (lebbn : forall n:nat, b <= bn n), CR_cv R bn b -> CR_cv R (fun n : nat => UC_integral f a (bn n) cont_mod fCont (CRle_trans a b (bn n) leab (lebbn n))) (UC_integral f a b cont_mod fCont leab).
proof: Proof. intros. intro p. assert (0 < CR_of_Q R (1 # p)). { apply CR_of_Q_pos. reflexivity. } destruct (UC_right_bound_continuous f a b leab _ H0 cont_mod fCont) as [eta [etaPos etaMaj]]. pose proof (Un_cv_nat_real _ _ H eta etaPos) as [n nmaj]. exists n. intros. rewrite CRabs_minus_sym. assert (bn i < b + eta). { specialize (nmaj i H1). apply (CRplus_lt_reg_l R (-b)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l, CRplus_comm. exact (CRle_lt_trans _ _ _ (CRle_abs _) nmaj). } apply (etaMaj (bn i) (pair (lebbn i) H2)). Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont