(* 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 Monoid_cat.
Section Lemmas.
Variable E : MONOID.

Lemma MONOID_unit_r : forall x : E, Equal (sgroup_law _ x (monoid_unit E)) x.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup E)), @Equal (sgroup_set (monoid_sgroup E)) (sgroup_law (monoid_sgroup E) x (@monoid_unit (monoid_sgroup E) (monoid_on_def E))) x *)
intros; apply (monoid_unit_r_prf E x).
Qed.

Lemma MONOID_unit_l : forall x : E, Equal (sgroup_law _ (monoid_unit E) x) x.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup E)), @Equal (sgroup_set (monoid_sgroup E)) (sgroup_law (monoid_sgroup E) (@monoid_unit (monoid_sgroup E) (monoid_on_def E)) x) x *)
intros; apply (monoid_unit_l_prf E x).
Qed.

Lemma MONOID_unit_unique :
 forall e : E,
 (forall x : E, Equal (sgroup_law _ x e) x) ->
 (forall x : E, Equal (sgroup_law _ e x) x) -> Equal e (monoid_unit E).
(* Goal: forall (e : Carrier (sgroup_set (monoid_sgroup E))) (_ : forall x : Carrier (sgroup_set (monoid_sgroup E)), @Equal (sgroup_set (monoid_sgroup E)) (sgroup_law (monoid_sgroup E) x e) x) (_ : forall x : Carrier (sgroup_set (monoid_sgroup E)), @Equal (sgroup_set (monoid_sgroup E)) (sgroup_law (monoid_sgroup E) e x) x), @Equal (sgroup_set (monoid_sgroup E)) e (@monoid_unit (monoid_sgroup E) (monoid_on_def E)) *)
intros e H' H'0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup E)) e (@monoid_unit (monoid_sgroup E) (monoid_on_def E)) *)
apply Trans with (sgroup_law _ e (monoid_unit E)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup E)) e (sgroup_law (monoid_sgroup E) e (@monoid_unit (monoid_sgroup E) (monoid_on_def E))) *)
apply Sym.
(* Goal: @Equal (sgroup_set (monoid_sgroup E)) (sgroup_law (monoid_sgroup E) e (@monoid_unit (monoid_sgroup E) (monoid_on_def E))) e *)
apply MONOID_unit_r.
Qed.
Variable F : MONOID.
Variable f : Hom E F.

Lemma MONOID_hom_prop : Equal (f (monoid_unit E)) (monoid_unit F).
(* Goal: @Equal (sgroup_set (monoid_sgroup F)) (@Ap (sgroup_set (monoid_sgroup E)) (sgroup_set (monoid_sgroup F)) (@sgroup_map (monoid_sgroup E) (monoid_sgroup F) (@monoid_sgroup_hom E F f)) (@monoid_unit (monoid_sgroup E) (monoid_on_def E))) (@monoid_unit (monoid_sgroup F) (monoid_on_def F)) *)
apply (monoid_hom_prf f).
Qed.
End Lemmas.
Hint Resolve MONOID_unit_r MONOID_unit_l MONOID_unit_unique MONOID_hom_prop:
  algebra.