From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 theories/Reals/Rpow_def.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 theories/Reals/Rpow_def.v

(limited to 'theories/Reals/Rpow_def.v')

diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
new file mode 100644
index 00000000..5bdbb76b
--- /dev/null
+++ b/theories/Reals/Rpow_def.v
@@ -0,0 +1,7 @@
+Require Import Rdefinitions.
+
+Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+  match n with
+    | O => R1
+    | S n => Rmult r (pow r n)
+  end.
-- 
cgit v1.2.3