diff options
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 9856b5452c..1fcf6f61e4 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. |