ground_2 released and permanently renamed as ground

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / etc / lib / arith.etc

diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
deleted file mode 100644 (file)
index 11ef739..0000000
--- a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
+++ /dev/null
@@ -1,36 +0,0 @@
-
-lemma zero_or_gt: ∀n. n = 0 ∨ 0 < n.
-#n elim (lt_or_eq_or_gt 0 n) /2/
-#H elim (lt_zero_false … H)
-qed. 
-
-lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z.
-/3 width=2/
-
-lemma arith_b1x: ∀e,x1,x2,y. y ≤ x2 → x2 ≤ x1 → 
-                 e + (x1 - y) - (x2 - y) = e + (x1 - x2).
-#e #x1 #x2 #y #H1 #H2
-<(arith_b1 … H1) >le_plus_minus // /2 width=1/
-qed-.
-                
-lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w.
-#x #y #z #w #H <le_plus_minus_comm // /3 width=1 by lt_to_le, le_plus_a/
-qed-.
-
-lemma lt_dec: ∀n2,n1. Decidable (n1 < n2).
-#n2 elim n2 -n2
-[ /4 width=3 by or_intror, absurd, nmk/
-| #n2 #IHn2 * /2 width=1 by or_introl/
-  #n1 elim (IHn2 n1) -IHn2
-  /4 width=1 by le_S_S, monotonic_pred, or_intror, or_introl/
-]
-qed-.
-
-lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
-#x #y #H elim (decidable_lt x y) /2 width=1 by not_lt_to_le/
-#Hxy elim (H Hxy)
-qed-.
-
-lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y.
-#x #y #Hxy >minus_minus [|*: // ] <minus_Sn_n //
-qed-.