proposition: Lemma seq_cv_0_mult : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a : CRcarrier R), CR_cv R u 0 -> CR_cv R (fun n => u n * a) 0.
proof: Proof. intros R u a H p. destruct (CRup_nat (CRabs _ a)) as [n nup]. destruct (H (p * Pos.of_nat n)%positive) as [k kmaj]. exists k. intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r. specialize (kmaj i H0). unfold CRminus in kmaj. rewrite CRopp_0, CRplus_0_r in kmaj. rewrite CRabs_mult. apply (CRmult_le_compat_r (CR_of_Q R (Z.of_nat n # 1))) in kmaj. rewrite <- CR_of_Q_mult in kmaj. setoid_replace ((1 # p * Pos.of_nat n) * (Z.of_nat n # 1))%Q with (1#p)%Q in kmaj. apply (CRle_trans _ (CRabs _ (u i) * CR_of_Q R (Z.of_nat n # 1))). apply CRmult_le_compat_l. apply CRabs_pos. apply CRlt_asym, nup. exact kmaj. unfold Qmult, Qnum, Qden. rewrite Z.mul_1_l, Pos.mul_1_r. unfold Qeq, Qnum, Qden. rewrite Z.mul_1_l. rewrite Pos2Z.inj_mul, Z.mul_comm. unfold Z.of_nat. simpl. destruct n. exfalso. simpl in nup. exact (CRabs_pos a nup). rewrite Pos.of_nat_succ. reflexivity. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Zle_0_nat. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile