proposition: Lemma Rser_cv_pair_compat : forall Un l, Rser_cv Un l -> Rser_cv (fun n => Un (mult 2 n) + Un (S (mult 2 n))) l.
proof: Proof. intros Un l Ucv. intros e epos. destruct (Ucv e epos) as [N Hu]. exists N; intros n nN. replace (Rseq_sum (fun n0 : nat => Un (2 * n0)%nat + Un (S (2 * n0))) n) with (Rseq_sum Un (S (2 * n))). intros; apply Hu; lia. clear nN. induction n. intros; simpl; ring. simpl Rseq_sum. replace (n + S (n + 0))%nat with (S (2 * n)) by ring. rewrite IHn. ring_simplify. assert (SIMPL : forall a b c d, a = c -> a + b + d = b + d + c) by (intros; subst; ring). apply SIMPL. apply Rseq_sum_ext; intro. simpl; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia