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