is_finite_enumerable:> finite_enumerable semigroup
}.
-notation < "S"
-for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
-
-interpretation "Semigroup_of_finite_enumerable_semigroup"
- 'semigroup_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/semigroup.con S).
-
-notation < "S"
-for @{ 'magma_of_finite_enumerable_semigroup $S }.
-
-interpretation "Magma_of_finite_enumerable_semigroup"
- 'magma_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/Magma_of_finite_enumerable_SemiGroup.con S).
-
-notation < "S"
-for @{ 'type_of_finite_enumerable_semigroup $S }.
-
-interpretation "Type_of_finite_enumerable_semigroup"
- 'type_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/Type_of_finite_enumerable_SemiGroup.con S).
-
interpretation "Finite_enumerable representation" 'repr S i =
(cic:/matita/algebra/finite_groups/repr.con S
(cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
clearbody GOGO;
rewrite < HH in GOGO;
rewrite < HH in GOGO:(? ? % ?);
- rewrite > (associative ? G) in GOGO;
+ rewrite > (op_associative ? G) in GOGO;
letin GaGa ≝ (H ? ? ? GOGO);
clearbody GaGa;
clear GOGO;
letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite > (associative ? (semigroup_properties G)) in GaxGax;
+ rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
letin GaxGax ≝ (refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite < (associative ? (semigroup_properties G)) in GaxGax;
+ rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H1 ? ? ? GaxGax)
]
]
elim H3;
assumption
| intros;
- change in H5 with (ι(G \sub O · G \sub x) = ι(G \sub O · G \sub y));
+ simplify in H5;
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;