Adapted to new applyS.

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 3771bb6e56be891b628ed7991347ef2b63f5b92e..b970fb0c3ba1b1f1096cead8eb4951f1f2dafa87 100644 (file)
--- 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.