proposition: Lemma nrootCC_3 : forall r : IR, cc_IR nrootCC_3_poly ! r[*] (Two[*]II) [=] (r[+I*][1]) [^]n[*] (a[+I*][--]b) [-] (r[+I*][--][1]) [^]n[*] (a[+I*]b).
proof: Proof. intros. cut (CC_conj ((r[+I*][1]) [^]n[*] (a[+I*][--]b)) [=] (r[+I*][--][1]) [^]n[*] (a[+I*]b)); intros. Hint Resolve nrootCC_3_: algebra. apply eq_transitive_unfolded with (cc_IR (Im ((r[+I*][1]) [^]n[*] (a[+I*][--]b))) [*] (Two[*]II)). apply bin_op_wd_unfolded. apply cc_IR_wd. apply nrootCC_3_. apply eq_reflexive_unfolded. Hint Resolve calculate_Im: algebra. apply eq_transitive_unfolded with ((r[+I*][1]) [^]n[*] (a[+I*][--]b) [-] CC_conj ((r[+I*][1]) [^]n[*] (a[+I*][--]b))). apply calculate_Im. apply cg_minus_wd. apply eq_reflexive_unfolded. exact H. apply eq_transitive_unfolded with (CC_conj ((r[+I*][1]) [^]n) [*]CC_conj (a[+I*][--]b)). apply CC_conj_mult. apply eq_transitive_unfolded with (CC_conj (r[+I*][1]) [^]n[*] (a[+I*][--][--]b)). apply bin_op_wd_unfolded. apply CC_conj_nexp. apply eq_reflexive_unfolded. apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply I_wd. apply eq_reflexive_unfolded. apply cg_inv_inv. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing