proposition: Lemma ExpCC_pow : forall z n, ExpCC z[^]n [=] ExpCC (nring n[*]z).
proof: Proof. intro z. simple induction n. unfold nexp in |- *. astepl ([1]:CC). astepr (ExpCC [0]). astepr ([1]:CC). apply eq_reflexive. apply ExpCC_wd. rational. intros n0 Hrec. astepl (ExpCC z[^]n0[*]ExpCC z). astepl (ExpCC (nring n0[*]z) [*]ExpCC z). astepl (ExpCC (nring n0[*]z[+]z)). apply ExpCC_wd. algebra. rstepl ((nring n0[+][1]) [*]z). algebra. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi