2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/nat.ma".
14 (* ARITHMETICAL PROPERTIES **************************************************)
16 lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
17 #n #m <plus_n_Sm #H destruct
20 lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
21 #n #m #p <plus_n_Sm #H @(lt_to_le_to_lt … H) //
24 lemma minus_le: ∀m,n. m - n ≤ m.
27 lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
30 lemma lt_to_le: ∀a,b. a < b → a ≤ b.
33 lemma lt_refl_false: ∀n. n < n → False.
34 #n #H elim (lt_to_not_eq … H) -H /2/
37 lemma lt_zero_false: ∀n. n < 0 → False.
38 #n #H elim (lt_to_not_le … H) -H /2/
41 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
42 #m #n elim (decidable_lt m n) /3/
45 lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
49 lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
52 lemma plus_lt_false: ∀m,n. m + n < m → False.
53 #m #n #H1 lapply (le_plus_n_r n m) #H2
54 lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
55 elim (lt_refl_false … H)
58 lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
60 @lt_plus_to_minus_r <plus_minus_m_m //.
63 lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
66 lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
69 lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
72 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
73 #n #m #p #lepm @plus_to_minus <associative_plus
74 >(commutative_plus p) <plus_minus_m_m //
77 lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
79 [ #c #a #H >(le_O_to_eq_O … H) -H //
80 | #b #IHb #c elim c -c //
82 lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
83 <plus_n_Sm normalize /2/
87 lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
90 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
93 lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c).
96 lemma plus_minus_m_m_comm: ∀n,m. m ≤ n → n = m + (n - m).
99 theorem minus_plus_m_m_comm: ∀n,m. n = (m + n) - m.
102 lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
105 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
106 #a #b #c1 #H >minus_plus @eq_f2 /2/
109 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
110 #a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2/
113 lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b.
116 lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
117 #x #a #b #c1 >plus_plus_comm_23 //
120 lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b.
123 lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a.
126 lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b.
127 #a #b #c1 #H >minus_plus <minus_minus //
130 lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b.
133 lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
134 a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
135 #a1 #a2 #b #c1 #H1 #H2 <le_plus_minus_comm /2/
138 lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
141 (* unstable *****************************************************************)
143 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
146 lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
147 #j #i #e #d #H lapply (plus_le_minus … H) -H /2/
150 lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1.
153 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
156 lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
157 #a #b1 #b2 #c1 #H1 #H2 #H3
158 <le_plus_minus_comm // @monotonic_lt_minus_l //
161 lemma arith8: ∀a,b. a < a + b + 1.
164 lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
167 lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
169 >minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //