X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fgcd.ma;h=fdb1e8d9018dc5b877c52e93918894a6c43194f5;hb=2632e0520c373f191b81c3975385d77e71314ca7;hp=2bb22081fc2be6da6f4c8ec70ddc7193f01d4ed7;hpb=6e62c12e14cea178366801f8d5e47fc6adaf1200;p=helm.git

diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma
index 2bb22081f..fdb1e8d90 100644
--- a/matita/library/nat/gcd.ma
+++ b/matita/library/nat/gcd.ma
@@ -413,7 +413,7 @@ symmetric_gcd.
 
 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
 intros.
-apply (nat_case n).reflexivity.
+apply (nat_case n).apply le_n.
 intro.
 apply divides_to_le.
 apply lt_O_gcd.
@@ -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.