proposition: Lemma nrCC4_a6 : (x[^]2[+]y[^]2) [^]n [=] a[^]2[+]b[^]2.
proof: Proof. unfold x in |- *. unfold nrCC4_x in |- *. cut ((y[*]r) [^]2[+]y[^]2 [=] y[^]2[*] (r[^]2[+][1])). intro. apply eq_transitive_unfolded with ((y[^]2[*] (r[^]2[+][1])) [^]n). apply un_op_wd_unfolded. exact H. cut (y[^]2 [=] y2). intro. apply eq_transitive_unfolded with ((y2[*] (r[^]2[+][1])) [^]n). apply un_op_wd_unfolded. apply bin_op_wd_unfolded. exact H0. apply eq_reflexive_unfolded. exact y2_property. unfold y in |- *. unfold nrCC4_y in |- *. apply sqrt_sqr. apply eq_transitive_unfolded with (y[^]2[*]r[^]2[+]y[^]2[*][1]). apply bin_op_wd_unfolded. apply mult_nexp. apply eq_symmetric_unfolded. apply mult_one. apply eq_symmetric_unfolded. apply ring_dist_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing