proposition: Theorem gpow_gpow: forall (A : Set) (op : A -> A -> A) (a : A) (G : FGroup op), In a (s G) -> forall n m, 0 <= n -> 0 <= m -> gpow a G (n * m ) = gpow (gpow a G n) G m.
proof: Proof. intros A op a G H n m; case n. simpl; intros _ H1; generalize H1. pattern m; apply natlike_ind; simpl; auto. intros x H2 Rec _; unfold Z.succ; rewrite gpow_add; simpl; auto with zarith. repeat rewrite G.(e_is_zero_r); auto with zarith. apply gpow_in; sauto. intros p1 _; case m; simpl; auto. assert(H1: In (iter_pos A (op a) (e G) p1) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p1)); auto. intros p2 _; pattern p2; apply Pind; simpl; auto. rewrite Pmult_1_r; rewrite G.(e_is_zero_r); try rewrite G.(e_is_zero_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 G.(e_is_zero_r); auto. rewrite gpow_op with (G:= G); try rewrite Rec; auto. apply sym_equal; apply gpow_op; auto. intros p Hp; contradict Hp; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange