-(*** S_pred *)
-lemma nlt_inv_zero_sn (m): ๐ < m โ m = โโm.
-#m @(nat_ind โฆ m) -m //
-#H elim (nlt_inv_refl โฆ H)
+(*** lt_inv_gen *)
+lemma nlt_inv_gen (m) (n): m < n โ โงโง m โค โn & n = โโn.
+/2 width=1 by nle_inv_succ_sn/ qed-.
+
+(*** lt_inv_S1 *)
+lemma nlt_inv_succ_sn (m) (n): โm < n โ โงโง m < โn & n = โโn.
+/2 width=1 by nle_inv_succ_sn/ qed-.
+
+lemma nlt_inv_pred_dx (m) (n): m < โn โ โm < n.
+#m #n #H >(nlt_des_gen (๐) n)
+[ /2 width=1 by nlt_succ_bi/
+| /3 width=3 by nle_nlt_trans, nlt_nle_trans/
+]
+qed-.
+
+lemma nlt_inv_pred_bi (m) (n):
+ โm < โn โ m < n.
+/3 width=3 by nlt_inv_pred_dx, nle_nlt_trans/