(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Automatic Coercions Import.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Z_group.
(** Title "Facts about powers." *)
Section Lemmas.
Variable G : GROUP.

Lemma Z_to_group_nat_eq_pos :
 forall (n : Z) (g : G), Equal (Z_to_group_nat_fun g n) (Z_to_group_fun g n).
(* Goal: forall (n : Z) (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g n) (@Z_to_group_fun G g n) *)
intros n g; try assumption.
apply Trans with (Ap (sgroup_map (monoid_sgroup_hom (Z_to_group_nat g))) n);
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (Zpos p)) (group_inverse G (group_power G g (Zneg p))) *)
(* Goal: @eq Z (Z.mul (Zpos p) (Zpos p0)) (Z.opp (Z.opp (Z.mul (Zpos p) (Zpos p0)))) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zpos p) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Sym.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_fun G g n) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group_nat G g))) n) *)
apply Z_to_group_fun_eq.
Qed.
Hint Resolve Z_to_group_nat_eq_pos: algebra.

Lemma Zopp1 : forall n : Z, (n < 0)%Z -> (- n > 0)%Z.
(* Goal: forall (n : Z) (_ : Z.gt n Z0), Z.lt (Z.opp n) Z0 *)
simple induction n.
(* Goal: forall _ : Z.gt Z0 Z0, Z.lt (Z.opp Z0) Z0 *)
(* Goal: forall (p : positive) (_ : Z.gt (Zpos p) Z0), Z.lt (Z.opp (Zpos p)) Z0 *)
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), Z.lt (Z.opp (Zneg p)) Z0 *)
intros H'; try assumption.
(* Goal: Z.lt (Z.opp Z0) Z0 *)
(* Goal: forall (p : positive) (_ : Z.gt (Zpos p) Z0), Z.lt (Z.opp (Zpos p)) Z0 *)
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), Z.lt (Z.opp (Zneg p)) Z0 *)
inversion H'.
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), Z.lt (Z.opp (Zneg p)) Z0 *)
intros p H'; try assumption.
(* Goal: Z.lt (Z.opp (Zneg p)) Z0 *)
replace 0%Z with (- (0))%Z.
(* Goal: Z.gt (Z.opp (Zneg p)) (Z.opp Z0) *)
(* Goal: @eq Z (Z.opp Z0) Z0 *)
apply Zlt_gt; auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), Z.lt (Z.opp (Zneg p)) Z0 *)
intros p H'; try assumption.
(* Goal: Z.lt (Z.opp (Zneg p)) Z0 *)
replace 0%Z with (- (0))%Z.
(* Goal: Z.gt (Z.opp (Zneg p)) (Z.opp Z0) *)
(* Goal: @eq Z (Z.opp Z0) Z0 *)
apply Zlt_gt; auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
Qed.
Hint Resolve Zopp1: algebra.

Lemma Zopp2 : forall n : Z, (n > 0)%Z -> (- n < 0)%Z.
(* Goal: forall (n : Z) (_ : Z.gt n Z0), Z.lt (Z.opp n) Z0 *)
simple induction n.
(* Goal: forall _ : Z.gt Z0 Z0, Z.lt (Z.opp Z0) Z0 *)
(* Goal: forall (p : positive) (_ : Z.gt (Zpos p) Z0), Z.lt (Z.opp (Zpos p)) Z0 *)
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), Z.lt (Z.opp (Zneg p)) Z0 *)
intros H'; try assumption.
(* Goal: Z.lt (Z.opp Z0) Z0 *)
(* Goal: forall (p : positive) (_ : Z.gt (Zpos p) Z0), Z.lt (Z.opp (Zpos p)) Z0 *)
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), Z.lt (Z.opp (Zneg p)) Z0 *)
inversion H'.
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), Z.lt (Z.opp (Zneg p)) Z0 *)
intros p H'; try assumption.
(* Goal: Z.lt (Z.opp (Zneg p)) Z0 *)
replace 0%Z with (- (0))%Z.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Zgt_lt; auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), Z.lt (Z.opp (Zneg p)) Z0 *)
intros p H'; try assumption.
(* Goal: Z.lt (Z.opp (Zneg p)) Z0 *)
replace 0%Z with (- (0))%Z.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Zgt_lt; auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
Qed.
Hint Resolve Zopp2: algebra.

Lemma pos_abs_comp :
 forall (x : Z) (p p' : (x > 0)%Z), pos_abs p = pos_abs p'.
(* Goal: forall (x : Z) (p p' : Z.gt x Z0), @eq positive (@pos_abs x p) (@pos_abs x p') *)
intros x; try assumption.
(* Goal: forall p p' : Z.gt x Z0, @eq positive (@pos_abs x p) (@pos_abs x p') *)
elim x.
(* Goal: forall p p' : Z.gt Z0 Z0, @eq positive (@pos_abs Z0 p) (@pos_abs Z0 p') *)
(* Goal: forall (p : positive) (p0 p' : Z.gt (Zpos p) Z0), @eq positive (@pos_abs (Zpos p) p0) (@pos_abs (Zpos p) p') *)
(* Goal: forall (p : positive) (p0 p' : Z.gt (Zneg p) Z0), @eq positive (@pos_abs (Zneg p) p0) (@pos_abs (Zneg p) p') *)
intros p p'; try assumption.
(* Goal: @eq positive (@pos_abs (Zneg p) p0) (@pos_abs (Zneg p) p') *)
red in p'.
(* Goal: @eq positive (@pos_abs Z0 p) (@pos_abs Z0 p') *)
(* Goal: forall (p : positive) (p0 p' : Z.gt (Zpos p) Z0), @eq positive (@pos_abs (Zpos p) p0) (@pos_abs (Zpos p) p') *)
(* Goal: forall (p : positive) (p0 p' : Z.gt (Zneg p) Z0), @eq positive (@pos_abs (Zneg p) p0) (@pos_abs (Zneg p) p') *)
inversion p.
(* Goal: forall (p : positive) (p0 p' : Z.gt (Zpos p) Z0), @eq positive (@pos_abs (Zpos p) p0) (@pos_abs (Zpos p) p') *)
(* Goal: forall (p : positive) (p0 p' : Z.gt (Zneg p) Z0), @eq positive (@pos_abs (Zneg p) p0) (@pos_abs (Zneg p) p') *)
intros p p0 p'; simpl in |- *.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: forall (p : positive) (p0 p' : Z.gt (Zneg p) Z0), @eq positive (@pos_abs (Zneg p) p0) (@pos_abs (Zneg p) p') *)
intros p p0 p'; try assumption.
(* Goal: @eq positive (@pos_abs (Zneg p) p0) (@pos_abs (Zneg p) p') *)
red in p'.
(* Goal: @eq positive (@pos_abs (Zneg p) p0) (@pos_abs (Zneg p) p') *)
simpl in p'.
(* Goal: @eq positive (@pos_abs (Zneg p) p0) (@pos_abs (Zneg p) p') *)
inversion p'.
Qed.
Hint Resolve Zl2 Zl1 Zl3 nat_to_group_inverse: algebra.

Lemma nat_to_group_comp :
 forall (r r' : G) (n : nat),
 Equal r r' -> Equal (nat_to_group r n) (nat_to_group r' n).
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
simple induction n; simpl in |- *; auto with algebra.
Qed.
Hint Resolve nat_to_group_comp: algebra.

Lemma Z_to_group_nat_fun_comp :
 forall (r r' : G) (n : Z),
 Equal r r' -> Equal (Z_to_group_nat_fun r n) (Z_to_group_nat_fun r' n).
(* Goal: forall (r r' : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n : Z) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) r r'), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G r n) (@Z_to_group_nat_fun G r' n) *)
intros r r' n H'; try assumption.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) (Zneg p)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
elim n.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Trans with (monoid_unit G); auto with algebra.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul Z0 (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g Z0) (Zneg p)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zpos p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p; try assumption.
apply Trans with (nat_to_group r (nat_of_P (pos_abs (ax3 p))));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply Trans with (nat_to_group r' (nat_of_P (pos_abs (ax3 p))));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul Z0 (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g Z0) (Zneg p)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zpos p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p; try assumption.
apply
 Trans with (group_inverse G (nat_to_group r (nat_of_P (pos_abs (ax3 p)))));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply
 Trans with (group_inverse G (nat_to_group r' (nat_of_P (pos_abs (ax3 p)))));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve Z_to_group_nat_fun_comp: algebra.

Lemma Z_to_group_nat_neg :
 forall (p : positive) (r : G),
 Equal (Z_to_group_nat_fun r (Zneg p))
   (Z_to_group_nat_fun (group_inverse G r) (Zpos p)).
(* Goal: forall (p : positive) (r : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G r (Zpos p)) (@Z_to_group_nat_fun G (group_inverse G r) (Zneg p)) *)
intros p r; try assumption.
apply
 Trans with (group_inverse G (nat_to_group r (nat_of_P (pos_abs (ax3 p)))));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply
 Trans with (nat_to_group (group_inverse G r) (nat_of_P (pos_abs (ax3 p))));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve Z_to_group_nat_neg: algebra.

Lemma Z_to_group_nat_inv :
 forall (n : Z) (r : G),
 Equal (Z_to_group_nat_fun r (- n)%Z)
   (Z_to_group_nat_fun (group_inverse G r) n).
(* Goal: forall (n : Z) (r : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G r (Z.opp n)) (@Z_to_group_nat_fun G (group_inverse G r) n) *)
simple induction n; simpl in |- *.
(* Goal: forall r : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G r Z0) (@Z_to_group_nat_fun G (group_inverse G r) Z0) *)
(* Goal: forall (p : positive) (r : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G r (Zneg p)) (@Z_to_group_nat_fun G (group_inverse G r) (Zpos p)) *)
(* Goal: forall (p : positive) (r : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G r (Zpos p)) (@Z_to_group_nat_fun G (group_inverse G r) (Zneg p)) *)
intros r; try assumption.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Trans with (monoid_unit G); auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: forall (p : positive) (r : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G r (Zpos p)) (@Z_to_group_nat_fun G (group_inverse G r) (Zneg p)) *)
intros p r; try assumption.
apply
 Trans
  with (Z_to_group_nat_fun (group_inverse G (group_inverse G r)) (Zpos p));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve Z_to_group_nat_inv: algebra.

Lemma nat_to_group_mult :
 forall (r : G) (n m : nat),
 Equal (nat_to_group r (n * m)) (nat_to_group (nat_to_group r n) m).
(* Goal: forall (r : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n m : nat), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@nat_to_group G r (Init.Nat.mul n m)) (@nat_to_group G (@nat_to_group G r n) m) *)
simple induction m; simpl in |- *.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite mult_comm; simpl in |- *; auto with algebra.
(* Goal: forall (n : nat) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@nat_to_group G (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) n) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (@nat_to_group G (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) n) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros n0 H'; try assumption.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite mult_comm; simpl in |- *; auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
simpl in |- *.
apply Trans with (sgroup_law G (nat_to_group r n) (nat_to_group r (n0 * n)));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply Trans with (sgroup_law G (nat_to_group r (n0 * n)) (nat_to_group r n));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply SGROUP_comp; auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite mult_comm; simpl in |- *; auto with algebra.
Qed.
Hint Resolve nat_to_group_mult: algebra.

Lemma nat_to_group_unit :
 forall n : nat, Equal (nat_to_group (monoid_unit G) n) (monoid_unit G).
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
simple induction n; simpl in |- *; auto with algebra.
(* Goal: forall (n : nat) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@nat_to_group G (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) n) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (@nat_to_group G (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) n) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros n0 H'; try assumption.
apply Trans with (sgroup_law G (monoid_unit G) (monoid_unit G));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve nat_to_group_unit: algebra.

Lemma Z_to_group_nat_unit :
 forall n : Z, Equal (Z_to_group_nat_fun (monoid_unit G) n) (monoid_unit G).
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
simple induction n; simpl in |- *; auto with algebra.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul Z0 (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g Z0) (Zneg p)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zpos p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p; try assumption.
apply Trans with (nat_to_group (monoid_unit G) (nat_of_P (pos_abs (ax3 p))));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul Z0 (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g Z0) (Zneg p)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zpos p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p; try assumption.
apply
 Trans
  with
    (group_inverse G
       (nat_to_group (monoid_unit G) (nat_of_P (pos_abs (ax3 p)))));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Trans with (group_inverse G (monoid_unit G)); auto with algebra.
Qed.
Hint Resolve Z_to_group_nat_unit: algebra.

Lemma group_power_plus :
 forall (g : G) (n m : ZZ),
 Equal (group_power G g (sgroup_law ZZ n m))
   (sgroup_law G (group_power G g n) (group_power G g m)).
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
unfold group_power in |- *; auto with algebra.
Qed.
Hint Resolve group_power_plus: algebra.

Lemma group_power_S :
 forall (g : G) (n : ZZ),
 Equal (group_power G g (sgroup_law ZZ n (ring_unit ZZ)))
   (sgroup_law G (group_power G g n) g).
(* Goal: forall (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n m : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (group_power G (group_power G g n) m) *)
unfold group_power in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
simpl in |- *.
(* Goal: forall (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (group_inverse (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))) n)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (group_inverse G g)))) n) *)
intros g n; try assumption.
apply
 Trans
  with (sgroup_law G (Z_to_group_fun g n) (Z_to_group_fun g (ring_unit Zr)));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve group_power_S: algebra.

Lemma group_power_0 :
 forall g : G, Equal (group_power G g (monoid_unit ZZ)) (monoid_unit G).
(* Goal: forall (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n m : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (group_power G (group_power G g n) m) *)
unfold group_power in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
simpl in |- *.
(* Goal: forall g : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (ring_unit (cring_ring (idomain_ring ZZ)))) g *)
intros g; try assumption.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Trans with (Z_to_group_nat_fun g 0%Z); auto with algebra.
Qed.
Hint Resolve group_power_0: algebra.

Lemma group_power_1 : forall g : G, Equal (group_power G g (ring_unit ZZ)) g.
(* Goal: forall g : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (ring_unit (cring_ring (idomain_ring ZZ)))) g *)
intros g; try assumption.
apply
 Trans with (group_power G g (sgroup_law ZZ (monoid_unit ZZ) (ring_unit ZZ)));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve group_power_1: algebra.

Lemma group_power_inv :
 forall (g : G) (n : ZZ),
 Equal (group_power G g (group_inverse ZZ n))
   (group_power G (group_inverse G g) n).
(* Goal: forall (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n m : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (group_power G (group_power G g n) m) *)
unfold group_power in |- *.
(* Goal: forall (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (group_inverse (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))) n)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (group_inverse G g)))) n) *)
intros g n; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
simpl in |- *.
apply Trans with (Z_to_group_nat_fun g (group_inverse ZZ n));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply Trans with (Z_to_group_nat_fun (group_inverse G g) n);
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve group_power_inv: algebra.

Lemma Z_group_nat_fun_mult_pos :
 forall (p q : positive) (g : G),
 Equal (Z_to_group_nat_fun g (Zpos p * Zpos q)%Z)
   (Z_to_group_nat_fun (Z_to_group_nat_fun g (Zpos p)) (Zpos q)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
simpl in |- *.
(* Goal: forall (p q : positive) (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Zpos (Pos.mul p q))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zpos q)) *)
intros p q g; try assumption.
apply
 Trans
  with
    (nat_to_group g
       (nat_of_P
          (pos_abs
             (ax3
                ((fun (x : positive) (_ : positive -> positive)
                    (y : positive) => (x * y)%positive) p
                   (fun y : positive => y) q))))); 
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply
 Trans
  with
    (nat_to_group (Z_to_group_nat_fun g (Zpos p))
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
       (nat_of_P (pos_abs (ax3 q)))); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
simpl in |- *.
rewrite
 (fun (x y : positive) (_ : positive -> positive) =>
  nat_of_P_mult_morphism x y).
apply Trans with (nat_to_group (nat_to_group g (nat_of_P p)) (nat_of_P q));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve Z_group_nat_fun_mult_pos: algebra.

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).
(* Goal: forall (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n m : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (group_power G (group_power G g n) m) *)
unfold group_power in |- *.
(* Goal: forall (g : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (n m : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
intros g n m; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
simpl in |- *.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
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);
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) (@ring_mult (cring_ring (idomain_ring ZZ)) n m)) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) (sgroup_set (monoid_sgroup (group_monoid G))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_sgroup (group_monoid G)) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))) (group_monoid G) (@Z_to_group G g))) n)))) m) *)
unfold ring_mult in |- *; simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n m)) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
elim m.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n Z0)) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) Z0) *)
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n (Zpos p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) (Zpos p)) *)
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) (Zneg p)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zmult_0_r.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Trans with (monoid_unit G); auto with algebra.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) (Zneg p)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
elim n.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul Z0 (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g Z0) (Zneg p)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zpos p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul Z0 (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g Z0) (Zneg p)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zpos p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zmult_0_l.
apply Trans with (Z_to_group_nat_fun (monoid_unit G) (Zpos p));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p p0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zpos p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zpos p0)) *)
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) (Zneg p)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
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);
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply
 Trans
  with
    (Z_to_group_nat_fun (Z_to_group_nat_fun (group_inverse G g) (Zpos p))
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
       (Zpos p0)); auto with algebra.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zneg p) (Zpos p0)) *)
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) (Zneg p)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite <- Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul n (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) (Zneg p)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
elim n.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul Z0 (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g Z0) (Zneg p)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zpos p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul Z0 (Zneg p))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g Z0) (Zneg p)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zpos p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zpos p)) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zmult_0_l.
apply Trans with (Z_to_group_nat_fun (monoid_unit G) (Zneg p));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p p0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.opp (Z.mul (Zpos p) (Zneg p0)))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
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);
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply
 Trans
  with
    (Z_to_group_nat_fun (group_inverse G (Z_to_group_nat_fun g (Zpos p)))
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
       (Zpos p0)); auto with algebra.
apply
 Trans
  with
    (Z_to_group_nat_fun (Z_to_group_nat_fun (group_inverse G g) (Zpos p))
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
       (Zpos p0)); auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Z_to_group_nat_fun_comp; auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Trans with (Z_to_group_nat_fun g (Zneg p)); auto with algebra.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zpos p) (Zneg p0)) *)
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
replace (Zpos p) with (- Zneg p)%Z.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
intros p p0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.mul (Zneg p) (Zneg p0))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
replace (Zneg p * Zneg p0)%Z with (- (Zpos p * Zneg p0))%Z.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.opp (Z.mul (Zpos p) (Zneg p0)))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
replace (Zpos p * Zneg p0)%Z with (- (Zpos p * Zpos p0))%Z.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G g (Z.opp (Z.opp (Z.mul (Zpos p) (Zpos p0))))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g (Zneg p)) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zpos p) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
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));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
apply
 Trans
  with
    (Z_to_group_nat_fun (group_inverse G (Z_to_group_nat_fun g (Zneg p)))
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
       (Zpos p0)); auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Z_to_group_nat_fun_comp; auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Trans with (group_power G g (Zpos p)); auto with algebra.
apply Trans with (group_inverse G (group_power G g (Zneg p)));
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (Zpos p)) (group_inverse G (group_power G g (Zneg p))) *)
(* Goal: @eq Z (Z.mul (Zpos p) (Zpos p0)) (Z.opp (Z.opp (Z.mul (Zpos p) (Zpos p0)))) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zpos p) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Sym.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (group_power G g (Zneg p))) (group_power G g (Zpos p)) *)
(* Goal: @eq Z (Z.mul (Zpos p) (Zpos p0)) (Z.opp (Z.opp (Z.mul (Zpos p) (Zpos p0)))) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zpos p) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply GROUP_law_inverse.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
apply Trans with (group_power G g (Zneg p + Zpos p)%Z); auto with algebra.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
replace (Zneg p) with (- Zpos p)%Z.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g (Z.add (Z.opp (Zpos p)) (Zpos p))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @eq Z (Z.mul (Zpos p) (Zpos p0)) (Z.opp (Z.opp (Z.mul (Zpos p) (Zpos p0)))) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zpos p) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zplus_opp_l.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zopp_involutive; auto with algebra.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zpos p) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
replace (Zneg p0) with (- Zpos p0)%Z.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zpos p0))) (Z.mul (Zpos p) (Z.opp (Zpos p0))) *)
(* Goal: @eq Z (Z.opp (Zpos p0)) (Zneg p0) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
replace (Zpos p * - Zpos p0)%Z with (- Zpos p0 * Zpos p)%Z.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Z.opp (Zpos p)) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.mul (Z.opp (Zpos p0)) (Zpos p)) (Z.mul (Zpos p) (Z.opp (Zpos p0))) *)
(* Goal: @eq Z (Z.opp (Zpos p0)) (Zneg p0) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zmult_comm.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: @eq Z (Z.mul (Z.opp (Zpos p0)) (Zpos p)) (Z.mul (Zpos p) (Z.opp (Zpos p0))) *)
(* Goal: @eq Z (Z.opp (Zpos p0)) (Zneg p0) *)
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zmult_comm.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Zneg p) (Zneg p0)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
replace (Zneg p) with (- Zpos p)%Z.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos p) (Zneg p0))) (Z.mul (Z.opp (Zpos p)) (Zneg p0)) *)
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
auto with algebra.
apply Trans with (Z_to_group_nat_fun (Z_to_group_fun g n) m);
(* Goal: @eq Z (Z.opp (Zpos p)) (Zneg p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@Z_to_group_nat_fun G (@Z_to_group_nat_fun G g n) m) (@Z_to_group_fun G (@Z_to_group_fun G g n) m) *)
 auto with algebra.
Qed.
Hint Resolve group_power_mult: algebra.
End Lemmas.
Hint Resolve group_power_plus group_power_S group_power_0 group_power_1
  group_power_inv group_power_mult: algebra.
