proposition: Lemma sum_f_C0_const_1 : forall (n : nat) (a : C), a = sum_f_C0 (fun _ => a/INC( S n )) (n).
proof: Proof. unfold Cdiv. intros. rewrite <- sum_f_C0_const. field. apply not_0_INC. intuition lia. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia