proposition: Theorem ppow_ppow: forall n m p, 0 <= n -> 0 <= m -> ppow p (n * m ) = ppow (ppow p n) m.
proof: Proof. intros n m; case n. intros p _ Hm; rewrite Zmult_0_l. rewrite ppow_0; apply sym_equal; apply ppow_1. 2: intros p p1 H; contradict H; auto with zarith. intros p1 p _; case m; simpl; auto. intros p2 _; pattern p2; apply Pind; simpl; auto. rewrite Pmult_1_r; rewrite pmult_1_r; auto. intros p3 Rec; rewrite Pplus_one_succ_r; rewrite Pmult_plus_distr_l. rewrite Pmult_1_r. simpl; repeat rewrite iter_pos_plus; simpl. rewrite pmult_1_r. rewrite ppow_op; try rewrite Rec; auto. apply sym_equal; apply ppow_op; auto. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup