proposition: Lemma Rsum_shift : forall Un, sum_f_R0 (Rseq_shift Un) == ((Rseq_shift (sum_f_R0 Un)) - (Un O))%Rseq.
proof: Proof. intros Un n. assert (REW : forall a b c, c + a = b -> a = b - c) by (intros; subst; field). apply REW. induction n. compute; field. unfold Rseq_shift in *. do 2 rewrite tech5. rewrite <- IHn. unfold Rseq_constant. field. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic