X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fground.ma;h=f4279588b251aa360158fab7826fc6f3b4abbc19;hb=95aa0f13b906e2b145c60bde078b752869976e7f;hp=651c2dd99eeffa3e62032ec6d88a476c4a6d071e;hpb=861d99cbe515be1a8e6ca204c2cafa40ccdec8a3;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 651c2dd99..f4279588b 100644
--- 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.