X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=b970fb0c3ba1b1f1096cead8eb4951f1f2dafa87;hb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;hp=3771bb6e56be891b628ed7991347ef2b63f5b92e;hpb=4ab6e0f7956b870227c6986ea800c1c6a3332565;p=helm.git

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 3771bb6e5..b970fb0c3 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -761,10 +761,6 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
           elim H1.
-          (*
-             rewrite > H6.
-             applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
-             reflexivity. *);
           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
           (*
           rewrite < (sym_times n).rewrite < assoc_times.
@@ -780,11 +776,14 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
           elim H1.rewrite > H6.
+          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
+          (*
           rewrite < sym_times.rewrite > assoc_times.
           rewrite < (assoc_times q).
           rewrite < (sym_times n).
           rewrite < distr_times_minus.
           apply (witness ? ? (n1*a1-q*a)).reflexivity
+          *)
         ](* end second case *)
      |rewrite < (prime_to_gcd_SO n p)
        [apply eq_minus_gcd|assumption|assumption
@@ -882,14 +881,14 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > distr_times_minus.
           rewrite > (sym_times p (a1*m)).
           rewrite > (assoc_times a1).
-          elim H2.
+          elim H2.rewrite > H7. 
           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
          |(* second case *)
           rewrite > (times_n_SO p).rewrite < H6.
           rewrite > distr_times_minus.
           rewrite > (sym_times p (a1*m)).
           rewrite > (assoc_times a1).
-          elim H2.
+          elim H2.rewrite > H7.
           applyS (witness n ? ? (refl_eq ? ?)).
         ](* end second case *)
      |rewrite < H1.apply eq_minus_gcd.