interpretation "Semigroup operation" 'ptimes S a b =
(cic:/matita/algebra/semigroups/op.con S a b). *)
+notation < "S"
+for @{ 'carrier $S }.
+
+interpretation "Carrier coercion" 'carrier S =
+ (cic:/matita/algebra/semigroups/carrier.con S).
+
definition is_left_unit ≝
λS:SemiGroup. λe:S. ∀x:S. e·x = x.