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