interpretation "Finite_enumerable order" 'card C =
(cic:/matita/algebra/finite_groups/order.con C _).
interpretation "Finite_enumerable order" 'card C =
(cic:/matita/algebra/finite_groups/order.con C _).
theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
∀G:finite_enumerable_SemiGroup.
left_cancellable ? (op G) →
right_cancellable ? (op G) →
∃e:G. isMonoid (mk_PreMonoid G e).
intros;
theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
∀G:finite_enumerable_SemiGroup.
left_cancellable ? (op G) →
right_cancellable ? (op G) →
∃e:G. isMonoid (mk_PreMonoid G e).
intros;
rewrite < GaGa in GaxGax:(? ? % ?);
rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
rewrite < GaGa in GaxGax:(? ? % ?);
rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
[ rewrite > (repr_index_of ? ? (G \sub O · G \sub x)) in Hcut;
rewrite > (repr_index_of ? ? (G \sub O · G \sub y)) in Hcut;
cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
[ rewrite > (repr_index_of ? ? (G \sub O · G \sub x)) in Hcut;
rewrite > (repr_index_of ? ? (G \sub O · G \sub y)) in Hcut;