Renamed Rabs_le theorems and added lt versions.

src/Core/Fcore_FTZ.v

@@ -251,7 +251,7 @@ now apply Zrnd_monotone.
 rewrite <- (Zrnd_Z2R rnd 0).
 apply Zrnd_monotone.
 apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le.
-destruct (Rabs_le_r_inv _ _ Hx) as [Hx1|Hx1].
+destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1].
 exact Hx1.
 elim Rle_not_lt with (1 := Hx1).
 apply Rle_lt_trans with (2 := Hy).
@@ -262,7 +262,7 @@ rewrite <- (Zrnd_Z2R rnd 0).
 apply Zrnd_monotone.
 apply Rle_trans with (Z2R 1).
 now apply Z2R_le.
-destruct (Rabs_le_r_inv _ _ Hy) as [Hy1|Hy1].
+destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1].
 elim Rle_not_lt with (1 := Hy1).
 apply Rlt_le_trans with (2 := Hxy).
 apply (Rabs_def2 _ _ Hx).

src/Core/Fcore_Raux.v

@@ -177,7 +177,7 @@ apply Rle_refl.
 apply Rsqrt_positivity.
 Qed.
 
-Theorem Rabs_le_l :
+Theorem Rabs_le :
   forall x y,
   (-y <= x <= y)%R -> (Rabs x <= y)%R.
 Proof.
@@ -189,7 +189,7 @@ now rewrite Ropp_involutive.
 exact Hxy.
 Qed.
 
-Theorem Rabs_le_l_inv :
+Theorem Rabs_le_inv :
   forall x y,
   (Rabs x <= y)%R -> (-y <= x <= y)%R.
 Proof.
@@ -204,7 +204,7 @@ apply Rle_trans with (2 := Hxy).
 apply RRle_abs.
 Qed.
 
-Theorem Rabs_le_r :
+Theorem Rabs_ge :
   forall x y,
   (y <= -x \/ x <= y)%R -> (x <= Rabs y)%R.
 Proof.
@@ -218,12 +218,12 @@ apply Rle_trans with (1 := Hxy).
 apply RRle_abs.
 Qed.
 
-Theorem Rabs_le_r_inv :
+Theorem Rabs_ge_inv :
   forall x y,
   (x <= Rabs y)%R -> (y <= -x \/ x <= y)%R.
 Proof.
-unfold Rabs.
 intros x y.
+unfold Rabs.
 case Rcase_abs ; intros Hy Hxy.
 left.
 apply Ropp_le_cancel.
@@ -231,6 +231,49 @@ now rewrite Ropp_involutive.
 now right.
 Qed.
 
+Theorem Rabs_lt :
+  forall x y,
+  (-y < x < y)%R -> (Rabs x < y)%R.
+Proof.
+intros x y (Hyx,Hxy).
+now apply Rabs_def1.
+Qed.
+
+Theorem Rabs_lt_inv :
+  forall x y,
+  (Rabs x < y)%R -> (-y < x < y)%R.
+Proof.
+intros x y H.
+now split ; eapply Rabs_def2.
+Qed.
+
+Theorem Rabs_gt :
+  forall x y,
+  (y < -x \/ x < y)%R -> (x < Rabs y)%R.
+Proof.
+intros x y [Hyx|Hxy].
+rewrite <- Rabs_Ropp.
+apply Rlt_le_trans with (Ropp y).
+apply Ropp_lt_cancel.
+now rewrite Ropp_involutive.
+apply RRle_abs.
+apply Rlt_le_trans with (1 := Hxy).
+apply RRle_abs.
+Qed.
+
+Theorem Rabs_gt_inv :
+  forall x y,
+  (x < Rabs y)%R -> (y < -x \/ x < y)%R.
+Proof.
+intros x y.
+unfold Rabs.
+case Rcase_abs ; intros Hy Hxy.
+left.
+apply Ropp_lt_cancel.
+now rewrite Ropp_involutive.
+now right.
+Qed.
+
 End Rmissing.
 
 Section Zmissing.