proposition: Theorem gpow_op: forall b p, In b G.(s) -> iter_pos _ (op a) b p = op (iter_pos _ (op a) G.(e) p) b.
proof: Proof. intros b p; generalize b; elim p; simpl; auto; clear b p. intros p Rec b Hb. assert (H: In (gpow (Zpos p)) G.(s)). apply gpow_in. rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos A x y p)); auto. repeat rewrite G.(assoc); auto. intros p Rec b Hb. assert (H: In (gpow (Zpos p)) G.(s)). apply gpow_in. rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos A x y p)); auto. repeat rewrite G.(assoc); auto. intros b H; rewrite e_is_zero_r; auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange