proposition: Theorem ppow_add: forall n m p, 0 <= m -> 0 <= p -> ppow n (m + p) = pmult (ppow n m) (ppow n p).
proof: Proof. intros n m; case m; clear m. intros p _ _; rewrite ppow_0; rewrite pmult_1_l; auto. 2: intros p m H; contradict H; auto with zarith. intros p1 m _; case m. intros _; rewrite Zplus_0_r; simpl; apply sym_equal; apply pmult_1_r. 2: intros p2 H; contradict H; auto with zarith. intros p2 _; simpl. rewrite iter_pos_plus. rewrite ppow_op; auto. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup