proposition: Lemma sum_reorder_0 : forall Un n N, (n <= N)%nat -> sum_f_R0 (fun k0 : nat => Un (k0 - N)%nat) n = INR (S n) * Un O.
proof: Proof. intros Un n N HnN. induction n. simpl ; ring. rewrite tech5. rewrite IHn ; intuition (auto with real). do 3 rewrite S_INR. inversion HnN. rewrite Nat.sub_diag. ring. rewrite (proj2 (Nat.sub_0_le _ _)). ring. lia. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq