(* 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.
Unset Standard Proposition Elimination Names.
Require Export Zring.
Require Export Group_kernel.
(** Title "Universal property of integers." *)
Section Int_power.
Variable G : GROUP.
Set Strict Implicit.
Unset Implicit Arguments.

Definition group_square (x : G) : G := sgroup_law G x x.
Set Implicit Arguments.
Unset Strict Implicit.
End Int_power.
Section Zup1.
Variable G : GROUP.
Variable r : G.

Fixpoint nat_to_group (n : nat) : G :=
  match n with
  | O => monoid_unit G
  | S n' => sgroup_law G (nat_to_group n') r
  end.

Definition pos_abs : forall x : Z, (x > 0)%Z -> positive.
(* Goal: forall (x : Z) (px : Z.gt x Z0), @eq Z x (Zpos (@pos_abs x px)) *)
intros x; try assumption.
(* Goal: forall _ : Z.gt x Z0, positive *)
case x.
(* Goal: forall _ : Z.gt Z0 Z0, positive *)
(* Goal: forall (p : positive) (_ : Z.gt (Zpos p) Z0), positive *)
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), positive *)
intros H'; red in H'.
(* Goal: @eq Z (Z.add (Zpos p) (Zneg q)) (Zneg (Pos.sub q p)) *)
simpl in H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
inversion H'.
(* Goal: forall (p : positive) (_ : Z.gt (Zpos p) Z0), positive *)
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), positive *)
intros p H'.
(* Goal: positive *)
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), positive *)
exact p.
(* Goal: forall (p : positive) (_ : Z.gt (Zneg p) Z0), positive *)
intros p H'; red in H'.
(* Goal: @eq Z (Z.add (Zpos p) (Zneg q)) (Zneg (Pos.sub q p)) *)
simpl in H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
inversion H'.
Defined.

Lemma pos_abs_ok : forall (x : Z) (px : (x > 0)%Z), x = Zpos (pos_abs px).
(* Goal: forall (x : Z) (px : Z.gt x Z0), @eq Z x (Zpos (@pos_abs x px)) *)
intros x; try assumption.
(* Goal: forall px : Z.gt x Z0, @eq Z x (Zpos (@pos_abs x px)) *)
elim x.
(* Goal: forall px : Z.gt Z0 Z0, @eq Z Z0 (Zpos (@pos_abs Z0 px)) *)
(* Goal: forall (p : positive) (px : Z.gt (Zpos p) Z0), @eq Z (Zpos p) (Zpos (@pos_abs (Zpos p) px)) *)
(* Goal: forall (p : positive) (px : Z.gt (Zneg p) Z0), @eq Z (Zneg p) (Zpos (@pos_abs (Zneg p) px)) *)
intros px; red in px.
(* Goal: @eq Z (Zneg p) (Zpos (@pos_abs (Zneg p) px)) *)
simpl in px.
(* Goal: @eq Z (Zneg p) (Zpos (@pos_abs (Zneg p) px)) *)
inversion px.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: forall (p : positive) (px : Z.gt (Zneg p) Z0), @eq Z (Zneg p) (Zpos (@pos_abs (Zneg p) px)) *)
intros p px; red in px.
(* Goal: @eq Z (Zneg p) (Zpos (@pos_abs (Zneg p) px)) *)
simpl in px.
(* Goal: @eq Z (Zneg p) (Zpos (@pos_abs (Zneg p) px)) *)
inversion px.
Qed.

Lemma Zlt_reg_l : forall a b c : Z, (a < b)%Z -> (c + a < c + b)%Z.
(* Goal: forall (a b c : Z) (_ : Z.lt a b), Z.lt (Z.add c a) (Z.add c b) *)
intros a b c; try assumption.
(* Goal: forall _ : Z.lt a b, Z.lt (Z.add c a) (Z.add c b) *)
unfold Zlt, not in |- *.
(* Goal: forall _ : @eq Z (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
rewrite <- H'.
(* Goal: @eq comparison (Z.compare (Z.add c a) (Z.add c b)) (Z.compare a b) *)
apply Zcompare_plus_compat; assumption.
Qed.

Lemma Zlemma1 : forall x : Z, (x < 0)%Z -> (- x > 0)%Z.
(* Goal: forall (x : Z) (_ : Z.lt x Z0), Z.gt (Z.opp x) Z0 *)
intros x H'; try assumption.
(* Goal: Z.gt (Z.opp x) Z0 *)
apply Zlt_gt.
(* Goal: Z.lt Z0 (Z.opp x) *)
replace (- x)%Z with (- x + 0)%Z.
(* Goal: Z.lt Z0 (Z.add (Z.opp x) Z0) *)
(* Goal: @eq Z (Z.add (Z.opp x) Z0) (Z.opp x) *)
pattern 0%Z at 1 in |- *.
(* Goal: (fun z : Z => Z.lt z (Z.add (Z.opp x) Z0)) Z0 *)
(* Goal: @eq Z (Z.add (Z.opp x) Z0) (Z.opp x) *)
replace 0%Z with (- x + x)%Z.
(* Goal: Z.lt (Z.add (Z.opp x) x) (Z.add (Z.opp x) Z0) *)
(* Goal: @eq Z (Z.add (Z.opp x) x) Z0 *)
(* Goal: @eq Z (Z.add (Z.opp x) Z0) (Z.opp x) *)
apply Zlt_reg_l.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: @eq Z (Z.add (Z.opp x) x) Z0 *)
(* Goal: @eq Z (Z.add (Z.opp x) Z0) (Z.opp x) *)
apply Zplus_opp_l.
(* Goal: @eq Z (Z.add (Z.opp x) Z0) (Z.opp x) *)
apply Zplus_0_r.
Qed.
Comments "The powers of" r ".".

Definition Z_to_group_nat_fun : ZZ -> G.
(* Goal: forall _ : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))), Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
intros x.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
case (Z_gt_le_dec x 0); intros z.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
exact (nat_to_group (nat_of_P (pos_abs z))).
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
case (Z_le_lt_eq_dec _ _ z); intros.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
cut (- x > 0)%Z.
(* Goal: forall _ : Z.gt (Z.opp x) Z0, Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
intros H'.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
exact (group_inverse G (nat_to_group (nat_of_P (pos_abs H')))).
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
apply Zlemma1.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
exact (monoid_unit G).
Defined.

Lemma nat_to_group_com :
 forall n : nat,
 Equal (sgroup_law G (nat_to_group n) r) (sgroup_law G r (nat_to_group n)).
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
simple induction n; simpl in |- *; auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with r; auto with *.
(* Goal: forall (n : nat) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) (group_inverse G r)) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G r) (nat_to_group n))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r) (group_inverse G r)) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G r) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r)) *)
intros n0 H'; try assumption.
apply Trans with (sgroup_law G (sgroup_law G r (nat_to_group n0)) r);
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
Qed.
Hint Resolve nat_to_group_com: algebra.

Lemma nat_to_group_add :
 forall n m : nat,
 Equal (nat_to_group (n + m))
   (sgroup_law G (nat_to_group n) (nat_to_group m)).
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simple induction n; simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: forall (n : nat) (_ : forall m : nat, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (nat_to_group n))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (nat_to_group n)) (nat_to_group m))) (m : nat), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r)) (nat_to_group m)) *)
intros n0 H' m; try assumption.
apply
 Trans
  with (sgroup_law G (nat_to_group n0) (sgroup_law G r (nat_to_group m)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with (sgroup_law G (nat_to_group n0) (sgroup_law G (nat_to_group m) r));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with (sgroup_law G (sgroup_law G (nat_to_group n0) (nat_to_group m)) r);
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
Qed.
Hint Resolve nat_to_group_add: algebra.

Lemma ax1 : ~ (0 > 0)%Z.
(* Goal: gt (Pos.to_nat q) (Pos.to_nat p) *)
red in |- *.
(* Goal: forall _ : @eq Z (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
intros H'; try assumption.
(* Goal: False *)
red in H'.
(* Goal: @eq Z (Z.add (Zpos p) (Zneg q)) (Zneg (Pos.sub q p)) *)
simpl in H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
inversion H'.
Qed.
Hint Resolve ax1: algebra.

Lemma ax2 : ~ (0 < 0)%Z.
(* Goal: gt (Pos.to_nat q) (Pos.to_nat p) *)
red in |- *.
(* Goal: forall _ : @eq Z (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
intros H'; try assumption.
(* Goal: False *)
red in H'.
(* Goal: @eq Z (Z.add (Zpos p) (Zneg q)) (Zneg (Pos.sub q p)) *)
simpl in H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
inversion H'.
Qed.
Hint Resolve ax2: algebra.

Lemma Zl1 : Equal (Z_to_group_nat_fun 0%Z) (monoid_unit G).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec z Z0 with | left z0 => pos_to_group r (@pos_abs z z0) | right z0 => match Z_le_lt_eq_dec z Z0 z0 with | left l => pos_to_group (group_inverse G r) (@pos_abs (Z.opp z) (@Zlemma1 z l)) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end (@Z_to_group_nat_fun G r z) *)
unfold Z_to_group_nat_fun in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec Z0 Z0 with | left z => nat_to_group (Pos.to_nat (@pos_abs Z0 z)) | right z => match Z_le_lt_eq_dec Z0 Z0 z with | left l => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp Z0) (@Zlemma1 Z0 l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
case (Z_gt_le_dec 0 0).
(* Goal: forall l : Z.le (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec (ring_unit (cring_ring (idomain_ring ZZ))) Z0 l with | left l0 => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (ring_unit (cring_ring (idomain_ring ZZ)))) (@Zlemma1 (ring_unit (cring_ring (idomain_ring ZZ))) l0)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end r *)
intros z; try assumption.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
absurd (0 > 0)%Z; auto with *.
(* Goal: forall l : Z.le (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec (ring_unit (cring_ring (idomain_ring ZZ))) Z0 l with | left l0 => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (ring_unit (cring_ring (idomain_ring ZZ)))) (@Zlemma1 (ring_unit (cring_ring (idomain_ring ZZ))) l0)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end r *)
intros z; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec Z0 Z0 z with | left l => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp Z0) (@Zlemma1 Z0 l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
case (Z_le_lt_eq_dec 0 0 z).
(* Goal: forall l : Z.lt (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (ring_unit (cring_ring (idomain_ring ZZ)))) (@Zlemma1 (ring_unit (cring_ring (idomain_ring ZZ))) l))))) r *)
(* Goal: forall _ : @eq Z (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
intros z0; try assumption.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
absurd (0 < 0)%Z; auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Qed.
Hint Resolve Zl1: algebra.

Lemma ax3 : forall p : positive, (Zpos p > 0)%Z.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) Z0 (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun Z0) (Z_to_group_nat_fun (Zneg p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p; try assumption.
(* Goal: gt (Pos.to_nat q) (Pos.to_nat p) *)
red in |- *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Qed.
Hint Resolve ax3: algebra.

Lemma Zl2 :
 forall p : positive,
 Equal (Z_to_group_nat_fun (Zpos p))
   (nat_to_group (nat_of_P (pos_abs (ax3 p)))).
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) Z0 (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun Z0) (Z_to_group_nat_fun (Zneg p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec z Z0 with | left z0 => pos_to_group r (@pos_abs z z0) | right z0 => match Z_le_lt_eq_dec z Z0 z0 with | left l => pos_to_group (group_inverse G r) (@pos_abs (Z.opp z) (@Zlemma1 z l)) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end (@Z_to_group_nat_fun G r z) *)
unfold Z_to_group_nat_fun in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec (Zpos p) Z0 with | left z => nat_to_group (Pos.to_nat (@pos_abs (Zpos p) z)) | right z => match Z_le_lt_eq_dec (Zpos p) Z0 z with | left l => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (Zpos p)) (@Zlemma1 (Zpos p) l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end (nat_to_group (Pos.to_nat (@pos_abs (Zpos p) (ax3 p)))) *)
case (Z_gt_le_dec (Zpos p) 0); intros z.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
simpl in |- *; auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec (Zpos p) Z0 z with | left l => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (Zpos p)) (@Zlemma1 (Zpos p) l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end (nat_to_group (Pos.to_nat (@pos_abs (Zpos p) (ax3 p)))) *)
case (Z_le_lt_eq_dec (Zpos p) 0 z); intros.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
absurd (Zpos p < 0)%Z; auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Zpos p) (ax3 p))))) *)
inversion e.
Qed.
Hint Resolve Zl2: algebra.

Lemma ax4 : forall p : positive, ~ (Zneg p > 0)%Z.
(* Goal: gt (Pos.to_nat q) (Pos.to_nat p) *)
intros p; red in |- *.
(* Goal: forall _ : @eq Z (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
intros H'; try assumption.
(* Goal: False *)
red in H'.
(* Goal: @eq Z (Z.add (Zpos p) (Zneg q)) (Zneg (Pos.sub q p)) *)
simpl in H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
inversion H'.
Qed.
Hint Resolve ax4: algebra.

Lemma Zl3 :
 forall p : positive,
 Equal (Z_to_group_nat_fun (Zneg p))
   (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 p))))).
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) Z0 (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun Z0) (Z_to_group_nat_fun (Zneg p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec z Z0 with | left z0 => pos_to_group r (@pos_abs z z0) | right z0 => match Z_le_lt_eq_dec z Z0 z0 with | left l => pos_to_group (group_inverse G r) (@pos_abs (Z.opp z) (@Zlemma1 z l)) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end (@Z_to_group_nat_fun G r z) *)
unfold Z_to_group_nat_fun in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec (Zneg p) Z0 with | left z => nat_to_group (Pos.to_nat (@pos_abs (Zneg p) z)) | right z => match Z_le_lt_eq_dec (Zneg p) Z0 z with | left l => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (Zneg p)) (@Zlemma1 (Zneg p) l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end (group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Zpos p) (ax3 p))))) *)
case (Z_gt_le_dec (Zneg p) 0); intros z.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
absurd (Zneg p > 0)%Z; auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec (Zneg p) Z0 z with | left l => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (Zneg p)) (@Zlemma1 (Zneg p) l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end (group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Zpos p) (ax3 p))))) *)
case (Z_le_lt_eq_dec (Zneg p) 0 z); intros.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
simpl in |- *; auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Zpos p) (ax3 p))))) *)
inversion e.
Qed.
Hint Resolve Zl3: algebra.

Lemma ax5 :
 forall p q : positive,
 (Zpos p > Zpos q)%Z -> (Zpos p + Zneg q)%Z = Zpos (p - q).
(* Goal: False *)
intros p q H'; red in H'.
(* Goal: @eq Z (Z.add (Zpos p) (Zneg q)) (Zneg (Pos.sub q p)) *)
simpl in H'.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: @eq Z (Z.pos_sub p q) (Zneg (Pos.sub q p)) *)
rewrite Z.pos_sub_spec.
(* Goal: @eq Z match Pos.compare p q with | Eq => Z0 | Lt => Zneg (Pos.sub q p) | Gt => Zpos (Pos.sub p q) end (Zneg (Pos.sub q p)) *)
rewrite H'.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Qed.

Lemma ax6 :
 forall p q : positive,
 (Zpos p < Zpos q)%Z -> (Zpos p + Zneg q)%Z = Zneg (q - p).
(* Goal: False *)
intros p q H'; red in H'.
(* Goal: @eq Z (Z.add (Zpos p) (Zneg q)) (Zneg (Pos.sub q p)) *)
simpl in H'.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: @eq Z (Z.pos_sub p q) (Zneg (Pos.sub q p)) *)
rewrite Z.pos_sub_spec.
(* Goal: @eq Z match Pos.compare p q with | Eq => Z0 | Lt => Zneg (Pos.sub q p) | Gt => Zpos (Pos.sub p q) end (Zneg (Pos.sub q p)) *)
rewrite H'.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Qed.

Lemma ax7 : forall p : positive, (Zpos p + Zneg p)%Z = 0%Z.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) Z0 (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun Z0) (Z_to_group_nat_fun (Zneg p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: @eq Z (Z.pos_sub p p) Z0 *)
rewrite Z.pos_sub_spec; unfold Pos.compare.
(* Goal: @eq Z match Pos.compare_cont Eq p p with | Eq => Z0 | Lt => Zneg (Pos.sub p p) | Gt => Zpos (Pos.sub p p) end Z0 *)
replace (Pcompare p p Datatypes.Eq) with Datatypes.Eq.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: @eq comparison Eq (Pos.compare_cont Eq p p) *)
elim p.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
intros p0; simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
intros p0; simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Qed.
Hint Resolve ax7 ax6 ax5: algebra.

Lemma nat_to_group_com2 :
 forall n m : nat,
 Equal (sgroup_law G (nat_to_group n) (nat_to_group m))
   (sgroup_law G (nat_to_group m) (nat_to_group n)).
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
simple induction n; simpl in |- *; auto with *.
(* Goal: forall m : nat, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) (nat_to_group m)) *)
(* Goal: forall (n : nat) (_ : forall m : nat, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (nat_to_group n))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (nat_to_group n)) (nat_to_group m))) (m : nat), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r)) (nat_to_group m)) *)
intros m; try assumption.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (nat_to_group m); auto with *.
(* Goal: forall (n : nat) (_ : forall m : nat, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (nat_to_group n))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (nat_to_group n)) (nat_to_group m))) (m : nat), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r)) (nat_to_group m)) *)
intros n0 H' m; try assumption.
apply
 Trans
  with (sgroup_law G (nat_to_group n0) (sgroup_law G r (nat_to_group m)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with (sgroup_law G (nat_to_group n0) (sgroup_law G (nat_to_group m) r));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with (sgroup_law G (sgroup_law G (nat_to_group n0) (nat_to_group m)) r);
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with (sgroup_law G (sgroup_law G (nat_to_group m) (nat_to_group n0)) r);
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
Qed.
Hint Resolve nat_to_group_com2: algebra.

Lemma nat_to_group_minus :
 forall n m : nat,
 n > m ->
 Equal (nat_to_group (n - m))
   (sgroup_law G (nat_to_group n) (group_inverse G (nat_to_group m))).
(* Goal: forall (n m : nat) (_ : gt n m), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (nat_to_group (Init.Nat.sub n m)) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) (group_inverse G (nat_to_group m))) *)
intros n m H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (nat_to_group (Init.Nat.sub n m)) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) (group_inverse G (nat_to_group m))) *)
replace n with (m + (n - m)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (nat_to_group (Init.Nat.sub (Init.Nat.add m (Init.Nat.sub n m)) m)) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Init.Nat.add m (Init.Nat.sub n m))) (group_inverse G (nat_to_group m))) *)
(* Goal: @eq nat (Init.Nat.add m (Init.Nat.sub n m)) n *)
rewrite minus_plus.
apply
 Trans
  with
    (sgroup_law G (sgroup_law G (nat_to_group m) (nat_to_group (n - m)))
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
       (group_inverse G (nat_to_group m))); auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply GROUP_reg_right with (nat_to_group m); auto with *.
apply
 Trans
  with
    (sgroup_law G (sgroup_law G (nat_to_group m) (nat_to_group (n - m)))
       (sgroup_law G (group_inverse G (nat_to_group m)) (nat_to_group m)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (sgroup_law G (sgroup_law G (nat_to_group m) (nat_to_group (n - m)))
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
       (monoid_unit G)); auto with *.
apply Trans with (sgroup_law G (nat_to_group m) (nat_to_group (n - m)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Qed.
Hint Resolve nat_to_group_minus: algebra.

Lemma ax8 :
 forall p q : positive,
 Pcompare p q Datatypes.Eq = Datatypes.Lt ->
 Pcompare q p Datatypes.Eq = Datatypes.Gt.
(* Goal: forall (p q : positive) (_ : @eq comparison (Pos.compare_cont Eq p q) Lt), @eq comparison (Pos.compare_cont Eq q p) Gt *)
intros p q H'; try assumption.
(* Goal: @eq comparison (Pos.compare_cont Eq q p) Gt *)
apply nat_of_P_gt_Gt_compare_complement_morphism.
(* Goal: gt (Pos.to_nat q) (Pos.to_nat p) *)
red in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply nat_of_P_lt_Lt_compare_morphism; auto with *.
Qed.
Hint Resolve ax8: algebra.

Lemma Zl4 :
 forall p p0 : positive,
 Equal (Z_to_group_nat_fun (Zpos p + Zneg p0)%Z)
   (sgroup_law G (nat_to_group (nat_of_P p))
      (group_inverse G (nat_to_group (nat_of_P p0)))).
(* Goal: forall p p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
intros p p0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
case (Z_gt_le_dec (Zpos p) (Zpos p0)); intros z.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
rewrite ax5; auto with *.
apply Trans with (nat_to_group (nat_of_P (pos_abs (ax3 (p - p0)))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
rewrite nat_of_P_minus_morphism; auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (nat_to_group (Init.Nat.sub (Pos.to_nat p0) (Pos.to_nat p))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p0)) (group_inverse G (nat_to_group (Pos.to_nat p)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p0)) (group_inverse G (nat_to_group (Pos.to_nat p))))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
apply nat_to_group_minus.
(* Goal: gt (Pos.to_nat p0) (Pos.to_nat p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p0)) (group_inverse G (nat_to_group (Pos.to_nat p))))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
apply nat_of_P_gt_Gt_compare_morphism.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
case (Z_le_lt_eq_dec _ _ z); intros.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
rewrite ax6; auto with *.
apply
 Trans
  with (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 (p0 - p))))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
rewrite nat_of_P_minus_morphism; auto with *.
apply
 Trans
  with
    (group_inverse G
       (sgroup_law G (nat_to_group (nat_of_P p0))
          (group_inverse G (nat_to_group (nat_of_P p))))); 
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (nat_to_group (Init.Nat.sub (Pos.to_nat p0) (Pos.to_nat p)))) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p0)) (group_inverse G (nat_to_group (Pos.to_nat p))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p0)) (group_inverse G (nat_to_group (Pos.to_nat p))))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
apply GROUP_comp.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (nat_to_group (Init.Nat.sub (Pos.to_nat p0) (Pos.to_nat p))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p0)) (group_inverse G (nat_to_group (Pos.to_nat p)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p0)) (group_inverse G (nat_to_group (Pos.to_nat p))))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
apply nat_to_group_minus.
(* Goal: gt (Pos.to_nat p0) (Pos.to_nat p) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p0)) (group_inverse G (nat_to_group (Pos.to_nat p))))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
apply nat_of_P_gt_Gt_compare_morphism.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
apply
 Trans
  with
    (sgroup_law G
       (group_inverse G (group_inverse G (nat_to_group (nat_of_P p))))
       (group_inverse G (nat_to_group (nat_of_P p0)))); 
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
injection e.
(* Goal: forall _ : @eq Z (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
rewrite <- H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Z.add (Zpos p) (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group (Pos.to_nat p)) (group_inverse G (nat_to_group (Pos.to_nat p)))) *)
rewrite ax7.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (monoid_unit G); auto with *.
Qed.
Hint Resolve Zl4: algebra.

Lemma nat_to_group_com3 :
 forall n : nat,
 Equal (sgroup_law G (nat_to_group n) (group_inverse G r))
   (sgroup_law G (group_inverse G r) (nat_to_group n)).
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
simple induction n; simpl in |- *; auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (group_inverse G r); auto with *.
(* Goal: forall (n : nat) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) (group_inverse G r)) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G r) (nat_to_group n))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r) (group_inverse G r)) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G r) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r)) *)
intros n0 H'; try assumption.
apply
 Trans
  with (sgroup_law G (nat_to_group n0) (sgroup_law G r (group_inverse G r)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply Trans with (sgroup_law G (nat_to_group n0) (monoid_unit G));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (nat_to_group n0); auto with *.
apply
 Trans
  with (sgroup_law G (group_inverse G r) (sgroup_law G r (nat_to_group n0)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with (sgroup_law G (sgroup_law G (group_inverse G r) r) (nat_to_group n0));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply Trans with (sgroup_law G (monoid_unit G) (nat_to_group n0));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
Qed.
Hint Resolve nat_to_group_com3: algebra.

Lemma Zl5 : Equal (Z_to_group_nat_fun (ring_unit ZZ)) r.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec z Z0 with | left z0 => pos_to_group r (@pos_abs z z0) | right z0 => match Z_le_lt_eq_dec z Z0 z0 with | left l => pos_to_group (group_inverse G r) (@pos_abs (Z.opp z) (@Zlemma1 z l)) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end (@Z_to_group_nat_fun G r z) *)
unfold Z_to_group_nat_fun in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec (ring_unit (cring_ring (idomain_ring ZZ))) Z0 with | left z => nat_to_group (Pos.to_nat (@pos_abs (ring_unit (cring_ring (idomain_ring ZZ))) z)) | right z => match Z_le_lt_eq_dec (ring_unit (cring_ring (idomain_ring ZZ))) Z0 z with | left l => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (ring_unit (cring_ring (idomain_ring ZZ)))) (@Zlemma1 (ring_unit (cring_ring (idomain_ring ZZ))) l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end r *)
case (Z_gt_le_dec (ring_unit ZZ) 0).
(* Goal: forall l : Z.le (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec (ring_unit (cring_ring (idomain_ring ZZ))) Z0 l with | left l0 => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (ring_unit (cring_ring (idomain_ring ZZ)))) (@Zlemma1 (ring_unit (cring_ring (idomain_ring ZZ))) l0)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end r *)
intros z; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: forall l : Z.le (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec (ring_unit (cring_ring (idomain_ring ZZ))) Z0 l with | left l0 => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (ring_unit (cring_ring (idomain_ring ZZ)))) (@Zlemma1 (ring_unit (cring_ring (idomain_ring ZZ))) l0)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end r *)
intros z; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec (ring_unit (cring_ring (idomain_ring ZZ))) Z0 z with | left l => group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (ring_unit (cring_ring (idomain_ring ZZ)))) (@Zlemma1 (ring_unit (cring_ring (idomain_ring ZZ))) l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end r *)
case (Z_le_lt_eq_dec (ring_unit ZZ) 0 z).
(* Goal: forall l : Z.lt (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (nat_to_group (Pos.to_nat (@pos_abs (Z.opp (ring_unit (cring_ring (idomain_ring ZZ)))) (@Zlemma1 (ring_unit (cring_ring (idomain_ring ZZ))) l))))) r *)
(* Goal: forall _ : @eq Z (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
intros z0; try assumption.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
absurd (ring_unit ZZ < 0)%Z; auto with *.
(* Goal: forall _ : @eq Z (ring_unit (cring_ring (idomain_ring ZZ))) Z0, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r *)
inversion H'.
Qed.
Hint Resolve Zl5: algebra.

Lemma nat_to_group_com4 :
 forall n m : nat,
 Equal (sgroup_law G (nat_to_group m) (group_inverse G (nat_to_group n)))
   (sgroup_law G (group_inverse G (nat_to_group n)) (nat_to_group m)).
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
simple induction n; simpl in |- *; auto with *.
(* Goal: forall m : nat, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) (nat_to_group m)) *)
(* Goal: forall (n : nat) (_ : forall m : nat, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (nat_to_group n))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (nat_to_group n)) (nat_to_group m))) (m : nat), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r)) (nat_to_group m)) *)
intros m; try assumption.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (sgroup_law G (nat_to_group m) (monoid_unit G)); auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (nat_to_group m); auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (sgroup_law G (monoid_unit G) (nat_to_group m)); auto with *.
(* Goal: forall (n : nat) (_ : forall m : nat, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (nat_to_group n))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (nat_to_group n)) (nat_to_group m))) (m : nat), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group m) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (nat_to_group n) r)) (nat_to_group m)) *)
intros n0 H' m; try assumption.
apply
 Trans
  with
    (sgroup_law G (nat_to_group m)
       (sgroup_law G (group_inverse G r) (group_inverse G (nat_to_group n0))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (sgroup_law G (sgroup_law G (nat_to_group m) (group_inverse G r))
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
       (group_inverse G (nat_to_group n0))); auto with *.
apply
 Trans
  with
    (sgroup_law G (sgroup_law G (group_inverse G r) (nat_to_group m))
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
       (group_inverse G (nat_to_group n0))); auto with *.
apply
 Trans
  with
    (sgroup_law G (group_inverse G r)
       (sgroup_law G (nat_to_group m) (group_inverse G (nat_to_group n0))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (sgroup_law G (group_inverse G r)
       (sgroup_law G (group_inverse G (nat_to_group n0)) (nat_to_group m)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (sgroup_law G
       (sgroup_law G (group_inverse G r) (group_inverse G (nat_to_group n0)))
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
       (nat_to_group m)); auto with *.
Qed.
Hint Resolve nat_to_group_com4: algebra.
Comments "The group  morphism from the integers to an arbitrary group.".

Definition Z_to_group_nat : Hom (ZZ:GROUP) G.
(* Goal: Carrier (@Hom GROUP (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))) : Ob GROUP) G) *)
apply (BUILD_HOM_GROUP (G:=ZZ:GROUP) (G':=G) (ff:=Z_to_group_nat_fun)).
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) x y), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_fun x) (Z_to_group_fun y) *)
(* Goal: forall x y : 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))) (Z_to_group_fun (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) x y)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_fun x) (Z_to_group_fun y)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros x y H'; try assumption.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
rewrite H'; auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simple induction x; simple induction y; simpl in |- *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
unfold sgroup_law at 1 in |- *; simpl in |- *.
apply Trans with (sgroup_law G (Z_to_group_nat_fun 0%Z) (monoid_unit G));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) Z0 (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun Z0) (Z_to_group_nat_fun (Zneg p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) Z0 (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun Z0) (Z_to_group_nat_fun (Zneg p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
rewrite Zplus_0_l.
apply Trans with (sgroup_law G (monoid_unit G) (Z_to_group_nat_fun (Zpos p)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: forall p : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) Z0 (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun Z0) (Z_to_group_nat_fun (Zneg p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) Z0 (Zneg p))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun Z0) (Z_to_group_nat_fun (Zneg p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
rewrite Zplus_0_l.
apply Trans with (sgroup_law G (monoid_unit G) (Z_to_group_nat_fun (Zneg p)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zpos p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zpos p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) Z0)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun Z0)) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
rewrite Zplus_0_r.
apply Trans with (sgroup_law G (Z_to_group_nat_fun (Zpos p)) (monoid_unit G));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
unfold sgroup_law at 1 in |- *; simpl in |- *.
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Zneg (Pos.add p p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p0; try assumption.
apply Trans with (nat_to_group (nat_of_P (pos_abs (ax3 (p + p0)))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (sgroup_law G (nat_to_group (nat_of_P (pos_abs (ax3 p))))
       (nat_to_group (nat_of_P (pos_abs (ax3 p0))))); 
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (nat_to_group (Pos.to_nat (Pos.add p p0)))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (nat_to_group (Pos.to_nat p))) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
rewrite nat_of_P_plus_morphism.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Zneg (Pos.add p p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p0; try assumption.
apply
 Trans
  with
    (sgroup_law G (nat_to_group (nat_of_P (pos_abs (ax3 p))))
       (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 p0))))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply Trans with (sgroup_law G (Z_to_group_nat_fun (Zneg p)) (monoid_unit G));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Zneg (Pos.add p p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zpos p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zpos p0))) *)
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (sgroup_law (@Group_util.sg (Leibnitz_set Z) Z.add (fun (x x' y y' : Z) (H' : @eq Z x x') (H'0 : @eq Z y y') => @eq_ind_r Z y' (fun y0 : Z => @eq Z (Z.add x y0) (Z.add x' y')) (@eq_ind_r Z x' (fun x0 : Z => @eq Z (Z.add x0 y') (Z.add x' y')) (@eq_refl Z (Z.add x' y')) x H') y H'0) (fun x y z : Z => @Sym (Leibnitz_set Z) (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) (@eq_ind_r Z (Z.add (Z.add x y) z) (fun z0 : Z => @eq Z z0 (Z.add (Z.add x y) z)) (@eq_refl Z (Z.add (Z.add x y) z)) (Z.add x (Z.add y z)) (Z.add_assoc x y z)))) (Zneg p) (Zneg p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
rewrite Zplus_comm.
apply
 Trans
  with
    (sgroup_law G
       (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 p)))))
       (nat_to_group (nat_of_P (pos_abs (ax3 p0))))); 
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (sgroup_law G (nat_to_group (nat_of_P (pos_abs (ax3 p0))))
       (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 p))))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
unfold sgroup_law at 1 in |- *; simpl in |- *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
simpl in |- *; auto with *.
(* Goal: forall p0 : positive, @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (Zneg (Pos.add p p0))) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_nat_fun (Zneg p)) (Z_to_group_nat_fun (Zneg p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros p0; try assumption.
apply
 Trans
  with (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 (p + p0))))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (sgroup_law G
       (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 p)))))
       (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 p0))))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (nat_to_group (Pos.to_nat (Pos.add p p0)))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G (nat_to_group (Pos.to_nat p))) (group_inverse G (nat_to_group (Pos.to_nat p0)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_nat_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
rewrite nat_of_P_plus_morphism.
apply
 Trans
  with
    (group_inverse G
       (sgroup_law G (nat_to_group (nat_of_P p)) (nat_to_group (nat_of_P p0))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (group_inverse G
       (sgroup_law G (nat_to_group (nat_of_P p0)) (nat_to_group (nat_of_P p))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Defined.
End Zup1.
Hint Resolve nat_to_group_com nat_to_group_add nat_to_group_com2
  nat_to_group_minus nat_to_group_com3 nat_to_group_com4: algebra.
Section Zup2.
Variable G : GROUP.
Section pos_def.
Variable r : G.

Fixpoint pos_to_group (p : positive) : G :=
  match p with
  | xH => r
  | xO p' => group_square G (pos_to_group p')
  | xI p' => sgroup_law G (group_square G (pos_to_group p')) r
  end.

Lemma pos_nat_group :
 forall p : positive, Equal (pos_to_group p) (nat_to_group r (nat_of_P p)).
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simple induction p; simpl in |- *.
(* Goal: forall (p : positive) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (pos_to_group p) (@nat_to_group G r (Pos.to_nat p))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (pos_to_group p) (pos_to_group p)) (@nat_to_group G r (Pos.to_nat (xO p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) r (sgroup_law (monoid_sgroup (group_monoid G)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r) *)
intros p0 H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (pos_to_group p0) (pos_to_group p0)) (@nat_to_group G r (Pos.iter_op nat Init.Nat.add p0 (S (S O)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) r (sgroup_law (monoid_sgroup (group_monoid G)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r) *)
rewrite ZL6.
(* Goal: forall (p : positive) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (pos_to_group p) (@nat_to_group G r (Pos.to_nat p))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_square G (pos_to_group p)) (@nat_to_group G r (Pos.to_nat (xO p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) r (sgroup_law (monoid_sgroup (group_monoid G)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r) *)
unfold group_square in |- *.
apply
 Trans
  with
    (sgroup_law G
       (sgroup_law G (nat_to_group r (nat_of_P p0))
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
          (nat_to_group r (nat_of_P p0))) r); auto with *.
(* Goal: forall (p : positive) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (pos_to_group p) (@nat_to_group G r (Pos.to_nat p))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_square G (pos_to_group p)) (@nat_to_group G r (Pos.to_nat (xO p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) r (sgroup_law (monoid_sgroup (group_monoid G)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r) *)
unfold group_square in |- *.
(* Goal: forall (p : positive) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (pos_to_group p) (@nat_to_group G r (Pos.to_nat p))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (pos_to_group p) (pos_to_group p)) (@nat_to_group G r (Pos.to_nat (xO p))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) r (sgroup_law (monoid_sgroup (group_monoid G)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r) *)
intros p0 H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (pos_to_group p0) (pos_to_group p0)) (@nat_to_group G r (Pos.to_nat (xO p0))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) r (sgroup_law (monoid_sgroup (group_monoid G)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r) *)
unfold nat_of_P in |- *.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (pos_to_group p0) (pos_to_group p0)) (@nat_to_group G r (Pos.iter_op nat Init.Nat.add p0 (S (S O)))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) r (sgroup_law (monoid_sgroup (group_monoid G)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) r) *)
rewrite ZL6.
apply
 Trans
  with
    (sgroup_law G (nat_to_group r (nat_of_P p0))
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
       (nat_to_group r (nat_of_P p0))); auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Qed.
End pos_def.
Hint Resolve pos_nat_group: algebra.
Variable r : G.

Definition Z_to_group_fun : ZZ -> G.
(* Goal: forall _ : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))), Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
intros x.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
case (Z_gt_le_dec x 0); intros z.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
exact (pos_to_group r (pos_abs z)).
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
case (Z_le_lt_eq_dec _ _ z); intros.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
cut (- x > 0)%Z.
(* Goal: forall _ : Z.gt (Z.opp x) Z0, Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
intros H'.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
exact (pos_to_group (group_inverse G r) (pos_abs H')).
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
apply Zlemma1.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: Carrier (sgroup_set (monoid_sgroup (group_monoid G))) *)
exact (monoid_unit G).
Defined.

Lemma nat_to_group_inverse :
 forall (n : nat) (r : G),
 Equal (group_inverse G (nat_to_group r n))
   (nat_to_group (group_inverse G r) n).
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
simple induction n; simpl in |- *; auto with *.
(* Goal: forall (n : nat) (_ : forall r : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (@nat_to_group G r n)) (@nat_to_group G (group_inverse G r) n)) (r : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) (@nat_to_group G r n) r)) (sgroup_law (monoid_sgroup (group_monoid G)) (@nat_to_group G (group_inverse G r) n) (group_inverse G r)) *)
intros n0 H' r0; try assumption.
apply
 Trans
  with
    (sgroup_law G (group_inverse G r0) (group_inverse G (nat_to_group r0 n0)));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
apply
 Trans
  with
    (sgroup_law G (group_inverse G r0) (nat_to_group (group_inverse G r0) n0));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
Qed.
Hint Resolve nat_to_group_inverse: algebra.

Lemma Z_to_group_fun_eq :
 forall z : ZZ, Equal (Z_to_group_fun z) (Z_to_group_nat r z).
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
intros z; simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_fun z) (@Z_to_group_nat_fun G r z) *)
unfold Z_to_group_fun in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec z Z0 with | left z0 => pos_to_group r (@pos_abs z z0) | right z0 => match Z_le_lt_eq_dec z Z0 z0 with | left l => pos_to_group (group_inverse G r) (@pos_abs (Z.opp z) (@Zlemma1 z l)) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end (@Z_to_group_nat_fun G r z) *)
unfold Z_to_group_nat_fun in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_gt_le_dec z Z0 with | left z0 => pos_to_group r (@pos_abs z z0) | right z0 => match Z_le_lt_eq_dec z Z0 z0 with | left l => pos_to_group (group_inverse G r) (@pos_abs (Z.opp z) (@Zlemma1 z l)) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end match Z_gt_le_dec z Z0 with | left z0 => @nat_to_group G r (Pos.to_nat (@pos_abs z z0)) | right z0 => match Z_le_lt_eq_dec z Z0 z0 with | left l => group_inverse G (@nat_to_group G r (Pos.to_nat (@pos_abs (Z.opp z) (@Zlemma1 z l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end end *)
case (Z_gt_le_dec z 0); intros z0.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) match Z_le_lt_eq_dec z Z0 z0 with | left l => pos_to_group (group_inverse G r) (@pos_abs (Z.opp z) (@Zlemma1 z l)) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end match Z_le_lt_eq_dec z Z0 z0 with | left l => group_inverse G (@nat_to_group G r (Pos.to_nat (@pos_abs (Z.opp z) (@Zlemma1 z l)))) | right e => @monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)) end *)
case (Z_le_lt_eq_dec z 0 z0); intros z1.
apply
 Trans
  with (nat_to_group (group_inverse G r) (nat_of_P (pos_abs (Zlemma1 z1))));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
Qed.
Hint Resolve Z_to_group_fun_eq: algebra.

Definition Z_to_group : Hom (ZZ:GROUP) G.
(* Goal: Carrier (@Hom GROUP (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))) : Ob GROUP) G) *)
apply (BUILD_HOM_GROUP (G:=ZZ:GROUP) (G':=G) (ff:=Z_to_group_fun)).
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) x y), @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_fun x) (Z_to_group_fun y) *)
(* Goal: forall x y : 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))) (Z_to_group_fun (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) x y)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_fun x) (Z_to_group_fun y)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros x y H'; try assumption.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (Z_to_group_nat r x); auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (Z_to_group_nat r y); auto with *.
(* Goal: forall x y : 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))) (Z_to_group_fun (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) x y)) (sgroup_law (monoid_sgroup (group_monoid G)) (Z_to_group_fun x) (Z_to_group_fun y)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (Z_to_group_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros x y; try assumption.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (Z_to_group_nat r (sgroup_law ZZ x y)); auto with *.
apply Trans with (sgroup_law G (Z_to_group_nat r x) (Z_to_group_nat r y));
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
 auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
apply Trans with (Z_to_group_nat r (monoid_unit ZZ)); auto with *.
Defined.
End Zup2.
Set Strict Implicit.
Unset Implicit Arguments.

Definition group_power (G : GROUP) (x : G) (n : ZZ) := Z_to_group x n.
Set Implicit Arguments.
Unset Strict Implicit.

Definition sgroup_powers (G : GROUP) (g : G) := coKer (Z_to_group g).

Lemma sgroup_powers_prop :
 forall (G : GROUP) (g x : G),
 in_part x (sgroup_powers g) -> exists n : ZZ, Equal x (group_power G g n).
(* Goal: forall (G : Ob GROUP) (g x : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid G))) x (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g))))), @ex (Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (fun 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))) x (group_power G g n)) *)
intros G g x H'; try assumption.
(* Goal: @ex (Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (fun 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))) x (group_power G g n)) *)
elim H'.
(* Goal: forall (x0 : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (_ : and (@in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))) x0 (full (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ))))))))) (@Equal (sgroup_set (monoid_sgroup (group_monoid G))) x (@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))) x0))), @ex (Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (fun 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))) x (group_power G g n)) *)
intros x0 H'0; try assumption.
(* Goal: @ex (Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (fun 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))) x (group_power G g n)) *)
elim H'0; intros H'1 H'2; try exact H'2; clear H'0.
(* Goal: @ex (Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring ZZ)))))))) (fun 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))) x (group_power G g n)) *)
exists x0; try assumption.
Qed.

Lemma sgroup_powers_rev :
 forall (G : GROUP) (g : G) (n : ZZ),
 in_part (group_power G g n) (sgroup_powers g).
(* Goal: forall (G : Ob GROUP) (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)))))))), @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
intros G g n; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G (@sgroup_powers G g)))) *)
simpl in |- *.
(* Goal: @ex Z (fun x : Z => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g x))) *)
exists n; split; [ idtac | try assumption ].
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
auto with *.
(* Goal: True *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (group_power G g n) (@Z_to_group_fun G g n) *)
unfold group_power in |- *; auto with *.
Qed.
Hint Resolve sgroup_powers_prop sgroup_powers_rev: algebra.
