proposition: Lemma sum_minus: forall Un n n2, - sum_f_R0 Un n + sum_f_R0 Un (S (n2 + n)) = sum_f_R0 (fun k : nat => Un (S n + k)%nat) n2.
proof: Proof. intros Un n n2. induction n2. simpl. ring_simplify. rewrite Nat.add_0_r. reflexivity. repeat rewrite tech5. rewrite <- IHn2. rewrite <- plus_n_Sm. do 2 rewrite plus_Sn_m. rewrite Nat.add_comm. ring. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq