proposition: Theorem Ppow_plus: forall a z1 z2, Ppow a (z1 + z2) = ((Ppow a z1) * (Ppow a z2))%positive.
proof: Proof. intros a z1 z2. assert (tmp: forall x y, Zpos x = Zpos y -> x = y). intros x y H; injection H; auto. apply tmp. rewrite Zpos_mult_morphism; repeat rewrite Ppow_correct. rewrite Zpos_plus_distr; rewrite Zpower_exp; auto; red; simpl; intros; discriminate. Qed.
imports: ZArith Zpow_facts