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;