X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=0cbcff85e6ce1daec44d6f56fe0f3b32ed52a322;hb=b3f8b89278d193ed0aa0f39e7f8d74cf1de81d8d;hp=732c1b64ca426f9c15c80f2375cd0efb293873ec;hpb=c9a1672c725945b47f9ea8af3c23b67cf9026f01;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 732c1b64c..0cbcff85e 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -134,6 +134,10 @@ lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b).
 #B #f #b #l elim l -l normalize //
 qed.
 
+lemma iter_plus: ∀B:Type[0]. ∀f:B→B. ∀b,l1,l2. f^(l1+l2) b = f^l1 (f^l2 b).
+#B #f #b #l1 elim l1 -l1 normalize //
+qed.
+
 (* Trichotomy operator ******************************************************)
 
 (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)