+
+lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
+/2 width=4 by le_plus_xySz_x_false/ qed-.
+
+(* iterators ****************************************************************)
+
+(* Note: see also: lib/arithemetcs/bigops.ma *)
+let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
+ match n with
+ [ O ⇒ nil
+ | S k ⇒ op (iter k B op nil)
+ ].
+
+interpretation "iterated function" 'exp op n = (iter n ? op).
+
+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.
+
+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.