diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zmisc.v | 15 | ||||
| -rw-r--r-- | theories/ZArith/Zpower.v | 1 |
2 files changed, 2 insertions, 14 deletions
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index b05acd730..c99582a25 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -8,6 +8,7 @@ (*i $Id$ i*) +Require Import Wf_nat. Require Import BinInt. Require Import Zcompare. Require Import Zorder. @@ -18,11 +19,6 @@ Open Local Scope Z_scope. (** Iterators *) (** [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. Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A := match n with @@ -38,15 +34,6 @@ Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) := | Zneg p => 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. - Theorem iter_nat_of_P : forall (p:positive) (A:Type) (f:A -> A) (x:A), iter_pos p A f x = iter_nat (nat_of_P p) A f x. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index f3f357de1..7ee8b9766 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -8,6 +8,7 @@ (*i $Id$ i*) +Require Import Wf_nat. Require Import ZArith_base. Require Export Zpow_def. Require Import Omega. |