From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Sep 2005 09:29:17 +0000 (+0000)
Subject: Some code that used to avoid a fixed bug removed.
X-Git-Tag: LAST_BEFORE_NEW~106
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c328a3c15e865515a56d1c1d6d0c2619245a60a0;p=helm.git

Some code that used to avoid a fixed bug removed.
---

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index a162df9a3..1731f2bc2 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -173,8 +173,8 @@ qed.
 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
 intro.elim n.reflexivity.
 apply False_ind.
-(* non si applica not_le_Sn_O *)
-apply  (not_le_Sn_O ? H1).
+apply not_le_Sn_O.
+goal 17. apply H1.
 qed.
 
 theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.