proposition: Lemma Rpser_scal_compat : forall (r : R) An x l, Rpser An x l -> Rpser (r * An)%Rseq x (r * l).
proof: Proof. intros r An x l Hl eps eps_pos ; destruct (Req_dec r 0) as [Heq | Hneq]. exists O ; intros ; unfold R_dist ; rewrite Rseq_pps_scal_compat_l ; unfold Rseq_mult, Rseq_constant ; rewrite <- Rmult_minus_distr_l, Rabs_mult, Heq, Rabs_R0, Rmult_0_l ; assumption. pose (eps' := eps / Rabs r). assert (eps'_pos : 0 < eps') by (unfold eps', Rdiv ; apply Rlt_mult_inv_pos ; [| apply Rabs_pos_lt] ; assumption). destruct (Hl eps' eps'_pos) as [N HN] ; exists N ; intros ; unfold R_dist ; rewrite Rseq_pps_scal_compat_l ; unfold Rseq_mult, Rseq_constant ; rewrite <- Rmult_minus_distr_l, Rabs_mult ; apply Rlt_le_trans with (Rabs r * eps'). apply Rmult_lt_compat_l ; [apply Rabs_pos_lt | apply HN] ; assumption. right ; unfold eps' ; field ; apply Rabs_no_R0 ; assumption. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR