(**************************************************************************)
include "algebra/groups.ma".
(**************************************************************************)
include "algebra/groups.ma".
∀G:finite_enumerable_SemiGroup.
left_cancellable ? (op G) →
right_cancellable ? (op G) →
∀G:finite_enumerable_SemiGroup.
left_cancellable ? (op G) →
right_cancellable ? (op G) →
| unfold is_left_unit; intro;
letin GaxGax ≝(refl_eq ? (G \sub a ·x));
clearbody GaxGax; (* demo *)
rewrite < GaGa in GaxGax:(? ? % ?);
| unfold is_left_unit; intro;
letin GaxGax ≝(refl_eq ? (G \sub a ·x));
clearbody GaxGax; (* demo *)
rewrite < GaGa in GaxGax:(? ? % ?);
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
letin GaxGax ≝(refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
letin GaxGax ≝(refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);