proposition: Lemma sum_f_R0_sum1 : forall u n, sum1 u (S n) = sum_f_R0 (fun i => u (Z_of_nat (S i))) n.
proof: Proof. intros. induction n. compute; ring. simpl in *. rewrite IHn. trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith