proposition: Lemma nrootCC_1_ap_imag : {z : CC | z[^]2 [=] a[+I*]b}.
proof: Proof. elim (nrootCC_1_ap_real a' b'). intros x H. exists (x[*]sqrt_I). apply eq_transitive_unfolded with (x[^]2[*]sqrt_I[^]2). apply mult_nexp. Hint Resolve sqrt_I_nexp: algebra. apply eq_transitive_unfolded with ((a'[+I*]b') [*]II). apply bin_op_wd_unfolded. exact H. exact sqrt_I_nexp. apply eq_transitive_unfolded with ((a[+I*]b) [*][--]II[*]II). apply eq_reflexive_unfolded. apply eq_transitive_unfolded with ((a[+I*]b) [*] ( [--]II[*]II)). apply eq_symmetric_unfolded. apply mult_assoc_unfolded. apply eq_transitive_unfolded with ((a[+I*]b) [*][1]). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. exact I_recip_lft. apply mult_one. cut (b[+I*][--]a [=] c'); intros. apply ap_wdl_unfolded with (Im c'). 2: apply eq_reflexive_unfolded. apply ap_wdl_unfolded with (Im (b[+I*][--]a)). 2: apply Im_wd. 2: exact H. apply ap_wdl_unfolded with ( [--]a). apply zero_minus_apart. apply minus_ap_zero. apply inv_resp_ap_zero. exact a_. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with ( [--][--]b[+I*][--]a). apply I_wd. apply eq_symmetric_unfolded. apply cg_inv_inv. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with ( [--] ( [--]b[+I*]a)). apply eq_reflexive_unfolded. apply eq_transitive_unfolded with ( [--] ((a[+I*]b) [*]II)). apply un_op_wd_unfolded. apply eq_symmetric_unfolded. apply mult_I. apply eq_transitive_unfolded with ((a[+I*]b) [*][--]II). apply eq_symmetric_unfolded. apply cring_inv_mult_lft. apply eq_reflexive_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing