From 2e56d0c901ebaa034f9974a50b892378b755de24 Mon Sep 17 00:00:00 2001
From: bertot
Date: Thu, 7 May 2009 12:26:55 +0000
Subject: 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
---
 theories/ZArith/Zmisc.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index c99582a25f..34e76b8ac1 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).
-- 
cgit v1.2.3