-notation < "M" for @{ 'semigroup $M }.
-interpretation "premonoid coercion" 'premonoid M =
- (cic:/matita/algebra/monoids/premonoid.con M).
-
-notation < "M" for @{ 'typeofmonoid $M }.
-interpretation "premonoid coercion" 'typeofmonoid M =
- (cic:/matita/algebra/monoids/Type_of_Monoid.con M).
-
-notation < "M" for @{ 'magmaofmonoid $M }.
-interpretation "premonoid coercion" 'magmaofmonoid M =
- (cic:/matita/algebra/monoids/Magma_of_Monoid.con M).
-
-notation "1" with precedence 89
-for @{ 'munit }.
+definition SemiGroup_of_Monoid: Monoid → SemiGroup ≝
+ λM. mk_SemiGroup ? (is_monoid M).
+
+coercion SemiGroup_of_Monoid nocomposites.