proposition: Lemma cubicroot3 : forall z:C, Cpow (cubicroot z) 3=z.
proof: Proof. intro. unfold cubicroot. induction (Rcase_abs (Re z)). transitivity (-Cpow (nroot 3 (-z)) 3). unfold Cpow. field. rewrite nroot_Cpown. field. discriminate. apply nroot_Cpown. discriminate. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra