aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Wf_nat.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/Wf_nat.v')
-rw-r--r--theories/Arith/Wf_nat.v19
1 files changed, 19 insertions, 0 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 5e7ee4153..e87901080 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -257,3 +257,22 @@ Proof.
repeat split;
assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
Qed.
+
+Unset Implicit Arguments.
+
+(** [n]th iteration of the function [f] *)
+
+Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
+ match n with
+ | O => x
+ | S n' => f (iter_nat n' A f x)
+ end.
+
+Theorem iter_nat_plus :
+ forall (n m:nat) (A:Type) (f:A -> A) (x:A),
+ iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
+Proof.
+ simple induction n;
+ [ simpl in |- *; auto with arith
+ | intros; simpl in |- *; apply f_equal with (f := f); apply H ].
+Qed.