proposition: Theorem ppow_op: forall a b p, iter_pos _ (pmult a) b p = pmult (iter_pos _ (pmult a) (1, 0) p) b.
proof: Proof. intros a b p; generalize b; elim p; simpl; auto; clear b p. intros p Rec b. rewrite (Rec b). try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto. repeat rewrite pmult_assoc; auto. intros p Rec b. rewrite (Rec b); try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto. repeat rewrite pmult_assoc; auto. intros b; rewrite pmult_1_r; auto. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup