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 a162df9a3c418a6ca0761b64bbf44da513bda072..1731f2bc2e8ac3973d28255d61c04be3df060e36 100644 (file)
--- 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.