matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc

   1
   2 lemma zero_or_gt: ∀n. n = 0 ∨ 0 < n.
   3 #n elim (lt_or_eq_or_gt 0 n) /2/
   4 #H elim (lt_zero_false … H)
   5 qed.
   6
   7 lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z.
   8 /3 width=2/
   9
  10 lemma arith_b1x: ∀e,x1,x2,y. y ≤ x2 → x2 ≤ x1 →
  11                  e + (x1 - y) - (x2 - y) = e + (x1 - x2).
  12 #e #x1 #x2 #y #H1 #H2
  13 <(arith_b1 … H1) >le_plus_minus // /2 width=1/
  14 qed-.
  15
  16 lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w.
  17 #x #y #z #w #H <le_plus_minus_comm // /3 width=1 by lt_to_le, le_plus_a/
  18 qed-.