proposition: Lemma sum_f_C0_Cre_compat : forall (f : nat -> C) (N : nat), sum_f_R0 (fun n => Cre (f n)) N = Cre (sum_f_C0 f N).
proof: Proof. induction N. reflexivity. simpl ; rewrite IHN ; rewrite Cre_add_compat ; reflexivity. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia