proposition: Lemma Rseq_sum_shift_compat : forall Un n, Rseq_sum (Rseq_shift Un) n = (Rseq_shift (Rseq_sum Un) n - Un O)%R.
proof: Proof. intros Un n ; induction n ; [| simpl ; rewrite IHn] ; unfold Rseq_shift, Rseq_minus ; simpl ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra