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

diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma
index 2078cf1d7..44238d69e 100644
--- a/matita/library/algebra/finite_groups.ma
+++ b/matita/library/algebra/finite_groups.ma
@@ -516,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;