+(* Advanced eliminations ****************************************************)
+
+(*** le_elim *)
+lemma nle_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 … m n) -m -n //
+[ #m #H elim (nle_inv_succ_zero … H)
+| /4 width=1 by nle_inv_succ_bi/
+]
+qed-.
+
+(* Advanced constructions ***************************************************)
+