From 375a7d0e4c11f3b09d33b9dd24f1da7f7b442885 Mon Sep 17 00:00:00 2001
From: Matthias Puech <puech@cs.mcgill.ca>
Date: Tue, 23 Mar 2010 18:24:49 +0000
Subject: [PATCH] typo in a proof

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>
---
 helm/software/matita/nlibrary/arithmetics/nat.ma | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index 4f1f65411..1ef6a81cb 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -454,7 +454,7 @@ ntheorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
 
 ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
 napply nat_elim2; 
-##[#n; #H1; #H2; /4/;
+#n; #H1; #H2; /4/;
  nqed. 
 
 ntheorem lt_O_S : ∀n:nat. O < S n.
-- 
2.39.2