proposition: Lemma Rseq_cv_pos_infty_le_compat : forall Un Vn, (forall n, Un n <= Vn n) -> Rseq_cv_pos_infty Un -> Rseq_cv_pos_infty Vn.
proof: Proof. intros Un Vn Hle Un_inf M ; destruct (Un_inf M) as [N HN] ; exists N ; intros n n_lb ; apply Rlt_le_trans with (Un n) ; [apply HN | apply Hle] ; assumption. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics