X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fconcrete_spaces.ma;h=3c03b4e667803df8815c98e4ef7806ae86b47715;hb=f7bfc8096055b1a8e82594b7079bad987676e639;hp=d95072cb973a2fa4c65f3ecd60212f84ba71438a;hpb=dd7f52dfd7f80b80368661fce5b58b644c102d7b;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index d95072cb9..3c03b4e66 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -67,23 +67,23 @@ definition convergent_relation_space_composition:
        constructor 1;
         [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
         | intros;
-          change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
+          change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
           change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
-            with (c \sub \f ∘ c1 \sub \f);
+            with (c1 \sub \f ∘ c \sub \f);
           change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
-            with (c \sub \f ∘ c1 \sub \f);
+            with (c1 \sub \f ∘ c \sub \f);
           apply (.= (extS_com ??????));
           apply (.= (†(respects_converges ?????)));
           apply (.= (respects_converges ?????));
           apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
           apply refl1;
-        | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
+        | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
           apply (.= (extS_com ??????));
           apply (.= (†(respects_all_covered ???)));
           apply (.= respects_all_covered ???);
           apply refl1]
      | intros;
-       change with (a ∘ b = a' ∘ b');
+       change with (b ∘ a = b' ∘ a');
        change in H with (rp'' ?? a = rp'' ?? a');
        change in H1 with (rp'' ?? b = rp ?? b');
        apply (.= (H‡H1));
@@ -106,15 +106,15 @@ definition CSPA: category1.
        apply refl1]
   | apply convergent_relation_space_composition
   | intros; simplify;
-    change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
+    change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
     apply (.= ASSOC1);
     apply refl1
   | intros; simplify;
-    change with (id1 ? o1 ∘ a = a);
-    apply (.= id_neutral_left1 ????);
+    change with (a ∘ id1 ? o1 = a);
+    apply (.= id_neutral_right1 ????);
     apply refl1
   | intros; simplify;
-    change with (a ∘ id1 ? o2 = a);
-    apply (.= id_neutral_right1 ????);
+    change with (id1 ? o2 ∘ a = a);
+    apply (.= id_neutral_left1 ????);
     apply refl1]
 qed.