huge commit in automation:

[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..395b24248f692366330c48ec002ed5c82bb095bd 100644 (file)
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -758,12 +758,11 @@ cut (n \divides p \lor n \ndivides p)
          [(* first case *)
           rewrite > (times_n_SO q).rewrite < H5.
           rewrite > distr_times_minus.
+          elim H1. autobatch;
+          (*
           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 +773,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;
+          (*
           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).
@@ -925,7 +925,7 @@ intros.elim H3.
 rewrite > H4 in H2.
 elim (divides_times_to_divides ? ? ? H H2)
   [apply False_ind.apply H1.assumption
-  |elim H5.
+  |elim H5.  
    apply (witness ? ? n2).
    rewrite > sym_times in ⊢ (? ? ? (? % ?)).
    rewrite > assoc_times.