proposition: Lemma group_power_mult : forall (g : G) (n m : ZZ), Equal (group_power G g (ring_mult n m)) (group_power G (group_power G g n) m).
proof: Proof. unfold group_power in |- *. intros g n m; try assumption. simpl in |- *. apply Trans with (Z_to_group_nat_fun g (ring_mult n m)); auto with algebra. apply Trans with (Z_to_group_nat_fun (Z_to_group_nat_fun g n) m); auto with algebra. unfold ring_mult in |- *; simpl in |- *. elim m. rewrite Zmult_0_r. apply Trans with (monoid_unit G); auto with algebra. elim n. intros p; try assumption. rewrite Zmult_0_l. apply Trans with (Z_to_group_nat_fun (monoid_unit G) (Zpos p)); auto with algebra. auto with algebra. intros p p0; try assumption. replace (Zneg p * Zpos p0)%Z with (- (Zpos p * Zpos p0))%Z. apply Trans with (Z_to_group_nat_fun (group_inverse G g) (Zpos p * Zpos p0)%Z); auto with algebra. apply Trans with (Z_to_group_nat_fun (Z_to_group_nat_fun (group_inverse G g) (Zpos p)) (Zpos p0)); auto with algebra. rewrite <- Zopp_mult_distr_l_reverse. auto with algebra. elim n. intros p; try assumption. rewrite Zmult_0_l. apply Trans with (Z_to_group_nat_fun (monoid_unit G) (Zneg p)); auto with algebra. intros p p0; try assumption. replace (Zpos p * Zneg p0)%Z with (- (Zpos p * Zpos p0))%Z. apply Trans with (Z_to_group_nat_fun (group_inverse G g) (Zpos p * Zpos p0)%Z); auto with algebra. apply Trans with (Z_to_group_nat_fun (group_inverse G (Z_to_group_nat_fun g (Zpos p))) (Zpos p0)); auto with algebra. apply Trans with (Z_to_group_nat_fun (Z_to_group_nat_fun (group_inverse G g) (Zpos p)) (Zpos p0)); auto with algebra. apply Z_to_group_nat_fun_comp; auto with algebra. apply Trans with (Z_to_group_nat_fun g (Zneg p)); auto with algebra. replace (Zpos p) with (- Zneg p)%Z. auto with algebra. auto with algebra. intros p p0; try assumption. replace (Zneg p * Zneg p0)%Z with (- (Zpos p * Zneg p0))%Z. replace (Zpos p * Zneg p0)%Z with (- (Zpos p * Zpos p0))%Z. replace (- - (Zpos p * Zpos p0))%Z with (Zpos p * Zpos p0)%Z. apply Trans with (Z_to_group_nat_fun (Z_to_group_nat_fun g (Zpos p)) (Zpos p0)); auto with algebra. apply Trans with (Z_to_group_nat_fun (group_inverse G (Z_to_group_nat_fun g (Zneg p))) (Zpos p0)); auto with algebra. apply Z_to_group_nat_fun_comp; auto with algebra. apply Trans with (group_power G g (Zpos p)); auto with algebra. apply Trans with (group_inverse G (group_power G g (Zneg p))); auto with algebra. apply Sym. apply GROUP_law_inverse. apply Trans with (group_power G g (Zneg p + Zpos p)%Z); auto with algebra. replace (Zneg p) with (- Zpos p)%Z. rewrite Zplus_opp_l. auto with algebra. auto with algebra. rewrite Zopp_involutive; auto with algebra. replace (Zneg p0) with (- Zpos p0)%Z. replace (Zpos p * - Zpos p0)%Z with (- Zpos p0 * Zpos p)%Z. rewrite Zopp_mult_distr_l_reverse. rewrite Zmult_comm. auto with algebra. rewrite Zmult_comm. auto with algebra. auto with algebra. replace (Zneg p) with (- Zpos p)%Z. rewrite Zopp_mult_distr_l_reverse. auto with algebra. auto with algebra. apply Trans with (Z_to_group_nat_fun (Z_to_group_fun g n) m); auto with algebra. Qed.
imports: Z_group