proposition: Lemma Csum_eq_compat_weak : forall Un Vn n, (forall j, 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. simpl; rewrite H; rewrite IHn; trivial. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Lia Lra Complex Csequence_facts Cseries