X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnat.ma;h=e36c1beaa95303f52e693f11e4ac7f3d913b6928;hb=aeb7f0539398561dc84cadf38df14a051dd1ba75;hp=c85bb25c2c04faf4ace9c21e65527f89d6536331;hpb=da83446deba30fbe32b9bf617d83bd22cc9c9770;p=helm.git

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index c85bb25c2..e36c1beaa 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -14,9 +14,6 @@
 
 set "baseuri" "cic:/matita/nat/nat".
 
-include "logic/equality.ma".
-include "logic/connectives.ma".
-include "datatypes/bool.ma".
 include "higher_order_defs/functions.ma".
 
 inductive nat : Set \def
@@ -29,7 +26,7 @@ definition pred: nat \to nat \def
 | (S p) \Rightarrow p ].
 
 theorem pred_Sn : \forall n:nat.n=(pred (S n)).
-intros; reflexivity.
+intros. reflexivity.
 qed.
 
 theorem injective_S : injective nat nat S.
@@ -44,7 +41,7 @@ theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
 \def injective_S.
 
 theorem not_eq_S  : \forall n,m:nat. 
-\lnot n=m \to \lnot (S n = S m).
+\lnot n=m \to S n \neq S m.
 intros. simplify. intros.
 apply H. apply injective_S. assumption.
 qed.
@@ -55,14 +52,14 @@ definition not_zero : nat \to Prop \def
   [ O \Rightarrow False
   | (S p) \Rightarrow True ].
 
-theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
+theorem not_eq_O_S : \forall n:nat. O \neq S n.
 intros. simplify. intros.
 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.
 qed.
 
-theorem not_eq_n_Sn : \forall n:nat. \lnot n=S n.
+theorem not_eq_n_Sn : \forall n:nat. n \neq S n.
 intros.elim n.
 apply not_eq_O_S.
 apply not_eq_S.assumption.
@@ -100,7 +97,7 @@ intro.elim n1.
 left.reflexivity.
 right.apply not_eq_O_S.
 intro.right.intro.
-apply not_eq_O_S n1 ?.
+apply not_eq_O_S n1.
 apply sym_eq.assumption.
 intros.elim H.
 left.apply eq_f. assumption.