X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2Fnat.ma;h=9c420f9ec492e532cebae13dcd72fe76b5087c84;hb=65e8f1ba961ef81c5604168e7f1c891063c1ec76;hp=d4ba1135e241626f551b5bca4b55c0a43f7d01e5;hpb=2e6a92bad35a8f8883c498c6a2f36ea3208d4ddd;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index d4ba1135e..9c420f9ec 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -53,9 +53,10 @@ ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
 ndefinition not_zero: nat → Prop ≝
  λn: nat. match n with
   [ O ⇒ False | (S p) ⇒ True ].
-
+  
 ntheorem not_eq_O_S : ∀n:nat. O ≠ S n.
-#n; napply nmk; #eqOS; nchange with (not_zero O); nrewrite > eqOS; //.
+#n; napply nmk; #eqOS; nchange with (not_zero O); 
+nrewrite > eqOS; //.
 nqed.
 
 ntheorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
@@ -488,7 +489,7 @@ nelim n;
  ##[#q; #HleO; (* applica male *) 
     napply (le_n_O_elim ? HleO);
     napply H; #p; #ltpO;
-    napply False_ind; /2/; (* 3 *)
+    napply (False_ind ??); /2/; (* 3 *)
  ##|#p; #Hind; #q; #HleS; 
     napply H; #a; #lta; napply Hind;
     napply le_S_S_to_le;/2/;