Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 56 insertions, 70 deletions

diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index c9cee31d..1912f5e1 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,89 +6,75 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zpower.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Zpower.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
 
+Require Import Wf_nat.
 Require Import ZArith_base.
 Require Export Zpow_def.
 Require Import Omega.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
 
-Section section1.
+Infix "^" := Zpower : Z_scope.
 
 (** * Definition of powers over [Z]*)
 
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *) 
 
-  Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
-
-  (** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
-      [plus : nat->nat] and [Zmult : Z->Z] *)
-
-  Lemma Zpower_nat_is_exp :
-    forall (n m:nat) (z:Z),
-      Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
-  Proof.
-    intros; elim n;
-      [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
-	| unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
-	  apply Zmult_assoc ].
-  Qed.
-
-  (** This theorem shows that powers of unary and binary integers
-     are the same thing, modulo the function convert : [positive -> nat] *)
-
-  Theorem Zpower_pos_nat :
-    forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
-  Proof.
-    intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
-      apply iter_nat_of_P.
-  Qed.
-
-  (** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
-     deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
-     for [add : positive->positive] and [Zmult : Z->Z] *)
-
-  Theorem Zpower_pos_is_exp :
-    forall (n m:positive) (z:Z),
-      Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
-  Proof.
-    intros.
-    rewrite (Zpower_pos_nat z n).
-    rewrite (Zpower_pos_nat z m).
-    rewrite (Zpower_pos_nat z (n + m)).
-    rewrite (nat_of_P_plus_morphism n m).
-    apply Zpower_nat_is_exp.
-  Qed.
-
-  Infix "^" := Zpower : Z_scope.
-
-  Hint Immediate Zpower_nat_is_exp: zarith.
-  Hint Immediate Zpower_pos_is_exp: zarith.
-  Hint Unfold Zpower_pos: zarith.
-  Hint Unfold Zpower_nat: zarith.
-
-  Lemma Zpower_exp :
-    forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
-  Proof.
-    destruct n; destruct m; auto with zarith.
-    simpl in |- *; intros; apply Zred_factor0.
-    simpl in |- *; auto with zarith.
-    intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
-    intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
-  Qed.
-
-End section1.
-
-(** Exporting notation "^" *)
-
-Infix "^" := Zpower : Z_scope.
-
-Hint Immediate Zpower_nat_is_exp: zarith.
-Hint Immediate Zpower_pos_is_exp: zarith.
-Hint Unfold Zpower_pos: zarith.
-Hint Unfold Zpower_nat: zarith.
+Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
+
+(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
+    [plus : nat->nat] and [Zmult : Z->Z] *)
+
+Lemma Zpower_nat_is_exp :
+  forall (n m:nat) (z:Z),
+    Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
+Proof.
+  intros; elim n;
+   [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
+     | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
+       apply Zmult_assoc ].
+Qed.
+
+(** This theorem shows that powers of unary and binary integers
+   are the same thing, modulo the function convert : [positive -> nat] *)
+
+Lemma Zpower_pos_nat :
+  forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
+Proof.
+  intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
+    apply iter_nat_of_P.
+Qed.
+
+(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
+   deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
+   for [add : positive->positive] and [Zmult : Z->Z] *)
+
+Lemma Zpower_pos_is_exp :
+  forall (n m:positive) (z:Z),
+    Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
+Proof.
+  intros.
+  rewrite (Zpower_pos_nat z n).
+  rewrite (Zpower_pos_nat z m).
+  rewrite (Zpower_pos_nat z (n + m)).
+  rewrite (nat_of_P_plus_morphism n m).
+  apply Zpower_nat_is_exp.
+Qed.
+
+Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
+Hint Unfold Zpower_pos Zpower_nat: zarith.
+
+Theorem Zpower_exp :
+  forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
+Proof.
+  destruct n; destruct m; auto with zarith.
+  simpl; intros; apply Zred_factor0.
+  simpl; auto with zarith.
+  intros; compute in H0; elim H0; auto.
+  intros; compute in H; elim H; auto.
+Qed.
 
 Section Powers_of_2.