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_minus_plus.ma".
16 include "ground/arith/ynat_lminus_plus.ma".
17 include "ground/arith/ynat_le_plus.ma".
18 include "ground/arith/ynat_le_lminus.ma".
20 (* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
22 (* Constructions with ylminus and yplus *************************************)
24 (*** yle_plus1_to_minus_inj2 *)
25 lemma yle_plus_sn_dx_lminus_dx (n) (x) (z):
26 x + yinj_nat n ≤ z → x ≤ z - n.
28 lapply (yle_lminus_bi_dx n … H) -H //
31 (*** yle_plus1_to_minus_inj1 *)
32 lemma yle_plus_sn_sn_lminus_dx (n) (x) (z):
33 yinj_nat n + x ≤ z → x ≤ z - n.
34 /2 width=1 by yle_plus_sn_dx_lminus_dx/ qed.
36 (*** yle_plus2_to_minus_inj2 *)
37 lemma yle_plus_dx_dx_lminus_sn (o) (x) (y):
38 x ≤ y + yinj_nat o → x - o ≤ y.
39 /2 width=1 by yle_lminus_bi_dx/ qed.
41 (*** yle_plus2_to_minus_inj1 *)
42 lemma yle_plus_dx_sn_lminus_sn (o) (x) (y):
43 x ≤ yinj_nat o + y → x - o ≤ y.
44 /2 width=1 by yle_plus_dx_dx_lminus_sn/ qed.
46 (* Destructions with ylminus and yplus **************************************)
48 (*** yplus_minus_comm_inj *)
49 lemma ylminus_plus_comm_23 (n) (x) (z):
50 yinj_nat n ≤ x → x - n + z = x + z - n.
51 #n #x @(ynat_split_nat_inf … x) -x //
52 #m #z #Hnm @(ynat_split_nat_inf … z) -z
53 [ #o <ylminus_inj_sn <yplus_inj_bi <yplus_inj_bi <ylminus_inj_sn
54 <nminus_plus_comm_23 /2 width=1 by yle_inv_inj_bi/
55 | <yplus_inf_dx <yplus_inf_dx //
59 (*** yplus_minus_assoc_inj *)
60 lemma yplus_lminus_assoc (o) (x) (y):
61 yinj_nat o ≤ y → x + y - o = x + (y - o).
62 #o #x @(ynat_split_nat_inf … x) -x //
63 #m #y @(ynat_split_nat_inf … y) -y
64 [ #n #Hon <ylminus_inj_sn <yplus_inj_bi <yplus_inj_bi
65 <nplus_minus_assoc /2 width=1 by yle_inv_inj_bi/
66 | #_ <ylminus_inf_sn //
70 (*** yplus_minus_assoc_comm_inj *)
71 lemma ylminus_assoc_comm_23 (n) (o) (x):
72 n ≤ o → x + yinj_nat n - o = x - (o - n).
73 #n #o #x @(ynat_split_nat_inf … x) -x
74 [ #m #Hno <ylminus_inj_sn <yplus_inj_bi <ylminus_inj_sn
75 <nminus_assoc_comm_23 //
76 | #_ <ylminus_inf_sn <yplus_inf_sn //
80 (* Inversions with ylminus and yplus ****************************************)
83 lemma yplus_lminus_sn_refl_sn (n) (x):
84 yinj_nat n ≤ x → x = x - n + yinj_nat n.
85 /2 width=1 by ylminus_plus_comm_23/ qed-.
87 lemma yplus_lminus_dx_refl_sn (n) (x):
88 yinj_nat n ≤ x → x = yinj_nat n + (x - n).
89 /2 width=1 by yplus_lminus_sn_refl_sn/ qed-.
91 (*** yplus_inv_minus *)
92 lemma eq_inv_yplus_bi_inj_md (n1) (m2) (x1) (y2):
93 yinj_nat n1 ≤ x1 → x1 + yinj_nat m2 = yinj_nat n1 + y2 →
94 ∧∧ x1 - n1 = y2 - m2 & yinj_nat m2 ≤ y2.
95 #n1 #m2 #x1 #y2 #Hnx1 #H12
96 lapply (yle_plus_bi_dx (yinj_nat m2) … Hnx1) >H12 #H
97 lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2
98 generalize in match H12; -H12 (* * rewrite in hyp *)
99 >(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
100 lapply (eq_inv_yplus_bi_dx_inj … H) -H
101 >(yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H
102 lapply (eq_inv_yplus_bi_sn_inj … H) -H #H12
106 (*** yle_inv_plus_inj2 yle_inv_plus_inj_dx *)
107 lemma yle_inv_plus_sn_inj_dx (n) (x) (z):
109 ∧∧ x ≤ z - n & yinj_nat n ≤ z.
110 /3 width=3 by yle_plus_sn_dx_lminus_dx, yle_trans, conj/
113 (*** yle_inv_plus_inj1 *)
114 lemma yle_inv_plus_sn_inj_sn (n) (x) (z):
116 ∧∧ x ≤ z - n & yinj_nat n ≤ z.
117 /2 width=1 by yle_inv_plus_sn_inj_dx/ qed-.