1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/algebra/semigroups".
17 include "higher_order_defs/functions.ma".
19 definition isSemiGroup ≝
20 λC:Type. λop: C → C → C.associative C op.
22 record SemiGroup : Type ≝
24 op: carrier → carrier → carrier;
25 properties: isSemiGroup carrier op
28 coercion cic:/matita/algebra/semigroups/carrier.con.
30 definition is_left_unit ≝
31 λS:SemiGroup. λe:S. ∀x:S. op S e x = x.
33 definition is_right_unit ≝
34 λS:SemiGroup. λe:S. ∀x:S. op S x e = x.
36 theorem is_left_unit_to_is_right_unit_to_eq:
37 ∀S:SemiGroup. ∀e1,e2:S.
38 is_left_unit ? e1 → is_right_unit ? e2 → e1=e2.
41 rewrite < (H1 e1) in \vdash (? ? % ?);