adds a theorem to reason at the level of Z

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12119 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index c99582a25..34e76b8ac 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -49,6 +49,13 @@ Proof.
       | simpl in |- *; auto with arith ].
 Qed.
 
+Lemma iter_nat_of_Z : forall n A f x, 0 <= n ->
+  iter n A f x = iter_nat (Zabs_nat n) A f x.
+intros n A f x; case n; auto.
+intros p _; unfold iter, Zabs_nat; apply iter_nat_of_P.
+intros p abs; case abs; trivial.
+Qed.
+
 Theorem iter_pos_plus :
   forall (p q:positive) (A:Type) (f:A -> A) (x:A),
     iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x).