proposition: Lemma sum_f_C0_const : forall (n : nat) (a : C), a * INC (S n) = sum_f_C0 (fun _ => a) (n).
proof: Proof. intros n a. induction n. simpl. eauto with *. rewrite S_INC. rewrite sum_f_C0_simpl. rewrite <- IHn. field. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia