proposition: Lemma cc_pow_abs : forall (x : CC) (n : nat), AbsCC (x[^]n) [=] AbsCC x[^]n.
proof: Proof. intros. induction n as [| n Hrecn]; intros. simpl in |- *. apply AbsCC_one. simpl in |- *. Step_final (AbsCC (x[^]n) [*]AbsCC x). Qed.
imports: CoRN.complex.CComplex