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_plus.ma".
16 include "ground/arith/nat_le.ma".
18 (* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
20 (* Constructions with nplus *************************************************)
22 (*** monotonic_le_plus_l *)
23 lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.
24 #m #n1 #n2 #H elim H -n2 /2 width=3 by nle_trans/
27 (*** monotonic_le_plus_r *)
28 lemma nle_plus_bi_sn (m) (n1) (n2): n1 ≤ n2 → m + n1 ≤ m + n2.
29 #m #n1 #n2 #H <nplus_comm <nplus_comm in ⊢ (??%);
30 /2 width=1 by nle_plus_bi_dx/
34 lemma nle_plus_dx_dx_refl (m) (n): m ≤ m + n.
35 /2 width=1 by nle_plus_bi_sn/ qed.
38 lemma nle_plus_dx_sn_refl (m) (n): m ≤ n + m.
39 /2 width=1 by nle_plus_bi_sn/ qed.
42 lemma nle_plus_dx_sn (o) (m) (n): n ≤ m → n ≤ o + m.
43 /2 width=3 by nle_trans/ qed.
46 lemma nle_plus_dx_dx (o) (m) (n): n ≤ m → n ≤ m + o.
47 /2 width=3 by nle_trans/ qed.
49 (* Main constructions with nplus ********************************************)
52 theorem nle_plus_bi (m1) (m2) (n1) (n2):
53 m1 ≤ m2 → n1 ≤ n2 → m1 + n1 ≤ m2 + n2.
54 /3 width=3 by nle_plus_bi_dx, nle_plus_bi_sn, nle_trans/ qed.
56 (* Inversions with nplus ****************************************************)
59 lemma nle_inv_plus_sn_dx (m) (n) (o): n + o ≤ m → n ≤ m.
60 /2 width=3 by nle_trans/ qed.
63 lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
64 /3 width=1 by nle_inv_zero_dx, eq_inv_zero_nplus/ qed-.
66 (*** le_plus_to_le_r *)
67 lemma nle_inv_plus_bi_dx (o) (m) (n): n + o ≤ m + o → n ≤ m.
68 #o @(nat_ind_succ … o) -o /3 width=1 by nle_inv_succ_bi/
72 lemma nle_inv_plus_bi_sn (o) (m) (n): o + n ≤ o + m → n ≤ m.
73 /2 width=2 by nle_inv_plus_bi_dx/ qed-.
75 (* Destructions with nplus **************************************************)
77 (*** plus2_le_sn_sn *)
78 lemma nplus_2_des_le_sn_sn (m1) (m2) (n1) (n2):
79 m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
80 #m1 #m2 #n1 #n2 #H #Hm
81 lapply (nle_plus_bi_dx n1 … Hm) -Hm >H -H
82 /2 width=2 by nle_inv_plus_bi_sn/
85 (*** plus2_le_sn_dx *)
86 lemma nplus_2_des_le_sn_dx (m1) (m2) (n1) (n2):
87 m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
88 #m1 #m2 #n1 #n2 <nplus_comm in ⊢ (???%→?);
89 /2 width=4 by nplus_2_des_le_sn_sn/ qed-.
91 (*** plus2_le_dx_sn *)
92 lemma nplus_2_des_le_dx_sn (m1) (m2) (n1) (n2):
93 n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
94 #m1 #m2 #n1 #n2 <nplus_comm in ⊢ (??%?→?);
95 /2 width=4 by nplus_2_des_le_sn_sn/ qed-.
97 (*** plus2_le_dx_dx *)
98 lemma nplus_2_des_le_dx_dx (m1) (m2) (n1) (n2):
99 n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
100 #m1 #m2 #n1 #n2 <nplus_comm in ⊢ (??%?→?);
101 /2 width=4 by nplus_2_des_le_sn_dx/ qed-.