+
+(*** lt_elim *)
+lemma nlt_ind_alt (Q: relation2 nat nat):
+ (∀n. Q (𝟎) (↑n)) →
+ (∀m,n. m < n → Q m n → Q (↑m) (↑n)) →
+ ∀m,n. m < n → Q m n.
+#Q #IH1 #IH2 #m #n @(nat_ind_2_succ … n m) -m -n //
+[ #m #H
+ elim (nlt_inv_zero_dx … H)
+| /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-.