X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=b23fb9de8280f4fe9efd714c1c4462a07956c4dc;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=93fb86d42e0f830e574a0cb685271bc2dc7637d3;hpb=1994fe8e6355243652770f53a02db5fdf26915f0;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 93fb86d42..b23fb9de8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -17,6 +17,14 @@ include "ground_2/lib/star.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 
+(* Iota equations ***********************************************************)
+
+lemma pred_O: pred 0 = 0.
+normalize // qed.
+
+lemma pred_S: ∀m. pred (S m) = m.
+// qed.
+
 (* Equations ****************************************************************)
 
 lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
@@ -168,6 +176,12 @@ let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
 
 interpretation "iterated function" 'exp op n = (iter n ? op).
 
+lemma iter_O: ∀B:Type[0]. ∀f:B→B.∀b. f^0 b = b.
+// qed.
+
+lemma iter_S: ∀B:Type[0]. ∀f:B→B.∀b,l. f^(S l) b = f (f^l b).
+// qed.
+
 lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
 #B #f #b #l >commutative_plus //
 qed.