update in groud_2 and models

[helm.git] / helm / software / matita / library / Q / fraction / ftimes.ma

diff --git a/helm/software/matita/library/Q/fraction/ftimes.ma b/helm/software/matita/library/Q/fraction/ftimes.ma
index bcc7358b27a5ed0b3098c5cbb859a7a12d95a1fd..aff8a04a65c23a1c8a015800e9b008525f20a9f1 100644 (file)
--- 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