interpretation "Monoid unit" 'munit S =
(cic:/matita/algebra/monoids/e.con S).
+
+notation < "M"
+for @{ 'semigroup $M }.
+
+interpretation "Semigroup coercion" 'semigroup M =
+ (cic:/matita/algebra/monoids/semigroup.con M).
definition is_left_inverse ≝
λM:Monoid.