diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 17:21:01 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 17:21:01 +0200 |
| commit | 8271b23dd0a26bba79c7d6dadd92d2329945675c (patch) | |
| tree | 6d6b4faeda0fc272c1faaa7912406097ef055caa /theories/Reals/Rderiv.v | |
| parent | e5e3725fab9daa810a4c8a383886f1c5dc980e85 (diff) | |
| parent | 8c43e795c772090b336c0f170a6e5dcab196125d (diff) | |
Merge PR #7897: Remove fourier plugin
Diffstat (limited to 'theories/Reals/Rderiv.v')
| -rw-r--r-- | theories/Reals/Rderiv.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index dfa5c7104..aaf691ed1 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -16,7 +16,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rlimit. -Require Import Fourier. +Require Import Lra. Require Import Omega. Local Open Scope R_scope. @@ -77,7 +77,7 @@ Proof. elim (Rmin_Rgt (/ 2) x 0); intros a b; cut (0 < 2). intro; generalize (Rinv_0_lt_compat 2 H3); intro; fold (/ 2 > 0) in H4; apply (b (conj H4 H)). - fourier. + lra. intros; elim H3; clear H3; intros; generalize (let (H1, H2) := @@ -167,7 +167,7 @@ Proof. unfold Rabs; destruct (Rcase_abs 2) as [Hlt|Hge]; auto. cut (0 < 2). intro H7; elim (Rlt_asym 0 2 H7 Hlt). - fourier. + lra. apply Rabs_no_R0. discrR. Qed. |