proposition: Lemma nrootCC_1_lower : b [<] [0] -> (a'[+I*][--]b') [^]2 [=] a[+I*]b.
proof: Proof. intros. cut (a'[^]2[-][--]b'[^]2 [=] a); intros. cut (a'[*][--]b'[*]Two [=] b); intros. apply eq_transitive_unfolded with ((a'[^]2[-][--]b'[^]2) [+I*]a'[*][--]b'[*]Two). apply cc_calculate_square. apply I_wd. rename H0 into H1. rename H into H0. rename X into H. exact H0. rename H0 into H1. rename H into H0. rename X into H. exact H1. apply eq_transitive_unfolded with (b[*]Half[*]Two). apply bin_op_wd_unfolded. apply nrCC1_a7_lower. rename H into H0. rename X into H. exact H. apply eq_reflexive_unfolded. apply half_1'. apply eq_transitive_unfolded with (a'[^]2[-]b'[^]2). apply cg_minus_wd. apply eq_reflexive_unfolded. apply inv_nexp_two. exact nrCC1_a3. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing