diff options
Diffstat (limited to 'theories/Arith/Wf_nat.v')
-rw-r--r-- | theories/Arith/Wf_nat.v | 19 |
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. |