proposition: Lemma Rser_cv_eq_compat : forall Un Vn l, Un == Vn -> Rser_cv Un l -> Rser_cv Vn l.
proof: Proof. intros Un Vn l H n. apply Rseq_cv_eq_compat with (sum_f_R0 Un); [apply Rsum_eq_compat ; symmetry | ] ; assumption. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic