From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 31 Mar 2010 10:29:30 +0000 (+0000)
Subject: removed boh
X-Git-Tag: make_still_working~2952
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d5b162785294e62c1f35fe9698fe331172bb3ac;p=helm.git

removed boh

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>
---

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.