autobatch by

[helm.git] / helm / software / matita / library / nat / gcd.ma

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 958fddf970207216bfcab426a8389e202a942786..aa512566e7cc6735bb8e409b94a97f298bfcdf75 100644 (file)
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -755,15 +755,13 @@ cut (n \divides p \lor n \ndivides p)
     |right.
      cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
        [elim Hcut1.elim H3.elim H4
-         [(* first case *)
-          rewrite > (times_n_SO q).rewrite < H5.
+         [rewrite > (times_n_SO q).rewrite < H5.
           rewrite > distr_times_minus.
+          elim H1. autobatch by witness, divides_minus.
+         (*
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
-          elim H1.
-          pump 39.
-          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).          
-          (*
+          applyS (witness n ? ? (refl_eq ? ?)).          
           rewrite < (sym_times n).rewrite < assoc_times.
           rewrite > (sym_times q).rewrite > assoc_times.
           rewrite < (assoc_times a1).rewrite < (sym_times n).
@@ -774,11 +772,12 @@ cut (n \divides p \lor n \ndivides p)
          |(* second case *)
           rewrite > (times_n_SO q).rewrite < H5.
           rewrite > distr_times_minus.
+          elim H1. autobatch by witness, divides_minus.
+          (*
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
-          elim H1.rewrite > H6.
-          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
-          (*
+          rewrite > H6.
+          applyS (witness n ? ? (refl_eq ? ?)).
           rewrite < sym_times.rewrite > assoc_times.
           rewrite < (assoc_times q).
           rewrite < (sym_times n).
@@ -878,19 +877,15 @@ cut (n \divides p \lor n \ndivides p)
     |cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
       [elim Hcut1.elim H4.elim H5         
         [(* first case *)
+          elim H2. 
           rewrite > (times_n_SO p).rewrite < H6.
           rewrite > distr_times_minus.
-          rewrite > (sym_times p (a1*m)).
-          rewrite > (assoc_times a1).
-          elim H2.rewrite > H7. 
-          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
-         |(* second case *)
+          autobatch by witness, divides_minus.
+        |(* second case *)
+          elim H2.
           rewrite > (times_n_SO p).rewrite < H6.
           rewrite > distr_times_minus.
-          rewrite > (sym_times p (a1*m)).
-          rewrite > (assoc_times a1).
-          elim H2.rewrite > H7.
-          applyS (witness n ? ? (refl_eq ? ?)).
+          autobatch by witness, divides_minus.
         ](* end second case *)
      |rewrite < H1.apply eq_minus_gcd.
      ]
@@ -926,6 +921,7 @@ rewrite > H4 in H2.
 elim (divides_times_to_divides ? ? ? H H2)
   [apply False_ind.apply H1.assumption
   |elim H5.
+   (* applyS (witness ? ? n2 (refl_eq ? ?)).*)
    apply (witness ? ? n2).
    rewrite > sym_times in ⊢ (? ? ? (? % ?)).
    rewrite > assoc_times.