proposition: Lemma nrootCC_2' : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c -> z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] [0] -> (z[^]n) [^]2 [=] c[^]2.
proof: Proof. intros. cut (z[^]n[*]CC_conj c [=] CC_conj z[^]n[*]c); intros. apply (mult_cancel_rht _ ((z[^]n) [^]2) (c[^]2) (CC_conj c)). apply CC_conj_strext. apply ap_wdl_unfolded with c. 2: apply eq_symmetric_unfolded. 2: apply CC_conj_conj. apply ap_wdr_unfolded with ([0]:CC). exact c_. apply eq_symmetric_unfolded. exact CC_conj_zero. apply eq_transitive_unfolded with (z[^]n[*]z[^]n[*]CC_conj c). apply bin_op_wd_unfolded. apply nexp_two. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (z[^]n[*] (z[^]n[*]CC_conj c)). apply eq_symmetric_unfolded. apply mult_assoc_unfolded. apply eq_transitive_unfolded with (z[^]n[*] (CC_conj z[^]n[*]c)). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. exact H1. apply eq_transitive_unfolded with (z[^]n[*]CC_conj z[^]n[*]c). apply mult_assoc_unfolded. apply eq_transitive_unfolded with ((z[*]CC_conj z) [^]n[*]c). apply bin_op_wd_unfolded. apply eq_symmetric_unfolded. apply mult_nexp. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (c[*]CC_conj c[*]c). apply bin_op_wd_unfolded. exact H. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (c[*] (c[*]CC_conj c)). apply mult_commutes. apply eq_transitive_unfolded with (c[*]c[*]CC_conj c). apply mult_assoc_unfolded. apply bin_op_wd_unfolded. apply eq_symmetric_unfolded. apply nexp_two. apply eq_reflexive_unfolded. cut (forall (G : CGroup) (x y : G), x[-]y [=] [0] -> x [=] y); intros. apply H1. assumption. apply eq_transitive_unfolded with (x[+][0]). apply eq_symmetric_unfolded. apply cm_rht_unit_unfolded. apply eq_transitive_unfolded with (x[+] ( [--]y[+]y)). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply cg_lft_inv_unfolded. apply eq_transitive_unfolded with (x[+][--]y[+]y). apply plus_assoc_unfolded. apply eq_transitive_unfolded with ([0][+]y). apply bin_op_wd_unfolded. exact H1. apply eq_reflexive_unfolded. apply cm_lft_unit_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing