proposition: Lemma nrCC4_a8 : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c.
proof: Proof. unfold z in |- *. unfold nrCC4_z in |- *. unfold c in |- *. apply eq_transitive_unfolded with (cc_IR (x[^]2[+]y[^]2) [^]n). apply un_op_wd_unfolded. apply calculate_norm. apply eq_transitive_unfolded with (cc_IR ((x[^]2[+]y[^]2) [^]n)). apply cc_IR_nexp. Hint Resolve nrCC4_a6: algebra. apply eq_transitive_unfolded with (cc_IR (a[^]2[+]b[^]2)). apply cc_IR_wd. exact nrCC4_a6. apply eq_symmetric_unfolded. apply calculate_norm. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing