diff options
Diffstat (limited to 'theories/Reals/Rfunctions.v')
| -rw-r--r-- | theories/Reals/Rfunctions.v | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index c727623c..3d1c0375 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rfunctions.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: Rfunctions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) (*i Some properties about pow and sum have been made with John Harrison i*) (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*) @@ -15,10 +15,10 @@ (** Definition of the sum functions *) (* *) (********************************************************) -Require Export LegacyArithRing. (* for ring_nat... *) Require Export ArithRing. Require Import Rbase. +Require Export Rpow_def. Require Export R_Ifp. Require Export Rbasic_fun. Require Export R_sqr. @@ -65,11 +65,6 @@ Qed. (** * Power *) (*******************************) (*********) -Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R := - match n with - | O => 1 - | S n => r * pow r n - end. Infix "^" := pow : R_scope. @@ -382,7 +377,7 @@ Proof. replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)). rewrite Hrecn; reflexivity. simpl in |- *; ring. - ring_nat. + ring. Qed. Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n. @@ -429,7 +424,7 @@ Proof. rewrite Hrecn2. simpl in |- *. ring. - ring_nat. + ring. Qed. Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n. |