]> matita.cs.unibo.it Git - helm.git/commitdiff
other simplifications.
authorCristian Armentano <??>
Sun, 9 Sep 2007 13:45:27 +0000 (13:45 +0000)
committerCristian Armentano <??>
Sun, 9 Sep 2007 13:45:27 +0000 (13:45 +0000)
matita/library/nat/gcd_properties1.ma

index ad5cb2c6b7623cb86123eadbacfba80e24f6c63d..94aa67670aa07ac780712a2d3983097ed00d8f4b 100644 (file)
@@ -256,7 +256,7 @@ apply (nat_case1 a)
 [ intros.
   apply (nat_case1 b)
   [ intros.
-    cut (d = O)
+    cut (d = O) (*this is an impossible case*)
     [ rewrite > Hcut.
       simplify.
       apply divides_SO_n