From 943133d5a47ce4663a9b77a03b36c7c87c78d886 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 3 Dec 2013 16:43:14 +0100
Subject: Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.

---
 plugins/fourier/Fourier_util.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
index b10c304c8..3ab7ad84a 100644
--- a/plugins/fourier/Fourier_util.v
+++ b/plugins/fourier/Fourier_util.v
@@ -164,7 +164,7 @@ Qed.
 Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y.
 unfold not; intros.
 apply H.
-apply Rplus_lt_reg_r with x.
+apply Rplus_lt_reg_l with x.
 replace (x + 0) with x.
 replace (x + (y - x)) with y.
 try exact H0.
@@ -177,7 +177,7 @@ unfold not; intros.
 apply H.
 case H0; intros.
 left.
-apply Rplus_lt_reg_r with x.
+apply Rplus_lt_reg_l with x.
 replace (x + 0) with x.
 replace (x + (y - x)) with y.
 try exact H1.
-- 
cgit v1.2.3