X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=dfc61de151fa83e058f234f30fdc0f2438d0dd1b;hp=e3ec5c5040847cd64f141efd9aede61dcee4f658;hb=ede00573e3e4cb28df7ca9a5dae6228c2b432608;hpb=1083ac3b1acac5f1ac1fa40a9a417dd9d268dced

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index e3ec5c504..dfc61de15 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -60,9 +60,11 @@ lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
 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.
+lemma arith_l (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
+* // qed.
+
+lemma arith_l_eq: ∀x. 1 = 1-x+(x-(x-1)).
+// 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.