diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-11 13:24:12 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-11 13:24:12 +0000 |
| commit | 39bfa90d2bc53d4403962267da4c6ecbe26c3129 (patch) | |
| tree | 6142a7b573f4b53adcd66f50d80eaf58646ca451 /theories/Reals/Rfunctions.v | |
| parent | a37c28e3b76f921e377dccca639c6ffa5331eefc (diff) | |
Added the following lemmas to homogenize Reals a bit:
- Rmult_eq_compat_r, Rmult_eq_reg_r, Rplus_le_reg_r, Rmult_lt_reg_r,
Rmult_le_reg_r (mirrored variants of the existing _l lemmas);
- minus_IZR, opp_IZR (Ropp_Ropp_IZR), abs_IZR (mirrored Rabs_Zabs);
- Rle_abs (RRle_abs);
- Zpower_pos_powerRZ (signed variant of Zpower_nat_powerRZ).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12321 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rfunctions.v')
| -rw-r--r-- | theories/Reals/Rfunctions.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index da28184f2..68862f492 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -619,6 +619,18 @@ Proof. unfold Zpower_nat in |- *; auto. Qed. +Lemma Zpower_pos_powerRZ : + forall n m, IZR (Zpower_pos n m) = IZR n ^Z Zpos m. +Proof. + intros. + rewrite Zpower_pos_nat; simpl. + induction (nat_of_P m). + easy. + unfold Zpower_nat; simpl. + rewrite mult_IZR. + now rewrite <- IHn0. +Qed. + Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z. Proof. intros x z; case z; simpl in |- *; auto with real. |