]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/nat/gcd.ma
files with newest objects (to be included in the respective developments)
[helm.git] / helm / software / matita / library / nat / gcd.ma
index 6ce4f538e4b794331399e6d719a8bca0b7e25db9..fdb1e8d9018dc5b877c52e93918894a6c43194f5 100644 (file)
@@ -520,7 +520,7 @@ cut (n \divides p \lor n \ndivides p)
           elim H1.rewrite > H6.
           (* applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
              reflexivity. *);
-          applyS (witness n ? ? (refl_eq ? ?)).
+          applyS (witness n ? ? (refl_eq ? ?)) timeout=50.
           (*
           rewrite < (sym_times n).rewrite < assoc_times.
           rewrite > (sym_times q).rewrite > assoc_times.