X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2Fnat.ma;h=d4ba1135e241626f551b5bca4b55c0a43f7d01e5;hb=fa0d5a79683ea3966f62b21be7e1a3e274597911;hp=f15f8cbc858becfb524e6259b644cf6a7b841230;hpb=285a66d7ab69b1cb4b060cc9d8e4f1953095759e;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index f15f8cbc8..d4ba1135e 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -257,9 +257,6 @@ ntheorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
 ntheorem le_O_n : ∀n:nat. O ≤ n.
 #n; nelim n; /2/; nqed.
 
-ntheorem nboh: 0 ≤ 0 + 0.
-//; nqed.
-
 ntheorem le_n_Sn : ∀n:nat. n ≤ S n.
 /2/; nqed.