proposition: Lemma CR_cv_scale : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a : CRcarrier R) (s : CRcarrier R), CR_cv R u s -> CR_cv R (fun n => u n * a) (s * a).
proof: Proof. intros. intros n. destruct (CR_archimedean R (1 + CRabs R a)). destruct (H (n * x)%positive). exists x0. intros. unfold CRminus. rewrite CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r. apply (CRle_trans _ ((CR_of_Q R (1 # n * x)) * CRabs R a)). - rewrite CRabs_mult. apply CRmult_le_compat_r. + apply CRabs_pos. + apply c0, H0. - setoid_replace (1 # n * x)%Q with ((1 # n) *(1# x))%Q. 2: reflexivity. rewrite <- (CRmult_1_r (CR_of_Q R (1#n))). rewrite CR_of_Q_mult, CRmult_assoc. apply CRmult_le_compat_l. + apply CR_of_Q_le. discriminate. + intro abs. apply (CRmult_lt_compat_l (CR_of_Q R (Z.pos x #1))) in abs. * rewrite CRmult_1_r, <- CRmult_assoc, <- CR_of_Q_mult in abs. rewrite (CR_of_Q_morph R ((Z.pos x # 1) * (1 # x))%Q 1%Q) in abs. -- rewrite CRmult_1_l in abs. apply (CRlt_asym _ _ abs), (CRlt_trans _ (1 + CRabs R a)). 2: exact c. rewrite <- CRplus_0_l, <- CRplus_assoc. apply CRplus_lt_compat_r. rewrite CRplus_0_r. apply CRzero_lt_one. -- unfold Qmult, Qeq, Qnum, Qden. ring_simplify. rewrite Pos.mul_1_l. reflexivity. * apply (CRlt_trans _ (1+CRabs R a)). 2: exact c. rewrite CRplus_comm. rewrite <- (CRplus_0_r 0). apply CRplus_le_lt_compat. -- apply CRabs_pos. -- apply CRzero_lt_one. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs