proposition: Lemma Cpow_mul : forall z n m, z ^ (n * m) = (z ^ n) ^ m.
proof: Proof. intros z n m ; induction m. rewrite Nat.mul_0_r ; reflexivity. simpl ; rewrite <- IHm ; rewrite <- Cpow_add ; replace (n * S m)%nat with (n + n * m)%nat by ring ; reflexivity. Qed.
imports: Cbase