theories/Reals/Rpow_def.v


1
2
3
4
5
6
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.