1 files changed, 12 insertions, 4 deletions
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 535f88c86..ec91dc5db 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -351,14 +351,22 @@ Definition testbit a n :=
 
 Definition to_nat (a:N) :=
   match a with
-  | 0 => O
-  | Npos p => Pos.to_nat p
+    | 0 => O
+    | Npos p => Pos.to_nat p
   end.
 
 Definition of_nat (n:nat) :=
   match n with
-  | O => 0
-  | S n' => Npos (Pos.of_succ_nat n')
+    | O => 0
+    | S n' => Npos (Pos.of_succ_nat n')
+  end.
+
+(** Iteration of a function *)
+
+Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
+  match n with
+    | 0 => x
+    | Npos p => Pos.iter p f x
   end.
 
 End N.
 \ No newline at end of file