proposition: Lemma trigoform: forall z : C, z=(cos(cargument z),sin(cargument z))*(Cmod z,0).
proof: Proof. intro. unfold cargument. induction Rneg_or_not as [znotneg|zneg]. pose proof (Csqrt_Cpow2 z) as z2. induction (Csqrt z) as (u,v). assert (Cmod z<>0%R) as zmodnot0. intro mz0. pose proof (Cmod_eq_0 z mz0) as z0. rewrite z0 in znotneg. unfold Re,Im,fst,snd,RtoC in znotneg. destruct znotneg as [rezspos|imzneq0]. apply (Rlt_neq _ _ rezspos). reflexivity. apply imzneq0. reflexivity. assert(u<>0) as uneq0. intro ueq0. rewrite ueq0 in z2. unfold Cmult,fst,snd in z2. repeat rewrite Rmult_0_r in z2. repeat rewrite Rmult_0_l in z2. unfold Rminus in z2. repeat rewrite Rplus_0_l in z2. rewrite<-z2 in znotneg. unfold Re,Im,fst,snd in znotneg. destruct znotneg as [sqrneg|neq00]. apply (Rlt_not_ge (Rsqr v) 0). unfold Rsqr. apply Ropp_lt_cancel. rewrite Ropp_0. assumption. apply Rle_ge. apply Rle_0_sqr. apply neq00. reflexivity. assert( forall x:R, (x*x)%R =(Rsqr x)%R) as multsqr. unfold Rsqr. reflexivity. rewrite<-z2. unfold Im,Re,fst,snd. rewrite z2 at 2. unfold Cmult,Re,Im,fst,snd. Rsimpl. rewrite cos_2a. repeat rewrite multsqr. rewrite sin2. assert( forall x:R, cos(x)<>0 -> (sin((INR 2) * x))%R =(2*(tan x)*(Rsqr (cos x)))%R) as sineq. intros. unfold tan,Rsqr. rewrite sin_2a. field. assumption. rewrite sineq. rewrite cosatan. rewrite atan_right_inv. assert(Cmod z=(u*u+v*v)%R) as modz. rewrite<-z2. rewrite Cmod_mult. repeat rewrite multsqr. unfold Cmod,fst,snd. rewrite Rsqr_sqrt. repeat rewrite Rsqr_pow2. reflexivity. apply normpos. rewrite modz. unfold Rsqr. rewrite modz in zmodnot0. f_equal; field; split; assumption. apply Rlt_neq. apply cosatanspos. rewrite cos_PI. rewrite sin_PI. unfold Cmult,fst,snd. destruct z as (u,v). unfold Im,snd,Re,fst,Rminus in zneg. rewrite (proj1 zneg). fold (RtoC u). rewrite Cmod_R. unfold Rminus,RtoC. Rsimpl. rewrite Rabs_left1. f_equal. field. apply (proj2 zneg). Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra