X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=44238d69ebb049f77a5f7d1e528263d95a20deff;hb=28acfd1782318702779811c36f5cafd3571ff6a6;hp=2f80525e704b3cc21682f843589b7317a7117934;hpb=e871e95f9ce6abc7fe6cd0e10c8cff60cd9a72e4;p=helm.git

diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma
index 2f80525e7..44238d69e 100644
--- a/matita/library/algebra/finite_groups.ma
+++ b/matita/library/algebra/finite_groups.ma
@@ -44,30 +44,6 @@ record finite_enumerable_SemiGroup : Type ≝
    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).
@@ -513,7 +489,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     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;
@@ -524,13 +500,13 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
       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)
     ]
   ]
@@ -540,7 +516,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     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;