From c328a3c15e865515a56d1c1d6d0c2619245a60a0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 09:29:17 +0000 Subject: [PATCH] Some code that used to avoid a fixed bug removed. --- helm/matita/library/nat/orders.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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. -- 2.39.2