include "ground/arith/nat_le_plus.ma".
include "ground/arith/nat_lt.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
-(* Basic constructions with plus ********************************************)
+(* Constructions with nplus *************************************************)
(*** monotonic_lt_plus_l *)
lemma nlt_plus_bi_dx (m) (n1) (n2): n1 < n2 → n1 + m < n2 + m.
lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
/2 width=1/ qed-.
-(* Basic inversions with plus ***********************************************)
+(* Inversions with nplus ****************************************************)
(*** lt_plus_to_lt_l *)
lemma nlt_inv_plus_bi_dx (m) (n1) (n2): n1 + m < n2 + m → n1 < n2.