+
+(*** 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_succ_2 … n m) -m -n //
+[ #m #H
+ elim (nlt_inv_zero_dx … H)
+| /4 width=1 by nlt_inv_succ_bi/
+]
+qed-.