proposition: Lemma nrootCC_3' : forall x : IR, nrootCC_3'_poly ! x [=] x[^]n[-]c.
proof: Proof. intros. unfold nrootCC_3'_poly in |- *. cut ((_X_[^]n) ! x [=] x[^]n). intros. apply eq_transitive_unfolded with ((_X_[^]n) ! x[-] (_C_ c) ! x). apply minus_apply. apply cg_minus_wd. exact H. apply c_apply. apply eq_transitive_unfolded with (_X_ ! x[^]n). apply nexp_apply. apply un_op_wd_unfolded. apply x_apply. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing