proposition: Theorem gpow_mult: forall (A : Set) (op : A -> A -> A) (a b: A) (G : FGroup op) (comm: forall a b, In a (s G) -> In b (s G) -> op a b = op b a), In a (s G) -> In b (s G) -> forall n, 0 <= n -> gpow (op a b) G n = op (gpow a G n) (gpow b G n).
proof: Proof. intros A op a b G comm Ha Hb n; case n; simpl; auto. intros _; rewrite G.(e_is_zero_r); auto. 2: intros p Hp; contradict Hp; auto with zarith. intros p _; pattern p; apply Pind; simpl; auto. repeat rewrite G.(e_is_zero_r); auto. intros p3 Rec; rewrite Pplus_one_succ_r. repeat rewrite iter_pos_plus; simpl. repeat rewrite (fun x y H z => gpow_op A op x G H (op y z)) ; auto. rewrite Rec. repeat rewrite G.(e_is_zero_r); auto. assert(H1: In (iter_pos A (op a) (e G) p3) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p3)); auto. assert(H2: In (iter_pos A (op b) (e G) p3) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p3)); auto. repeat rewrite <- G.(assoc); try eq_tac; auto. rewrite (fun x y => comm (iter_pos A x y p3) b); auto. rewrite (G.(assoc) a); try apply comm; auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange