proposition: Lemma Rseq_sum_reindex_compat : forall Un n, Rseq_sum Un n = Rseq_sum (fun i => Un (n - i)%nat) n.
proof: Proof. intros Un n ; revert Un ; induction n ; intro Un. reflexivity. do 2 rewrite Rseq_sum_simpl. rewrite (IHn (fun i => Un (S n - i)%nat)), Nat.sub_diag. rewrite (Rseq_sum_ext_strong (fun i => Un (S n - (n - i))%nat) (Rseq_shift Un)). rewrite Rseq_sum_shift_compat ; unfold Rseq_shift ; simpl ; ring. intros m m_bd ; unfold Rseq_shift ; replace (S n - (n - m))%nat with (S m) by lia ; reflexivity. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra