(* *)
(**************************************************************************)
-include "ground/arith/nat_pred_succ.ma".
+include "ground/arith/nat_le_pred.ma".
include "ground/arith/nat_lt.ma".
(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
(*** S_pred *)
lemma nlt_inv_zero_sn (m): 𝟎 < m → m = ↑↓m.
-#m @(nat_ind … m) -m //
+#m @(nat_ind_succ … m) -m //
#H elim (nlt_inv_refl … H)
qed-.
+
+lemma nlt_inv_pred_dx (m) (n): m < ↓n → ↑m < n.
+#m #n #H >(nlt_inv_zero_sn n)
+[ /2 width=1 by nlt_succ_bi/
+| /3 width=3 by le_nlt_trans, nlt_le_trans/
+]
+qed-.