(* 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 Implicit Arguments.
Unset Strict Implicit.
Require Export Sub_group.
Require Export Group_util.
(** Title "Quotient of a group by a normal sub-group." *)
Section Def.
Variable G : GROUP.
Variable H : subgroup G.

Definition normal :=
  forall x y : G,
  in_part y H ->
  in_part (sgroup_law _ x (sgroup_law _ y (group_inverse _ x))) H.
Hypothesis Hnormal : normal.

Definition group_quo_eq (x y : G) :=
  in_part (sgroup_law _ x (group_inverse _ y)) H.

Definition group_quo_eqrel : Relation G.
(* Goal: Relation (sgroup_set (monoid_sgroup (group_monoid G))) *)
apply (Build_Relation (E:=G) (Rel_fun:=group_quo_eq)).
(* Goal: @symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
red in |- *.
(* Goal: group_quo_eq (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) z) (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y z)) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) x *)
(* Goal: forall (x y : Carrier group_quo_set) (_ : @Equal group_quo_set x y), @Equal group_quo_set (group_inverse G x) (group_inverse G y) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
unfold app_rel, group_quo_eq in |- *.
(* Goal: forall (x x' y y' : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x x') (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) y y') (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G y)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H)))), @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x' (group_inverse G y')) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
intros x x' y y' H' H'0 H'1; try assumption.
apply in_part_comp_l with (sgroup_law G x (group_inverse G y));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
Defined.

Lemma group_quo_eqrel_equiv : equivalence group_quo_eqrel.
(* Goal: @equivalence (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
red in Hnormal.
(* Goal: @symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
red in |- *.
(* Goal: and (@transitive (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel)) (@symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel)) *)
split; [ try assumption | idtac ].
(* Goal: @symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
red in |- *.
(* Goal: @symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
intros x; red in |- *.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @app_rel (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) x y), @app_rel (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) y x *)
simpl in |- *.
(* Goal: group_quo_eq (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) z) (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y z)) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) x *)
(* Goal: forall (x y : Carrier group_quo_set) (_ : @Equal group_quo_set x y), @Equal group_quo_set (group_inverse G x) (group_inverse G y) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
unfold app_rel, group_quo_eq in |- *.
apply
 in_part_comp_l
  with (sgroup_law G x (sgroup_law G (monoid_unit G) (group_inverse G x)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
red in |- *.
(* Goal: and (@transitive (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel)) (@symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel)) *)
split; [ try assumption | idtac ].
(* Goal: @symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
red in |- *.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @app_rel (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) x y), @app_rel (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) y x *)
simpl in |- *.
(* Goal: group_quo_eq (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) z) (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y z)) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) x *)
(* Goal: forall (x y : Carrier group_quo_set) (_ : @Equal group_quo_set x y), @Equal group_quo_set (group_inverse G x) (group_inverse G y) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
unfold app_rel, group_quo_eq in |- *.
(* Goal: forall (x y z : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G y)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H)))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) y (group_inverse G z)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H)))), @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G z)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: @symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
intros x y z H' H'0; try assumption.
apply
 in_part_comp_l
  with
    (sgroup_law G (sgroup_law G x (group_inverse G y))
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
       (sgroup_law G y (group_inverse G z))); auto with algebra.
apply
 Trans
  with
    (sgroup_law G x
       (sgroup_law G (group_inverse G y) (sgroup_law G y (group_inverse G z))));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 Trans
  with
    (sgroup_law G x
       (sgroup_law G (sgroup_law G (group_inverse G y) y) (group_inverse G z)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 Trans
  with (sgroup_law G x (sgroup_law G (monoid_unit G) (group_inverse G z)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @symmetric (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) *)
red in |- *.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @app_rel (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) x y), @app_rel (Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (@Rel_fun (sgroup_set (monoid_sgroup (group_monoid G))) group_quo_eqrel) y x *)
simpl in |- *.
(* Goal: group_quo_eq (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) z) (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y z)) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) x *)
(* Goal: forall (x y : Carrier group_quo_set) (_ : @Equal group_quo_set x y), @Equal group_quo_set (group_inverse G x) (group_inverse G y) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
unfold app_rel, group_quo_eq in |- *.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H)))), @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) y x) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
intros x y H'; try assumption.
apply
 in_part_comp_l with (group_inverse G (sgroup_law G x (group_inverse G y)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 Trans
  with
    (sgroup_law G (group_inverse G (group_inverse G y)) (group_inverse G x));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
Qed.

Definition group_quo_set := quotient G group_quo_eqrel group_quo_eqrel_equiv.

Lemma normal_com_in :
 forall x y : G, in_part (sgroup_law _ x y) H -> in_part (sgroup_law _ y x) H.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H)))), @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) y x) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
intros x y H'; try assumption.
apply
 in_part_comp_l
  with (sgroup_law G y (sgroup_law G (sgroup_law G x y) (group_inverse G y)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) y x) (sgroup_law (monoid_sgroup (group_monoid G)) y (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (group_inverse G y))) *)
apply SGROUP_comp; auto with algebra.
apply Trans with (sgroup_law G x (sgroup_law G y (group_inverse G y)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y (group_inverse G y))) *)
apply Trans with (sgroup_law G x (monoid_unit G)); auto with algebra.
Qed.
Hint Immediate normal_com_in: algebra.
Set Strict Implicit.
Unset Implicit Arguments.

Definition group_quo : group.
apply
 (BUILD_GROUP (E:=group_quo_set) (genlaw:=fun x y : G => sgroup_law _ x y)
    (e:=monoid_unit G) (geninv:=fun x : G => group_inverse _ x)).
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
simpl in |- *; auto with algebra.
(* Goal: group_quo_eq (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) z) (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y z)) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) x *)
(* Goal: forall (x y : Carrier group_quo_set) (_ : @Equal group_quo_set x y), @Equal group_quo_set (group_inverse G x) (group_inverse G y) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
unfold app_rel, group_quo_eq in |- *.
(* Goal: forall (x x' y y' : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x')) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H)))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) y (group_inverse G y')) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H)))), @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (group_inverse G (sgroup_law (monoid_sgroup (group_monoid G)) x' y'))) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x y z : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) z) (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y z)) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) x *)
(* Goal: forall (x y : Carrier group_quo_set) (_ : @Equal group_quo_set x y), @Equal group_quo_set (group_inverse G x) (group_inverse G y) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros x x' y y' H' H'0; try assumption.
apply
 in_part_comp_l
  with
    (sgroup_law G x (sgroup_law G y (group_inverse G (sgroup_law G x' y'))));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G x) (group_inverse G (group_inverse G y))) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
apply normal_com_in.
apply
 in_part_comp_l
  with
    (sgroup_law G
       (sgroup_law G y
          (sgroup_law G (group_inverse G y') (group_inverse G x'))) x);
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G
       (sgroup_law G (sgroup_law G y (group_inverse G y'))
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
          (group_inverse G x')) x); auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G (sgroup_law G y (group_inverse G y'))
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
       (sgroup_law G (group_inverse G x') x)); auto with algebra.
(* Goal: forall x y z : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) z) (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y z)) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) x *)
(* Goal: forall (x y : Carrier group_quo_set) (_ : @Equal group_quo_set x y), @Equal group_quo_set (group_inverse G x) (group_inverse G y) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros x y z; try assumption.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
simpl in |- *; auto with algebra.
(* Goal: group_quo_eq (sgroup_law (monoid_sgroup (group_monoid G)) (sgroup_law (monoid_sgroup (group_monoid G)) x y) z) (sgroup_law (monoid_sgroup (group_monoid G)) x (sgroup_law (monoid_sgroup (group_monoid G)) y z)) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G)))) x *)
(* Goal: forall (x y : Carrier group_quo_set) (_ : @Equal group_quo_set x y), @Equal group_quo_set (group_inverse G x) (group_inverse G y) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
unfold app_rel, group_quo_eq in |- *.
apply
 in_part_comp_l
  with
    (sgroup_law G (sgroup_law G (sgroup_law G x y) z)
       (sgroup_law G (group_inverse G (sgroup_law G y z)) (group_inverse G x)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G (sgroup_law G (sgroup_law G x y) z)
       (sgroup_law G (sgroup_law G (group_inverse G z) (group_inverse G y))
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
          (group_inverse G x))); auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G (sgroup_law G x (sgroup_law G y z))
       (sgroup_law G (group_inverse G z)
          (sgroup_law G (group_inverse G y) (group_inverse G x))));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G x
       (sgroup_law G (sgroup_law G y z)
          (sgroup_law G (group_inverse G z)
             (sgroup_law G (group_inverse G y) (group_inverse G x)))));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G x
       (sgroup_law G y
          (sgroup_law G z
             (sgroup_law G (group_inverse G z)
                (sgroup_law G (group_inverse G y) (group_inverse G x))))));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G x
       (sgroup_law G y
          (sgroup_law G (sgroup_law G z (group_inverse G z))
             (sgroup_law G (group_inverse G y) (group_inverse G x)))));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G x
       (sgroup_law G y
          (sgroup_law G (monoid_unit G)
             (sgroup_law G (group_inverse G y) (group_inverse G x)))));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G x
       (sgroup_law G y (sgroup_law G (group_inverse G y) (group_inverse G x))));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with
    (sgroup_law G (sgroup_law G x y)
       (sgroup_law G (group_inverse G y) (group_inverse G x)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply
 in_part_comp_l
  with (sgroup_law G (sgroup_law G x y) (group_inverse G (sgroup_law G x y)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
apply in_part_comp_l with (monoid_unit G); auto with algebra.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
simpl in |- *; auto with algebra.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, group_quo_eq x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
unfold cart_eq, group_quo_eq in |- *.
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros x; try assumption.
apply in_part_comp_l with (sgroup_law G x (group_inverse G x));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
apply in_part_comp_l with (monoid_unit G); auto with algebra.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
intros x y; try assumption.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
simpl in |- *; auto with algebra.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, group_quo_eq x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
unfold cart_eq, group_quo_eq in |- *.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G y)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
intros H'; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) (group_inverse G x) (group_inverse G (group_inverse G y))) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
apply normal_com_in.
apply
 in_part_comp_l with (group_inverse G (sgroup_law G x (group_inverse G y)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: forall x : Carrier group_quo_set, @Equal group_quo_set (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) *)
intros x; try assumption.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
simpl in |- *; auto with algebra.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, group_quo_eq x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
unfold cart_eq, group_quo_eq in |- *.
apply
 in_part_comp_l
  with (sgroup_law G (sgroup_law G x (group_inverse G x)) (monoid_unit G));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
apply in_part_comp_l with (sgroup_law G x (group_inverse G x));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
apply in_part_comp_l with (monoid_unit G); auto with algebra.
Defined.
Set Implicit Arguments.
Unset Strict Implicit.

Definition group_quo_surj : Hom G group_quo.
(* Goal: Carrier (@Hom GROUP G group_quo) *)
apply (BUILD_HOM_GROUP (G:=G) (G':=group_quo) (ff:=fun x : G => x)).
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G)))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
intros x y; try assumption.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
simpl in |- *; auto with algebra.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, group_quo_eq x y *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
unfold cart_eq, group_quo_eq in |- *.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid G))) x y, @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G y)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
intros H'; try assumption.
apply in_part_comp_l with (sgroup_law G x (group_inverse G x));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
 auto with algebra.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid G))) (sgroup_law (monoid_sgroup (group_monoid G)) x (group_inverse G x)) (@subsgroup_part (monoid_sgroup (group_monoid G)) (@submonoid_subsgroup (group_monoid G) (@subgroup_submonoid G H))) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid G))), @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (sgroup_law (monoid_sgroup (group_monoid G)) x y) (sgroup_law (monoid_sgroup (group_monoid group_quo)) x y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
apply in_part_comp_l with (monoid_unit G); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid group_quo))) (@monoid_unit (monoid_sgroup (group_monoid G)) (monoid_on_def (group_monoid G))) (@monoid_unit (monoid_sgroup (group_monoid group_quo)) (monoid_on_def (group_monoid group_quo))) *)
auto with algebra.
Defined.
End Def.
Hint Immediate normal_com_in: algebra.