matita/matita/lib/lambda-delta/ground.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  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".
  16
  17 (* ARITHMETICAL PROPERTIES **************************************************)
  18
  19 lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
  20 // qed.
  21
  22 lemma minus_le: ∀m,n. m - n ≤ m.
  23 /2/ qed.
  24
  25 lemma plus_plus_minus_m_m: ∀e1,e2,d. e1 ≤ e2 → d + e1 + (e2 - e1) = d + e2.
  26 /2/ qed.
  27
  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 //
  31 qed.
  32
  33 lemma lt_false: ∀n. n < n → False.
  34 #n #H lapply (lt_to_not_eq … H) -H #H elim H -H /2/
  35 qed.
  36
  37 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
  38 /2/ qed.
  39
  40 lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
  41 /3/ qed.
  42
  43 lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
  44 /3/ qed.
  45
  46 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
  47 /2/ qed.
  48
  49 lemma arith5: ∀i,h,d. i + h ≤ d → d - i - h + (i + h) = d.
  50 /2/ qed.