--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/algebra/monoids/".
+
+include "algebra/semigroups.ma".
+
+record isMonoid (SS:SemiGroup) (e:SS) : Prop ≝
+ { e_is_left_unit: is_left_unit SS e;
+ e_is_right_unit: is_right_unit SS e
+ }.
+
+record Monoid : Type ≝
+ { semigroup: SemiGroup;
+ e: semigroup;
+ properties: isMonoid ? e
+ }.
+
+coercion cic:/matita/algebra/monoids/semigroup.con.
+
+definition is_left_inverse ≝
+ λM:Monoid. let op ≝ op M in let e ≝ e M in
+ λopp: M → M.
+ ∀x:M. op (opp x) x = e.
+
+definition is_right_inverse ≝
+ λM:Monoid. let op ≝ op M in let e ≝ e M in
+ λopp: M → M.
+ ∀x:M. op x (opp x) = e.
+
+theorem is_left_inverse_to_is_right_inverse_to_eq:
+ ∀M:Monoid. ∀oppL,oppR.
+ is_left_inverse M oppL → is_right_inverse M oppR →
+ ∀x:M. oppL x = oppR x.
+ intros;
+ letin op ≝ (op M);
+ letin e ≝ (e M);
+ generalize in match (H x); intro;
+ change in H2 with (op (oppL x) x = e);
+ generalize in match (eq_f ? ? (λy. op y (oppR x)) ? ? H2);
+ simplify; fold simplify op;
+ intro; clear H2;
+ generalize in match (properties (semigroup M)); intro;
+ unfold isSemiGroup in H2; unfold associative in H2;
+ rewrite > H2 in H3; clear H2;
+ rewrite > H1 in H3;
+ rewrite > (e_is_left_unit ? ? (properties M)) in H3;
+ rewrite > (e_is_right_unit ? ? (properties M)) in H3;
+ assumption.
+qed.
+