proposition: Lemma Csqrt_Cpow2 : forall z: C, (Csqrt z)*(Csqrt z)=z.
proof: Proof. intro. unfold Cmult. pose (fst (Csqrt z)) as u. pose (snd (Csqrt z)) as v. fold u. fold v. fold (Rsqr u). fold (Rsqr v). induction z as (x,y). rewrite Rmult_comm. rewrite<-double. unfold Csqrt,Re,Im,snd,fst in u,v. fold u in v. destruct Rneg_or_not as [znotneg|zneg]. unfold Im,Re,fst,snd in *. assert(0<(Cmod(x,y)+x)%R) as nspos. unfold Cmod,fst,snd. destruct znotneg as [xspos|ynot0]. apply Rplus_le_lt_0_compat. apply sqrt_pos. assumption. apply coordnormb. assumption. assert(0<u) as uspos. unfold u. apply sqrt_lt_R0. apply Rdiv_lt_0_compat. assumption. apply Rlt_0_2. pose proof (Rlt_neq _ _ uspos) as uneq0. unfold v. f_equal. rewrite Rsqr_div. rewrite<-(Rdiv_1 (Rsqr u)) at 1. rewrite Rdiv_minus. fold (Rsqr (Rsqr u)). unfold u. rewrite Rsqr_sqrt. rewrite Rsqr_div. rewrite Rsqr_plus. unfold Cmod at 1. unfold fst,snd. rewrite Rsqr_sqrt. unfold Rsqr. field. apply Rlt_neq. assumption. apply normpos. apply Rlt_neq. apply Rlt_0_2. left. apply Rdiv_lt_0_compat. assumption. apply Rlt_0_2. apply R1_neq_R0. apply Rlt_neq. apply Rlt_0_sqr. assumption. assumption. field. assumption. unfold Re,Im,fst,snd in *. unfold u,v. destruct zneg as [yeq0 xneg]. rewrite yeq0. fold (RtoC x). rewrite (Cmod_R x). rewrite Rabs_left1. unfold Rdiv. Rsimpl. rewrite sqrt_0. Rsimpl. rewrite Rsqr_sqrt. unfold Rminus,Rsqr. Rsimpl. reflexivity. rewrite<-Ropp_0. apply Ropp_le_contravar. assumption. assumption. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra