Inductive M1:Set :=
e1:M1 | u:M1.
Definition M1_eq :(Relation M1):= fun a => fun b => (a=b).
Definition M1_ap : (Crelation M1):= fun a => fun b => ~ (a=b).
Lemma M1_ap_irreflexive: (irreflexive M1_ap).
Lemma M1_ap_symmetric: (Csymmetric M1_ap).
Lemma M1_ap_cotransitive: (cotransitive M1_ap).
Lemma M1_eq_dec: forall(x:M1),(M1_eq x e1) or (M1_eq x u).
Definition is_e1 (x:M1):Prop :=
match x with
|e1 => True
|u => ⊥
end.
Lemma not_M1_eq_e1_u:Not (M1_eq e1 u).
Lemma M1_ap_tight: (tight_apart M1_eq M1_ap).
Definition M1_is_CSetoid:(is_CSetoid M1 M1_eq M1_ap) :=
(Build_is_CSetoid M1 M1_eq M1_ap M1_ap_irreflexive M1_ap_symmetric M1_ap_cotransitive M1_ap_tight).
Definition M1_as_CSetoid: CSetoid :=
(Build_CSetoid M1 M1_eq M1_ap M1_is_CSetoid).
Definition M1_mult (x:M1)(y:M1):M1:=
match x with
|e1 => y
|u => match y with
|e1 => u
|u => e1
end
end.
Definition M1_CS_mult: M1_as_CSetoid -> M1_as_CSetoid -> M1_as_CSetoid.
Defined.
Lemma M1_CS_mult_strext:(bin_fun_strext M1_as_CSetoid M1_as_CSetoid M1_as_CSetoid M1_CS_mult).
Definition M1_mult_as_bin_fun:=
(Build_CSetoid_bin_fun M1_as_CSetoid M1_as_CSetoid M1_as_CSetoid M1_CS_mult M1_CS_mult_strext).
Definition M2_mult (x:M1)(y:M1):M1:=
match x with
|e1 => y
|u => u
end.
Definition M2_CS_mult: M1_as_CSetoid -> M1_as_CSetoid -> M1_as_CSetoid.
Defined.
Lemma M2_CS_mult_strext: (bin_fun_strext M1_as_CSetoid M1_as_CSetoid M1_as_CSetoid M2_CS_mult).
Definition M2_mult_as_bin_fun:=
(Build_CSetoid_bin_fun M1_as_CSetoid M1_as_CSetoid M1_as_CSetoid
M2_CS_mult M2_CS_mult_strext).
End p68E1b1.