X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Ffraction%2Fftimes.ma;h=aff8a04a65c23a1c8a015800e9b008525f20a9f1;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=bcc7358b27a5ed0b3098c5cbb859a7a12d95a1fd;hpb=7a116453d799657958e32693be28d18a5aab84fc;p=helm.git

diff --git a/helm/software/matita/library/Q/fraction/ftimes.ma b/helm/software/matita/library/Q/fraction/ftimes.ma
index bcc7358b2..aff8a04a6 100644
--- a/helm/software/matita/library/Q/fraction/ftimes.ma
+++ b/helm/software/matita/library/Q/fraction/ftimes.ma
@@ -122,12 +122,15 @@ elim n
         ]
       |generalize in match n4.
        elim n2
-        [cases n6;simplify;autobatch
+        [cases n6;simplify;
+          [ exists; [2: autobatch;]
+          | exists; [2:autobatch;]
+          ]
         |cases n7;simplify
-          [autobatch
+          [exists;[2:autobatch]
           |elim (H2 n9).
            rewrite > H3.
            simplify.
-           autobatch
+           exists;[2:autobatch]
           ]]]]]
 qed.
\ No newline at end of file