(* *)
(**************************************************************************)
-include "ground/arith/nat_pred_succ.ma".
+include "ground/arith/nat_le_pred.ma".
include "ground/arith/nat_lt.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
-(* Basic constructions with pred ********************************************)
+(* Constructions with npred *************************************************)
lemma nlt_zero_sn (m): m = ↑↓m → 𝟎 < m.
// qed.
-(* Basic inversions with pred ***********************************************)
+(* Inversions with npred ****************************************************)
(*** 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-.