- natural numbers with infinity for lambdadelta

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 7d6f5dda47e7fbb0de2ed1151781f919c74146f2..732c1b64ca426f9c15c80f2375cd0efb293873ec 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -28,6 +28,9 @@ lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
 /2 by plus_minus/ qed.
 
+lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x.
+// qed.
+
 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
 #a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
 qed.
@@ -44,6 +47,31 @@ lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
 #a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/
 qed.
 
+lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
+/2 width=1 by plus_minus/ qed-.
+
+(* Properties ***************************************************************)
+
+lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
+/3 width=1 by monotonic_le_minus_l/ qed.
+
+lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
+/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
+
+lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1.
+#z #x #y #n #Hzx #Hxny
+>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
+>plus_minus [2: /2 width=1 by lt_to_le/ ]
+/2 width=1 by monotonic_le_minus_l2/
+qed.
+
+lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n.
+#z #x #y #n #Hzx #Hyxn
+>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
+>plus_minus [2: /2 width=1 by lt_to_le/ ]
+/2 width=1 by monotonic_le_minus_l2/
+qed.
+
 (* Inversion & forward lemmas ***********************************************)
 
 axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
@@ -69,6 +97,10 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
 #Hxy elim (H Hxy)
 qed-.
 
+lemma pred_inv_refl: ∀m. pred m = m → m = 0.
+* // normalize #m #H elim (lt_refl_false m) //
+qed-.
+
 lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
 #y #z #x elim x -x
 [ #H lapply (le_n_O_to_eq … H) -H