proposition: Theorem Ppow_correct: forall a z, Zpos (Ppow a z) = (Zpos a) ^ (Zpos z).
proof: Proof. intros a z; elim z; simpl Ppow; auto; try (intros z1 Hrec; repeat rewrite Zpos_mult_morphism; rewrite Hrec). rewrite Zpos_xI; rewrite Zpower_exp. 3: auto with zarith. 2: rewrite <-Zpos_xO; red; simpl; intros; discriminate. rewrite Zpower_1_r; rewrite (Zmult_comm 2); try rewrite Zpower_mult by auto with zarith. change 2 with (1 + 1); rewrite Zpower_exp by auto with zarith. rewrite Zpower_1_r; rewrite Zmult_comm; auto. rewrite Zpos_xO; rewrite (Zmult_comm 2); rewrite Zpower_mult by auto with zarith. change 2 with (1 + 1); rewrite Zpower_exp by auto with zarith. rewrite Zpower_1_r; auto. rewrite Zpower_1_r; auto. Qed.
imports: ZArith Zpow_facts