removed boh

[helm.git] / helm / software / matita / nlibrary / arithmetics / nat.ma

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index f15f8cbc858becfb524e6259b644cf6a7b841230..d4ba1135e241626f551b5bca4b55c0a43f7d01e5 100644 (file)
--- 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.