X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=932f95de21eb441d4897083156538eb71c282a67;hb=b634a816745cf8a9a7ad14650d088232c8ee1a1a;hp=dde95e8a7267d844ab844a0861e9ce1a044b480f;hpb=cc600ed1e115d5566947288d532a1e89d989227f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index dde95e8a7..932f95de2 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -57,6 +57,13 @@ lemma plus_SO: ∀n. n + 1 = ↑n.
 lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
 // qed-.
 
+lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
+// qed.
+
+lemma arith_l: ∀x. 1 = 1-x+(x-(x-1)).
+* // #x >minus_S_S >minus_S_S <minus_O_n <minus_n_O //
+qed.
+
 (* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
 lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
 #x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
@@ -69,9 +76,6 @@ qed-.
 fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
 /2 width=1 by plus_minus_minus_be/ qed-.
 
-lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
-// qed.
-
 lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
 /2 by plus_minus/ qed-.