-notation < "hvbox(|C|)" with precedence 89
-for @{ 'card $C }.
-
-interpretation "Finite_enumerable order" 'card C =
- (cic:/matita/algebra/finite_groups/order.con C _).
+interpretation "Finite_enumerable order" 'card C = (order C ?).
for @{ 'index_of_finite_enumerable_semigroup $e }.
interpretation "Index_of_finite_enumerable representation"
'index_of_finite_enumerable_semigroup e
=
for @{ 'index_of_finite_enumerable_semigroup $e }.
interpretation "Index_of_finite_enumerable representation"
'index_of_finite_enumerable_semigroup e
=
∀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:(? ? % ?);