proposition: Lemma Csum_eq_compat : forall Un Vn n, (forall j, (j <= n)%nat -> Un j = Vn j) -> sum_f_C0 Un n = sum_f_C0 Vn n.
proof: Proof. intros Un Vn n H. induction n. apply H; lia. simpl; rewrite H; try lia. rewrite IHn; trivial. intros j Hj. apply H; lia. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Lia Lra Complex Csequence_facts Cseries