proposition: Lemma cubicrootreal : forall (x:R), 0%R=Im (cubicroot x).
proof: Proof. intro. unfold cubicroot. destruct Rcase_abs as [xneg|xpos]. transitivity (-Im(nroot 3 (-x)%R))%R. rewrite nrootpositive. rewrite Ropp_0. reflexivity. unfold RtoC,Re,fst in xneg. lra. repeat unfold RtoC,Im,fst,snd,Copp. rewrite Ropp_0. reflexivity. symmetry. apply nrootpositive. unfold Re,RtoC,fst in xpos. apply Rge_le. assumption. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra