diff options
| author | Vincent Laporte | 2019-04-01 19:40:53 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-01 19:40:53 +0000 |
| commit | 424c1973e96dfbf3b2e3245d735853ffa9600373 (patch) | |
| tree | af087fa873c709e0066c8f6d81898f3aeae59b21 /theories/Reals/Rbasic_fun.v | |
| parent | 943fdd3277909f5229d95eb2e486944b0258648c (diff) | |
| parent | 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 (diff) | |
Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and #9615)
Reviewed-by: Zimmi48
Ack-by: fajb
Reviewed-by: vbgl
Diffstat (limited to 'theories/Reals/Rbasic_fun.v')
| -rw-r--r-- | theories/Reals/Rbasic_fun.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 59e0148625..e17f02bb6e 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -15,7 +15,6 @@ Require Import Rbase. Require Import R_Ifp. -Require Import Lra. Local Open Scope R_scope. Implicit Type r : R. @@ -357,7 +356,9 @@ Qed. Lemma Rle_abs : forall x:R, x <= Rabs x. Proof. - intro; unfold Rabs; case (Rcase_abs x); intros; lra. + intro; unfold Rabs; case (Rcase_abs x); intros;auto with real. + apply Rminus_le; rewrite <- Rplus_0_r; + unfold Rminus; rewrite Ropp_involutive; auto with real. Qed. Definition RRle_abs := Rle_abs. |