X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=dcdbc7b7ad302405a445bef9cc1bcf9bdb1f4235;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=aa512566e7cc6735bb8e409b94a97f298bfcdf75;hpb=a2b703feae630d0fdd1740bd18e80ee1f6654a88;p=helm.git

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index aa512566e..dcdbc7b7a 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -757,7 +757,8 @@ cut (n \divides p \lor n \ndivides p)
        [elim Hcut1.elim H3.elim H4
          [rewrite > (times_n_SO q).rewrite < H5.
           rewrite > distr_times_minus.
-          elim H1. autobatch by witness, divides_minus.
+          elim H1.
+          autobatch by witness; 
          (*
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
@@ -772,7 +773,7 @@ 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.
+          elim H1. autobatch by witness; 
           (*
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
@@ -921,10 +922,13 @@ rewrite > H4 in H2.
 elim (divides_times_to_divides ? ? ? H H2)
   [apply False_ind.apply H1.assumption
   |elim H5.
-   (* applyS (witness ? ? n2 (refl_eq ? ?)).*)
+   autobatch by transitive_divides, H5, reflexive_divides,divides_times.
+   (*
    apply (witness ? ? n2).
    rewrite > sym_times in ⊢ (? ? ? (? % ?)).
    rewrite > assoc_times.
-   rewrite < H6.assumption
+   autobatch.
+   (*rewrite < H6.assumption*)
+   *)
   ]
 qed.
\ No newline at end of file