X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Farith_etc.txt;h=9de8f4ed3f04e5f07d3dc46a33d17563a50d02a6;hp=331e5a93900832a0020843e4ebfab9786b0e9a0a;hb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;hpb=77c9255de3c5f7780aeacd745703a1cc76328a68

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt b/matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt
index 331e5a939..9de8f4ed3 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt
@@ -41,21 +41,6 @@ qed-.
 
 (* Decidability of predicates ***********************************************)
 
-lemma dec_lt (R:predicate nat):
-      (∀n. Decidable … (R n)) →
-      ∀n. Decidable … (∃∃m. m < n & R m).
-#R #HR #n elim n -n [| #n * ]
-[ @or_intror * /2 width=2 by lt_zero_false/
-| * /4 width=3 by lt_S, or_introl, ex2_intro/
-| #H0 elim (HR n) -HR
-  [ /3 width=3 by or_introl, ex2_intro/
-  | #Hn @or_intror * #m #Hmn #Hm
-    elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
-    /4 width=3 by lt_S_S_to_lt, ex2_intro/
-  ]
-]
-qed-.
-
 lemma dec_min (R:predicate nat):
       (∀n. Decidable … (R n)) → ∀n. R n →
       ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).