proposition: Lemma nrCC_5a3 : forall (n : nat) (z : CC), (z[^]2) [^]n [=] z[^]Nat.double n.
proof: Proof. intros. apply eq_transitive_unfolded with (z[^] (2 * n)). apply nexp_mult. rewrite <- nrCC_5a2. apply eq_reflexive_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing