diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 10:13:50 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 10:13:50 +0100 |
commit | e8c2d7a2f269eaa0c3b75d75680893f6af5dd29e (patch) | |
tree | a24c4143057fc72ec18e354792ebf0a9661edd5b /theories/Reals/RIneq.v | |
parent | 758df421b3e65ac349882e3d6c97448687eca098 (diff) | |
parent | dc71c8b582552dcc1ea40af8a2894f7f0ec84597 (diff) |
Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas
Diffstat (limited to 'theories/Reals/RIneq.v')
-rw-r--r-- | theories/Reals/RIneq.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 7bcd2799a..bc82c3712 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1611,6 +1611,9 @@ Proof. Qed. Hint Resolve mult_INR: real. +Lemma pow_INR (m n: nat) : INR (m ^ n) = pow (INR m) n. +Proof. now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed. + (*********) Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n. Proof. |