frees_drops completed!

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / arith.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index f86f7a3bd75b1ca4532acfa39c2829a704335c9f..8ce8b954c1bd353ce1d1e6f7ddf8e2411a863337 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -35,6 +35,9 @@ normalize // qed.
 lemma pred_S: ∀m. pred (S m) = m.
 // qed.
 
+lemma plus_S1: ∀x,y. ⫯(x+y) = (⫯x) + y.
+// qed.
+
 lemma max_O1: ∀n. n = (0 ∨ n).
 // qed.