proposition: Lemma Cpow_add : forall (z : C) (n m : nat), z ^ (n + m) = z ^ n * z ^ m.
proof: Proof. intros z n m. induction n. auto with complex. replace (z ^ (S n + m)%nat) with (z * z ^ (n+m)%nat). rewrite IHn. replace (z ^ S n) with (z * (z ^ n)). auto with complex. destruct n ; simpl ; auto with complex. replace (S n + m)%nat with (S (n + m))%nat. destruct n; destruct m ; simpl ; auto with complex. simpl ; reflexivity. Qed.
imports: Cbase