1. some "try ... with _ " removed

[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 2bb22081fc2be6da6f4c8ec70ddc7193f01d4ed7..6ce4f538e4b794331399e6d719a8bca0b7e25db9 100644 (file)
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/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.