From 943133d5a47ce4663a9b77a03b36c7c87c78d886 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 3 Dec 2013 16:43:14 +0100 Subject: Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l. --- theories/Reals/NewtonInt.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Reals/NewtonInt.v') diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 67e353eea..f67659b5b 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -393,7 +393,7 @@ Proof. case (Rle_dec (x + h) b); intro. cut (b < x + h). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H14)). - apply Rplus_lt_reg_r with (- h - b); replace (- h - b + b) with (- h); + apply Rplus_lt_reg_l with (- h - b); replace (- h - b + b) with (- h); [ idtac | ring ]; replace (- h - b + (x + h)) with (x - b); [ idtac | ring ]; apply Rle_lt_trans with (Rabs h). rewrite <- Rabs_Ropp; apply RRle_abs. -- cgit v1.2.3