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/Rbasic_fun.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/Rbasic_fun.v')
| -rw-r--r-- | theories/Reals/Rbasic_fun.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 9856b5452..1fcf6f61e 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -220,11 +220,13 @@ Proof. apply Rge_le; assumption. Qed. -Lemma RRle_abs : forall x:R, x <= Rabs x. +Lemma Rle_abs : forall x:R, x <= Rabs x. Proof. intro; unfold Rabs in |- *; case (Rcase_abs x); intros; fourier. Qed. +Definition RRle_abs := Rle_abs. + (*********) Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x. Proof. @@ -507,3 +509,8 @@ Proof. apply Rabs_right; auto with real zarith. Qed. +Lemma abs_IZR : forall z, IZR (Zabs z) = Rabs (IZR z). +Proof. + intros. + now rewrite Rabs_Zabs. +Qed. |