proposition: Lemma CR_cv_growing : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (l : CRcarrier R), (forall n:nat, un n <= un (S n)) -> (forall n:nat, un n <= l) -> (forall p : positive, { n : nat | l - un n <= CR_of_Q R (1#p) }) -> CR_cv R un l.
proof: Proof. intros. intro p. specialize (H1 p) as [n nmaj]. exists n. intros. rewrite CRabs_minus_sym, CRabs_right. apply (CRle_trans _ (l - un n)). apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. exact (growing_transit _ H n i H1). exact nmaj. rewrite <- (CRplus_opp_r (un i)). apply CRplus_le_compat. apply H0. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions