X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=6fa6d57a8e78b130ae818438e644254019bee790;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hp=6b3a1a19bf7b730af3e90aacec9d36b48a3d0289;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/matita/lib/arithmetics/nat.ma b/matitaB/matita/lib/arithmetics/nat.ma
index 6b3a1a19b..6fa6d57a8 100644
--- a/matitaB/matita/lib/arithmetics/nat.ma
+++ b/matitaB/matita/lib/arithmetics/nat.ma
@@ -22,7 +22,7 @@ alias num (instance 0) = "natural number".
 definition pred ≝
  λn. match n with [ O ⇒ O | S p ⇒ p].
 
-theorem pred_Sn : ∀n. n = pred (S n).
+theorem pred_Sn : ∀n.n = pred (S n).
 // qed.
 
 theorem injective_S : injective nat nat S.
@@ -76,7 +76,7 @@ theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
 // qed.
 *)
 
-theorem plus_n_O: ∀n:nat. n = n+O.
+theorem plus_n_O: ∀n:nat. n = n+0.
 #n (elim n) normalize // qed.
 
 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.