X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fground.ma;h=72a1eaf294443850b6d0ba2b149e21095f4cf797;hb=78b1c68fca5f15000588a1e091149a188831977e;hp=3a04f0d17ba947d38d69899fea5a3cb9180d9e97;hpb=42680d47c033d751738fd0f84af7b45b2a91a5b8;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 3a04f0d17..72a1eaf29 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -12,3 +12,35 @@
 include "basics/list.ma".
 include "lambda-delta/notation.ma".
 
+(* ARITHMETICAL PROPERTIES **************************************************)
+
+lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
+// qed.
+
+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.
+
+lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → (m + n) - p = (m - p) + n.
+#n #m #p #lepm @plus_to_minus <associative_plus
+>(commutative_plus p) <plus_minus_m_m //
+qed.
+
+lemma lt_false: ∀n. n < n → False.
+#n #H lapply (lt_to_not_eq … H) -H #H elim H -H /2/
+qed.
+
+lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
+/2/ qed.
+
+lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
+/3/ qed.
+
+lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
+/3/ qed.
+
+lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
+/2/ qed.