proposition: Theorem Cpowexp : forall n:nat, forall x:R, ((exp(x))^n=exp((INR n)*x)) % R.
proof: Proof. induction n. unfold INR. intro. rewrite Rmult_0_l. rewrite exp_0. rewrite pow_O. reflexivity. intros. rewrite<-tech_pow_Rmult. rewrite S_INR. rewrite Rmult_plus_distr_r. rewrite Rmult_1_l. rewrite exp_plus. rewrite IHn. field. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra