proposition: Lemma Rseq_sum_shifts_compat : forall Un k n, Rseq_sum (Rseq_shifts Un (S k)) n = (Rseq_shifts (Rseq_sum Un) (S k) n - Rseq_sum Un k)%R.
proof: Proof. intros Un k n ; induction n. unfold Rseq_shifts, Rseq_minus ; simpl ; rewrite Nat.add_0_r ; ring. simpl ; rewrite IHn ; unfold Rseq_minus, Rseq_shifts ; simpl ; rewrite <- (plus_n_Sm k n) ; simpl ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra