From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 16 Mar 2009 12:40:32 +0000 (+0000)
Subject: Adapted to new applyS.
X-Git-Tag: make_still_working~4150
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7de49ed6d5606e958fb00ec48bef43877dd2039a;p=helm.git

Adapted to new applyS.
---

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.