proposition: Lemma Cpow_mul_distr_l : forall z1 z2 n, (z1 * z2) ^ n = z1 ^ n * z2 ^ n.
proof: Proof. intros z1 z2 n; induction n. simpl; CusingR_f. repeat rewrite Cpow_S; rewrite IHn. rewrite Cmult_assoc. rewrite <- (Cmult_assoc (z2 ^ n) z1 z2). rewrite (Cmult_comm (z2 ^ n) z1). repeat rewrite Cmult_assoc. reflexivity. Qed.
imports: Cbase