proposition: Lemma Rsum_switch_index : forall Un N, sum_f_R0 (fun n => Un (N - n)%nat) N = sum_f_R0 Un N.
proof: Proof. intros Un N. induction N. trivial. rewrite decomp_sum by lia; simpl. rewrite IHN. ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith