+
+lemma nlt_inv_pred_bi (m) (n):
+ โm < โn โ m < n.
+/3 width=3 by nlt_inv_pred_dx, nle_nlt_trans/
+qed-.
+
+(* Constructions with npred *************************************************)
+
+lemma nlt_zero_sn (n): n = โโn โ ๐ < n.
+// qed.
+
+(*** monotonic_lt_pred *)
+lemma nlt_pred_bi (m) (n): ๐ < m โ m < n โ โm < โn.
+#m #n #Hm #Hmn
+@nle_inv_succ_bi
+<(nlt_des_gen โฆ Hm) -Hm
+<(nlt_des_gen โฆ Hmn) //
+qed.