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 "basics/list.ma".
13 include "lambda-delta/xoa_defs.ma".
14 include "lambda-delta/xoa_notation.ma".
15 include "lambda-delta/notation.ma".
17 (* ARITHMETICAL PROPERTIES **************************************************)
19 lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
22 lemma minus_le: ∀m,n. m - n ≤ m.
25 lemma plus_plus_minus_m_m: ∀e1,e2,d. e1 ≤ e2 → d + e1 + (e2 - e1) = d + e2.
28 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → (m + n) - p = (m - p) + n.
29 #n #m #p #lepm @plus_to_minus <associative_plus
30 >(commutative_plus p) <plus_minus_m_m //
33 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
34 #m #n elim (decidable_lt m n) /3/
37 lemma lt_refl_false: ∀n. n < n → False.
38 #n #H elim (lt_to_not_eq … H) -H /2/
41 lemma lt_zero_false: ∀n. n < 0 → False.
42 #n #H elim (lt_to_not_le … H) -H /2/
45 lemma plus_lt_false: ∀m,n. m + n < m → False.
46 #m #n #H1 lapply (le_plus_n_r n m) #H2
47 lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
48 elim (lt_refl_false … H)
51 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
54 lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
57 lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
60 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
63 lemma arith5: ∀i,h,d. i + h ≤ d → d - i - h + (i + h) = d.
66 lemma arith6: ∀m,n. m < n → n - (n - m - 1) = m + 1.
67 #m #n #H >minus_plus <minus_minus //
70 lemma arith7: ∀i,d. i ≤ d → d - i + i = d.