X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_lt.ma;h=4cfdfbacda75c0ce3e16bb77c56d3184a144e8ae;hp=0abb785f77f2966800665ace1bad20baceb18c68;hb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;hpb=77c9255de3c5f7780aeacd745703a1cc76328a68

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
index 0abb785f7..4cfdfbacd 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
@@ -149,3 +149,22 @@ lemma nlt_ind_alt (Q: relation2 nat nat):
 | /4 width=1 by nlt_inv_succ_bi/
 ]
 qed-.
+
+(* Advanced constructions (decidability) ************************************)
+
+(*** dec_lt *)
+lemma dec_nlt (R:predicate nat):
+      (∀n. Decidable … (R n)) →
+      ∀n. Decidable … (∃∃m. m < n & R m).
+#R #HR #n @(nat_ind_succ … n) -n [| #n * ]
+[ @or_intror * /2 width=2 by nlt_inv_zero_dx/
+| * /4 width=3 by nlt_succ_dx_trans, ex2_intro, or_introl/
+| #H0 elim (HR n) -HR
+  [ /3 width=3 by or_introl, ex2_intro/
+  | #Hn @or_intror * #m #Hmn #Hm
+    elim (nle_split_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
+    [ /4 width=3 by nlt_inv_succ_bi, ex2_intro/
+    | lapply (eq_inv_nsucc_bi … H) -H /2 width=1 by/
+  ]
+]
+qed-.