proposition: Lemma RCpow : forall n:nat,forall x:R, Cpow (x,0)%C n = ((x^n)%R,0)%C.
proof: Proof. induction n. intro. unfold Cpow. rewrite pow_O. reflexivity. intro. rewrite<-tech_pow_Rmult. unfold Cpow at 1. fold Cpow. rewrite IHn. Cfequal. unfold Rminus. Rsimpl. reflexivity. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra