From: Matthias Puech <puech@cs.mcgill.ca>
Date: Tue, 23 Mar 2010 18:24:49 +0000 (+0000)
Subject: typo in a proof
X-Git-Tag: make_still_working~2976
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=375a7d0e4c11f3b09d33b9dd24f1da7f7b442885;p=helm.git

typo in a proof

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

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.