From 1d5b162785294e62c1f35fe9698fe331172bb3ac Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 31 Mar 2010 10:29:30 +0000
Subject: [PATCH] removed boh

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>
---
 helm/software/matita/nlibrary/arithmetics/nat.ma | 3 ---
 1 file changed, 3 deletions(-)

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.
 
-- 
2.39.2