proposition: Lemma seq_cv_0_bound : forall {R : ConstructiveReals} (u v : nat -> CRcarrier R), (forall n:nat, 0 <= u n) -> (forall n:nat, u n <= v n) -> CR_cv R v 0 -> CR_cv R u 0.
proof: Proof. intros. intro p. specialize (H1 p) as [n H1]. exists n. intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite CRabs_right. specialize (H1 i H2). unfold CRminus in H1. rewrite CRopp_0, CRplus_0_r, CRabs_right in H1. exact (CRle_trans _ (v i) _ (H0 i) H1). exact (CRle_trans _ (u i) _ (H i) (H0 i)). exact (H i). Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile