proposition: Lemma nrootpositive : forall x:R, forall n:nat, 0<=x -> Im( nroot n x ) =0%R.
proof: Proof. intros. unfold nroot. induction(Ceq_dec x 0) as [xeq0|xneq0]. unfold RtoC,Im,snd. reflexivity. unfold Im,Re,Cmult,fst,snd. Rsimpl. apply Rmult_eq_0_compat_r. rewrite<-sin_0. f_equal. unfold Rdiv. apply Rmult_eq_0_compat_r. unfold cargument,Csqrt. rewrite Cmod_R. unfold Rabs,Re,Im,RtoC,fst,snd. destruct Rcase_abs as [xneg|xpos]. lra. unfold Rdiv. rewrite<-double. unfold Rdiv. destruct Rneg_or_not as [vra|fal]. repeat rewrite Rmult_0_l. rewrite atan_0. apply Rmult_0_r. exfalso. unfold Re,Im,fst,snd in fal. destruct fal. apply xneq0. f_equal. apply Rle_antisym; assumption. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra