demodulate takes an extra argument 'all', if present it attempts to solve

[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 3771bb6e56be891b628ed7991347ef2b63f5b92e..958fddf970207216bfcab426a8389e202a942786 100644 (file)
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -761,11 +761,8 @@ 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 *).
+          pump 39.
+          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).          
           (*
           rewrite < (sym_times n).rewrite < assoc_times.
           rewrite > (sym_times q).rewrite > assoc_times.
@@ -780,11 +777,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 +882,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.