- revision of ground_2 and basic_2

[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 93fb86d42e0f830e574a0cb685271bc2dc7637d3..b23fb9de8280f4fe9efd714c1c4462a07956c4dc 100644 (file)
--- 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.