Definition M1_is_CMonoid:(is_CMonoid M1_as_CSemiGroup e1):=
(Build_is_CMonoid M1_as_CSemiGroup e1 e1_is_rht_unit e1_is_lft_unit).
Definition M1_as_CMonoid:CMonoid:=
(Build_CMonoid M1_as_CSemiGroup e1 M1_is_CMonoid).
Definition M2_is_CMonoid :=
(Build_is_CMonoid M2_as_CSemiGroup e1 e1_is_rht_unit_M2 e1_is_lft_unit_M2).
Definition M2_as_CMonoid:CMonoid:=
(Build_CMonoid M2_as_CSemiGroup e1 M2_is_CMonoid).
Lemma two_element_CMonoids:
forall (op :(CSetoid_bin_fun M1_as_CSetoid M1_as_CSetoid M1_as_CSetoid))
(H: (is_CSemiGroup M1_as_CSetoid op)),
(is_unit (Build_CSemiGroup M1_as_CSetoid op H) e1)->
(forall (x y:M1_as_CSetoid),(op x y)= (M1_mult_as_bin_fun x y)) or
(forall (x y:M1_as_CSetoid), (op x y)= (M2_mult_as_bin_fun x y)).
End p68E1b1.
Section p69E1.
Let PM1M2:=(direct_product_as_CMonoid M1_as_CMonoid M2_as_CMonoid).
Let uu: PM1M2.
Defined.
Let e1u: PM1M2.
Defined.
Lemma ex_69 : uu [+] uu [=]e1u.
End p69E1.
Section p71E1_.
Lemma M1_is_generated_by_u: (forall(m:M1_as_CMonoid),
{n:nat | (@power_CMonoid M1_as_CMonoid u n)[=]m}):CProp.
Lemma not_injective_f:
~(injective (f_as_CSetoid_fun M1_as_CMonoid u M1_is_generated_by_u)).
End p71E1_.
Section p71E2b1.
Lemma not_isomorphic_M1_M2: ~ (isomorphic M1_as_CMonoid M2_as_CMonoid).
End p71E2b1.