summaryrefslogtreecommitdiff
path: root/theories/Reals/Rlimit.v
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /theories/Reals/Rlimit.v
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'theories/Reals/Rlimit.v')
-rw-r--r--theories/Reals/Rlimit.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index b14fcc4d..e3e995d2 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -15,7 +15,7 @@
Require Import Rbase.
Require Import Rfunctions.
-Require Import Fourier.
+Require Import Lra.
Local Open Scope R_scope.
(*******************************)
@@ -24,7 +24,7 @@ Local Open Scope R_scope.
(*********)
Lemma eps2_Rgt_R0 : forall eps:R, eps > 0 -> eps * / 2 > 0.
Proof.
- intros; fourier.
+ intros; lra.
Qed.
(*********)
@@ -45,14 +45,14 @@ Qed.
Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps.
Proof.
intros.
- fourier.
+ lra.
Qed.
(*********)
Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps.
Proof.
intros.
- fourier.
+ lra.
Qed.
(*********)