reductions rules and one lemma

[helm.git] / matita / matita / lib / lambda-delta / ground.ma

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 651c2dd99eeffa3e62032ec6d88a476c4a6d071e..f4279588b251aa360158fab7826fc6f3b4abbc19 100644 (file)
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -22,7 +22,6 @@ lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
 lemma minus_le: ∀m,n. m - n ≤ m.
 /2/ qed.
 
-
 lemma plus_plus_minus_m_m: ∀e1,e2,d. e1 ≤ e2 → d + e1 + (e2 - e1) = d + e2.
 /2/ qed.
 
@@ -46,3 +45,6 @@ lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
 
 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
 /2/ qed.
+
+lemma arith5: ∀i,h,d. i + h ≤ d → d - i - h + (i + h) = d.
+/2/ qed.