Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matitaB / matita / lib / arithmetics / nat.ma

diff --git a/matitaB/matita/lib/arithmetics/nat.ma b/matitaB/matita/lib/arithmetics/nat.ma
index 6b3a1a19bf7b730af3e90aacec9d36b48a3d0289..6fa6d57a8e78b130ae818438e644254019bee790 100644 (file)
--- 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.