+
+(* 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.