From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Reals/Ranalysis5.v | 87 +++++++++++++++++++--------------------------
 1 file changed, 36 insertions(+), 51 deletions(-)

(limited to 'theories/Reals/Ranalysis5.v')

diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index d172139f..afb78e1c 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Import Rbase.
@@ -15,6 +17,7 @@ Require Import RiemannInt.
 Require Import SeqProp.
 Require Import Max.
 Require Import Omega.
+Require Import Lra.
 Local Open Scope R_scope.
 
 (** * Preliminaries lemmas *)
@@ -26,46 +29,34 @@ Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub,
        (forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
        (forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y).
 Proof.
-intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub.
- assert (x_encad : f lb <= x <= f ub).
-  split ; [assumption | apply Rle_trans with (r2:=y) ; [apply Rlt_le|] ; assumption].
- assert (y_encad : f lb <= y <= f ub).
-  split ; [apply Rle_trans with (r2:=x) ; [|apply Rlt_le] ; assumption | assumption].
-  assert (Temp1 : lb <= lb) by intuition ; assert (Temp2 : ub <= ub) by intuition.
- assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)).
- assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)).
- clear Temp1 Temp2.
- case (Rlt_dec (g x) (g y)).
-  intuition.
+  intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub.
+  assert (x_encad : f lb <= x <= f ub) by lra.
+  assert (y_encad : f lb <= y <= f ub) by lra.
+  assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)).
+  assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)).
+  case (Rlt_dec (g x) (g y)); [ easy |].
   intros Hfalse.
-   assert (Temp := Rnot_lt_le _ _ Hfalse).
-   assert (Hcontradiction : y <= x).
-   replace y with (id y) by intuition ; replace x with (id x) by intuition ;
-   rewrite <- f_eq_g. rewrite <- f_eq_g.
-   assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y).
+  assert (Temp := Rnot_lt_le _ _ Hfalse).
+  enough (y <= x) by lra.
+  replace y with (id y) by easy.
+  replace x with (id x) by easy.
+  rewrite <- f_eq_g by easy.
+  rewrite <- f_eq_g by easy.
+  assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). {
     intros m n lb_le_m m_le_n n_lt_ub.
     case (m_le_n).
-     intros ; apply Rlt_le ; apply f_incr ; [| | apply Rlt_le] ; assumption.
-     intros Hyp ; rewrite Hyp ; apply Req_le ; reflexivity.
-   apply f_incr2.
-   intuition. intuition.
-   Focus 3. intuition.
-   Focus 2. intuition.
-   Focus 2. intuition. Focus 2. intuition.
-   assert (Temp2 : g x <> ub).
-   intro Hf.
-    assert (Htemp : (comp f g) x = f ub).
-     unfold comp ; rewrite Hf ; reflexivity.
-     rewrite f_eq_g in Htemp ; unfold id in Htemp.
-    assert (Htemp2 : x < f ub).
-     apply Rlt_le_trans with (r2:=y) ; intuition.
-    clear -Htemp Htemp2. fourier.
-    intuition. intuition.
-   clear -Temp2 gx_encad.
-   case (proj2 gx_encad).
-    intuition.
-    intro Hfalse ; apply False_ind ; apply Temp2 ; assumption.
-   apply False_ind. clear - Hcontradiction x_lt_y. fourier.
+    - intros; apply Rlt_le, f_incr, Rlt_le; assumption.
+    - intros Hyp; rewrite Hyp; apply Req_le; reflexivity.
+  }
+  apply f_incr2; intuition.
+  enough (g x <> ub) by lra.
+  intro Hf.
+  assert (Htemp : (comp f g) x = f ub). {
+    unfold comp; rewrite Hf; reflexivity.
+  }
+  rewrite f_eq_g in Htemp by easy.
+  unfold id in Htemp.
+  fourier.
 Qed.
 
 Lemma derivable_pt_id_interv : forall (lb ub x:R),
@@ -245,12 +236,8 @@ Lemma IVT_interv_prelim0 : forall (x y:R) (P:R->bool) (N:nat),
        x <= Dichotomy_ub x y P N <= y /\ x <= Dichotomy_lb x y P N <= y.
 Proof.
 assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+y) / 2 <= ub).
- intros x y lb ub Hyp.
-  split.
-  replace lb with ((lb + lb) * /2) by field.
-  unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
-  replace ub with ((ub + ub) * /2) by field.
-  unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
+  intros x y lb ub Hyp.
+  lra.
 intros x y P N x_lt_y.
 induction N.
  simpl ; intuition.
@@ -1027,9 +1014,7 @@ Qed.
 Lemma ub_lt_2_pos : forall x ub lb, lb < x -> x < ub -> 0 < (ub-lb)/2.
 Proof.
 intros x ub lb lb_lt_x x_lt_ub.
- assert (T : 0 < ub - lb).
-  fourier.
- unfold Rdiv ; apply Rlt_mult_inv_pos ; intuition.
+lra.
 Qed.
 
 Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal.
@@ -1102,7 +1087,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg.
     replace (- (fn N (x + h) - fn N x)) with (fn N x - fn N (x + h)) by field.
     assumption.
-   solve[apply Rlt_not_eq ; intuition].
+  now apply Rlt_not_eq, IZR_lt.
   rewrite <- Hc'; clear Hc Hc'.
   replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c).
   replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field.
-- 
cgit v1.2.3