1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/arith/nat_le_plus.ma".
16 include "ground/arith/nat_lt.ma".
18 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
20 (* Constructions with nplus *************************************************)
22 (*** monotonic_lt_plus_l *)
23 lemma nlt_plus_bi_dx (m) (n1) (n2): n1 < n2 → n1 + m < n2 + m.
25 @nlt_i >nplus_succ_sn /2 width=1 by nle_plus_bi_dx/
28 (*** monotonic_lt_plus_r *)
29 lemma nlt_plus_bi_sn (m) (n1) (n2): n1 < n2 → m + n1 < m + n2.
31 @nlt_i >nplus_succ_dx /2 width=1 by nle_plus_bi_sn/
34 (*** lt_plus_Sn_r *) (**)
35 lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
38 (* Inversions with nplus ****************************************************)
40 (*** lt_plus_to_lt_l *)
41 lemma nlt_inv_plus_bi_dx (m) (n1) (n2): n1 + m < n2 + m → n1 < n2.
42 /2 width=2 by nle_inv_plus_bi_dx/ qed-.
44 (*** lt_plus_to_lt_r *)
45 lemma nlt_inv_plus_bi_sn (m) (n1) (n2): m + n1 < m + n2 → n1 < n2.
46 /2 width=2 by nle_inv_plus_bi_sn/ qed-.