proposition: Lemma C_power_theory : power_theory C1 Cmult (eq (A:=C)) nat_of_N Cpow.
proof: Proof. constructor. intros z n ; elim n ; clear n. reflexivity. induction p ; simpl in *. rewrite ZL6 ; rewrite Cpow_add ; rewrite IHp ; reflexivity. unfold nat_of_P ; rewrite <- IHp ; rewrite <- Cpow_add ; rewrite <- ZL6 ; reflexivity. apply Cmult_1_r. Qed.
imports: Nnat Arith Ring Field Cbase Cpow