proposition: Theorem moivre : forall n:nat, forall x:R, Cpow (cos x,sin x) n=(cos ((INR n)*x), sin ((INR n)*x))%C.
proof: Proof. induction n. unfold Cpow,INR. intros. Rsimpl. rewrite cos_0. rewrite sin_0. reflexivity. intro. rewrite S_INR. rewrite Rmult_plus_distr_r. rewrite Rmult_1_l. rewrite cos_plus. rewrite sin_plus. unfold Cpow. fold Cpow. rewrite IHn. Cfequal. f_equal; field. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra