+(*** 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 le_nlt_trans, nlt_le_trans/
+]