proposition: Lemma nrootCC_3_ : forall r : IR, nrootCC_3_poly ! r [=] Im ((r[+I*][1]) [^]n[*] (a[+I*][--]b)).
proof: Proof. intros. unfold nrootCC_3_poly in |- *. Hint Resolve nrCC3_a1 nrCC3_a7: algebra. apply eq_transitive_unfolded with (Im nrCC3_poly' ! (cc_IR r)). apply nrCC3_a1. apply Im_wd. apply nrCC3_a7. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing