proposition: Theorem comCpow: forall n : nat, forall z:C, forall u:C, (Cpow (z*u)%C n)=((Cpow z n)*(Cpow u n))%C.
proof: Proof. induction n. intros. unfold Cpow. Cfequal. f_equal; field. intros. unfold Cpow. fold Cpow. rewrite IHn. field. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra