(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Conclusions                                                       *)
(* Chapter: Tame (Linear Programs)                                            *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2013-06-19                                                           *)
(* ========================================================================== *)

(*
Treatment of two special inequalities for the linear programs.

The main results are

LEMMA_8673686234 (uses inequalities "6170936724","8673686234 a","8673686234 b","8673686234 c")
see head.mod:yapex_sup_flat 'ID[8673686234]'

LEMMA_5691615370 (uses inequalities "5584033259","6170936724","5691615370")
see head.mod:perimZ 'ID[5691615370]'

*)

module Lp_details = struct

  open Hales_tactic;;
(* start 867 *)

let quadratic_root_plus_disc = 
prove_by_refinement(
  `!a b c x. &0 < a /\ a * x pow 2 + b * x + c <= &0 ==>
   &0 <= b pow 2 - &4 * a * c`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  TYPIFY `a * x pow 2 + b * x + c = a * (x + b /(&2 * a)) pow 2 - (b pow 2 - &4 * a*c)/(&4 * a)` (C SUBGOAL_THEN SUBST1_TAC);
    Calc_derivative.CALC_ID_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  ONCE_REWRITE_TAC[arith `u - v <= &0 <=> u <= v`];
  GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  CONJ_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  TYPIFY `&0 <= (a * (x + b / (&2 * a)) pow 2) * &4 * a` ENOUGH_TO_SHOW_TAC;
    BY(REAL_ARITH_TAC);
  GMATCH_SIMP_TAC REAL_LE_MUL;
  CONJ_TAC;
    GMATCH_SIMP_TAC REAL_LE_MUL;
    ASM_REWRITE_TAC[REAL_LE_POW_2];
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let quadratic_root_exists = 
prove_by_refinement(
  `!a b c x. &0 < a /\  a * x pow 2 + b * x + c <= &0 ==> 
    (?y. x <= y /\ a * y pow 2 + b *y + c = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `(h:real) = quadratic_root_plus (a, b + &2 * a *x, a * x pow 2 + b * x + c)`;
  TYPIFY `x + h` EXISTS_TAC;
  REWRITE_TAC[arith `a * (x + h) pow 2 + b * (x + h) +c = a * h pow 2 + (b + &2 * a *x) * h + (a * x pow 2 + b * x + c)`];
  TYPIFY `(b + &2 * a * x) pow 2 <= (b + &2 * a * x) pow 2 - &4 * a * (a * x pow 2 + b * x + c)` (C SUBGOAL_THEN ASSUME_TAC);
    ONCE_REWRITE_TAC[arith `v <= v - &4 * a * x <=> &0 <= a * (-- x)`];
    GMATCH_SIMP_TAC REAL_LE_MUL;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  CONJ2_TAC;
    EXPAND_TAC "h";
    MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Tame_lemmas.quadratic_root_plus_works);
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM MP_TAC;
    BY(MESON_TAC[REAL_LE_TRANS;REAL_LE_POW_2]);
  MATCH_MP_TAC (arith `&0 <= h ==> x <= x + h`);
  EXPAND_TAC "h";
  REWRITE_TAC[Sphere.quadratic_root_plus];
  GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  CONJ_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  ENOUGH_TO_SHOW_TAC `(b + &2 * a * x) <= sqrt((b + &2 * a*x) pow 2) /\ sqrt((b+ &2 * a*x) pow 2) <= sqrt((b + &2 * a * x) pow 2 - &4 * a * (a * x pow 2 + b * x + c))`;
    BY(REAL_ARITH_TAC);
  GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
  REWRITE_TAC[POW_2_SQRT_ABS];
  ASM_REWRITE_TAC[];
  CONJ2_TAC;
    BY(REAL_ARITH_TAC);
  SUBCONJ_TAC;
    BY(REWRITE_TAC[REAL_LE_POW_2]);
  BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let quadratic_root_pos_exists = 
prove_by_refinement(
  `!a b c x.  a < &0 /\  &0 <= a * x pow 2 + b * x + c ==> 
    (?y. x <= y /\ a * y pow 2 + b *y + c = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC quadratic_root_exists [`--a`;`--b`;`--c`;`x`];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `y` EXISTS_TAC;
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let delta_x_root_exists = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6.
    &0 <= delta_x x1 x2 x3 x4 x5 x6 /\ &0 < x1 ==>
     (?x4'. x4 <= x4' /\ delta_x x1 x2 x3 x4' x5 x6 = &0)`,

  (* {{{ proof *)
  [
 REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC  `b = ( delta_x4 x1 x2 x3 (&0) x5 x6)` ;
  TYPED_ABBREV_TAC  `c =  delta_x x1 x2 x3 (&0) x5 x6` ;
  TYPIFY `!z. delta_x x1 x2 x3 z x5 x6 = (-- x1) * z pow 2 + b * z + c` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "c";
    EXPAND_TAC "b";
    REWRITE_TAC[Sphere.delta_x;Sphere.delta_x4];
    BY(REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC quadratic_root_pos_exists;
  FIRST_X_ASSUM ((unlist REWRITE_TAC) o GSYM);
  ASM_REWRITE_TAC[];
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let delta_y_root_exists = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6.
    &0 <= delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y1 /\ &0 < y4 ==>
    (?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.delta_y];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC delta_x_root_exists [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `sqrt(x4')` EXISTS_TAC;
  TYPIFY `&0 <= x4'` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `<=` MP_TAC;
    BY(MESON_TAC[REAL_LE_POW_2;REAL_LE_TRANS;arith `x*x = x pow 2`]);
  TYPIFY `sqrt(x4') * sqrt(x4') = x4'` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC (GSYM SQRT_MUL);
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM_ST `y4 * y4 <= x4'` MP_TAC;
  FIRST_ASSUM_ST `(=)` (SUBST1_TAC o GSYM);
  REWRITE_TAC[arith `~(x <= y) <=> y < x`];
  MATCH_MP_TAC Misc_defs_and_lemmas.ABS_SQUARE;
  TYPIFY `&0 <= sqrt x4'` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC SQRT_POS_LE;
    BY(ASM_REWRITE_TAC[]);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let edge2_flatD_x1_quadratic_root_plus = 
prove_by_refinement(
  `!d x2 x3 x4 x5 x6.
    edge2_flatD_x1 d x2 x3 x4 x5 x6 = 
    quadratic_root_plus(x4,
			-- delta_x1 (&0) x2 x3 x4 x5 x6,
   d - delta_x (&0) x2 x3 x4 x5 x6 )`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.edge2_flatD_x1];
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
  TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`;
  TYPIFY `!z. d - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC));
    EXPAND_TAC "c";
    EXPAND_TAC "b";
    REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
    BY(REAL_ARITH_TAC);
  ASM_REWRITE_TAC[Nonlinear_lemma.abc_quadratic];
  ]);;
  (* }}} *)

let edge2_flatD_x1_expanded = 
prove_by_refinement(
  `!d x2 x3 x4 x5 x6. 
    edge2_flatD_x1 d x2 x3 x4 x5 x6 = (delta_x1 (&0) x2 x3 x4 x5 x6 
    + sqrt (ups_x x2 x3 x4 * ups_x x4 x5 x6 - &4 * x4 * d)) / (&2 * x4)
    `,

  (* {{{ proof *)
  [
  REWRITE_TAC[edge2_flatD_x1_quadratic_root_plus];
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
  TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`;
  REWRITE_TAC[Sphere.quadratic_root_plus];
  TYPIFY `b pow 2 - &4 * x4 * c = ups_x x2 x3 x4 * ups_x x4 x5 x6 - &4 * x4 * d` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "b";
    EXPAND_TAC "c";
    REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
    BY(REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  EXPAND_TAC "b";
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let derived_form_edge2_flatD_x1 = 
prove_by_refinement(
  `!x2 x3 x4 x5 x6. (&0 < ups_x x2 x3 x4 /\ &0 < ups_x x4 x5 x6 /\ &0 < x4)
     ==> (?f'.
    derived_form T
    (\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6) f' x2 (:real))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[edge2_flatD_x1_expanded];
  REWRITE_TAC[Nonlin_def.delta_x1;Sphere.ups_x;arith `x - &4 * x4 * &0 = x`];
  TYPIFY `((((x5 - x6 + x4) +    (((--x2 + -- &1 * x2) + &2 * x4 + &2 * x3) *     (--x4 * x4 - x5 * x5 - x6 * x6 +      &2 * x4 * x6 +      &2 * x4 * x5 +      &2 * x5 * x6)) *    inv    (&2 *     sqrt     ((--x2 * x2 - x3 * x3 - x4 * x4 +       &2 * x2 * x4 +       &2 * x2 * x3 +       &2 * x3 * x4) *      (--x4 * x4 - x5 * x5 - x6 * x6 +       &2 * x4 * x6 +       &2 * x4 * x5 +       &2 * x5 * x6)))) *   &2 *   x4) /  (&2 * x4) pow 2)` EXISTS_TAC;
  Pent_hex.DERIVED_TAC MP_TAC;
  REWRITE_TAC[GSYM Sphere.ups_x];
  TYPIFY_GOAL_THEN `(&0 < ups_x x2 x3 x4 * ups_x x4 x5 x6 /\ ~(&2 = &0) /\ ~(x4 = &0))` (unlist REWRITE_TAC);
  REWRITE_TAC[REAL_OF_NUM_EQ];
  GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
    BY(ARITH_TAC);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let edge2_flatD_x1_continuous = 
prove_by_refinement(
  `!x2 x3 x4 x5 x6. (&0 < ups_x x2 x3 x4 /\ &0 < ups_x x4 x5 x6 /\ &0 < x4 ==>
   (\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6) real_continuous atreal x2)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
  INTRO_TAC derived_form_edge2_flatD_x1 [`x2`;`x3`;`x4`;`x5`;`x6`];
  BY(ASM_REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV])
  ]);;
  (* }}} *)

let IVT_edge2_flatD_x1 = 
prove_by_refinement(
  `!x1m x1M x2m x2M x3 x4 x5 x6. 
    (!x2. x2m <= x2 /\ x2 <= x2M ==> &0 < ups_x x2 x3 x4) /\
    (&0 < ups_x x4 x5 x6) /\
    (&0 < x4) /\ 
    (x1m <= x1M) /\
    (x2m <= x2M) /\
    (delta_x x1M x2M x3 x4 x5 x6 = &0) /\
    (!x1 x2. x1m <= x1 /\ x1 <= x1M /\ x2m <= x2 /\ x2 <= x2M ==> 
       delta_x1 x1 x2 x3 x4 x5 x6 < &0) ==>
    ((?x2. x2m <= x2 /\ x2 <= x2M /\ edge2_flatD_x1 (&0) x2 x3 x4 x5 x6 = x1m) \/
       (x1m < edge2_flatD_x1 (&0) x2m x3 x4 x5 x6))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!x2. x2m <= x2 /\ x2 <= x2M ==> x1m < edge2_flatD_x1 (&0) x2 x3 x4 x5 x6` ASM_CASES_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`x2m`]);
    ASM_REWRITE_TAC[arith `x <= x`];
    BY(MESON_TAC[]);
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[NOT_FORALL_THM];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[TAUT `~(a ==> b) <=> (a /\ ~b)`];
  REWRITE_TAC[arith `~(x < b) <=> b <= x`];
  REPEAT WEAKER_STRIP_TAC;
  DISJ1_TAC;
  INTRO_TAC REAL_IVT_INCREASING [`(\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6)`;`x2`;`x2M`;`x1m`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    CONJ2_TAC;
      ENOUGH_TO_SHOW_TAC `edge2_flatD_x1 (&0) x2M x3 x4 x5 x6 = x1M`;
        BY(ASM_TAC THEN REAL_ARITH_TAC);
      MATCH_MP_TAC Pent_hex.edge2_flatD_x1_delta_lemma2;
      ASM_REWRITE_TAC[];
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN];
    REWRITE_TAC[IN_REAL_INTERVAL];
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL;
    MATCH_MP_TAC edge2_flatD_x1_continuous;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    ASM_REWRITE_TAC[];
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[IN_REAL_INTERVAL];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `x` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let edge2_flatD_x1_works = 
prove_by_refinement(
  `!x2 x3 x4 x5 x6.
  &0 <= ups_x x2 x3 x4 /\ &0 <= ups_x x4 x5 x6 /\ ~(x4 = &0) ==>
    delta_x (edge2_flatD_x1 (&0) x2 x3 x4 x5 x6) x2 x3 x4 x5 x6 = &0`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[edge2_flatD_x1_quadratic_root_plus];
  TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
  TYPED_ABBREV_TAC `c = (&0 - delta_x (&0) x2 x3 x4 x5 x6)`;
  ONCE_REWRITE_TAC[arith `d = &0 <=> &0 - d = &0`];
  TYPIFY `!z. &0 - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC));
    EXPAND_TAC "c";
    EXPAND_TAC "b";
    REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
    BY(REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Tame_lemmas.quadratic_root_plus_works);
  TYPIFY `b pow 2 - &4 * x4 * c = ups_x x2 x3 x4 * ups_x x4 x5 x6 ` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "b";
    EXPAND_TAC "c";
    REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
    BY(REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC REAL_LE_MUL;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let delta_x1_decreasing = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6 x1'.
    x1 <= x1' /\ &0 <= x4 ==>
    delta_x1 x1' x2 x3 x4 x5 x6 <= delta_x1 x1 x2 x3 x4 x5 x6`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  ENOUGH_TO_SHOW_TAC `delta_x1 x1 x2 x3 x4 x5 x6 - delta_x1 x1' x2 x3 x4 x5 x6 = &2 * x4 * (x1' - x1)`;
    ONCE_REWRITE_TAC[arith `d' <= d <=> &0 <= d - d'`];
    DISCH_THEN SUBST1_TAC;
    GMATCH_SIMP_TAC REAL_LE_MUL;
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    GMATCH_SIMP_TAC REAL_LE_MUL;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[Nonlin_def.delta_x1];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let IVT_delta_x = 
prove_by_refinement(
  `!x1m x1M x2m x2M x3 x4 x5 x6.
         (!x2. x2m <= x2 /\ x2 <= x2M ==> &0 < ups_x x2 x3 x4) /\
         &0 < ups_x x4 x5 x6 /\
         &0 < x4 /\
         x1m <= x1M /\
         x2m <= x2M /\
         delta_x x1M x2M x3 x4 x5 x6 = &0 /\
         (!x2. x2m <= x2 /\ x2 <= x2M
              ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0)
         ==> (?x2. x2m <= x2 /\
                   x2 <= x2M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/
             (?x1. x1m < x1 /\ delta_x x1 x2m x3 x4 x5 x6 = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC IVT_edge2_flatD_x1 [`x1m`;`x1M`;`x2m`;`x2M`;`x3`;`x4`;`x5`;`x6`];
  ANTS_TAC;
    (ASM_REWRITE_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    ENOUGH_TO_SHOW_TAC `delta_x1 x1 x2 x3 x4 x5 x6 <= delta_x1 x1m x2 x3 x4 x5 x6`;
      MATCH_MP_TAC (arith `x < &0 ==> (y <= x ==> y< &0)`);
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[]);
    MATCH_MP_TAC delta_x1_decreasing;
    BY(ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`]);
  STRIP_TAC;
    DISJ1_TAC;
    TYPIFY `x2` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    EXPAND_TAC "x1m";
    MATCH_MP_TAC edge2_flatD_x1_works;
    BY(ASM_SIMP_TAC[arith `x < y ==> x <= y`;arith `&0 < x ==> ~(x = &0)`]);
  DISJ2_TAC;
  TYPIFY `edge2_flatD_x1 (&0) x2m x3 x4 x5 x6` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC edge2_flatD_x1_works;
  ASM_SIMP_TAC[arith `x < y ==> x <= y`;arith `&0 < x ==> ~(x = &0)`];
  MATCH_MP_TAC (arith `x < y ==> x <= y`);
  FIRST_X_ASSUM MATCH_MP_TAC;
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let delta_x1_sym = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6.
     delta_x1 x1 x3 x2 x4 x6 x5 = delta_x1 x1 x2 x3 x4 x5 x6 /\
    delta_x1 x1 x5 x6 x4 x2 x3 = delta_x1 x1 x2 x3 x4 x5 x6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.delta_x1];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let IVT_delta_x_3 = 
prove_by_refinement(
  `!x1m x1M x2 x3m x3M x4 x5 x6.
         (!x3. x3m <= x3 /\ x3 <= x3M ==> &0 < ups_x x2 x3 x4) /\
         &0 < ups_x x4 x5 x6 /\
         &0 < x4 /\
         x1m <= x1M /\
         x3m <= x3M /\
         delta_x x1M x2 x3M x4 x5 x6 = &0 /\
         (!x3. x3m <= x3 /\ x3 <= x3M
              ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0)
         ==> (?x3. x3m <= x3 /\
                   x3 <= x3M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/
             (?x1. x1m < x1 /\ delta_x x1 x2 x3m x4 x5 x6 = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x3m`;`x3M`;`x2`;`x4`;`x6`;`x5`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      ONCE_REWRITE_TAC[Merge_ineq.ups_x_sym];
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[]);
    CONJ_TAC;
      FIRST_X_ASSUM_ST `ups_x` MP_TAC;
      BY(MESON_TAC[Collect_geom.UPS_X_SYM]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]);
    BY(ASM_MESON_TAC[delta_x1_sym]);
  BY(MESON_TAC[Merge_ineq.delta_x_sym])
  ]);;
  (* }}} *)

let IVT_delta_x_5 = 
prove_by_refinement(
  `!x1m x1M x2 x3 x4 x5m x5M x6.
         (!x5. x5m <= x5 /\ x5 <= x5M ==> &0 < ups_x x4 x5 x6) /\
         &0 < ups_x x2 x3 x4 /\
         &0 < x4 /\
         x1m <= x1M /\
         x5m <= x5M /\
         delta_x x1M x2 x3 x4 x5M x6 = &0 /\
         (!x5. x5m <= x5 /\ x5 <= x5M
              ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0)
         ==> (?x5. x5m <= x5 /\
                   x5 <= x5M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/
             (?x1. x1m < x1 /\ delta_x x1 x2 x3 x4 x5m x6 = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x5m`;`x5M`;`x6`;`x4`;`x2`;`x3`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]);
    BY(ASM_MESON_TAC[delta_x1_sym]);
  BY(MESON_TAC[Merge_ineq.delta_x_sym])
  ]);;
  (* }}} *)

let IVT_delta_x_6 = 
prove_by_refinement(
  `!x1m x1M x2 x3 x4 x5 x6m x6M.
         (!x6. x6m <= x6 /\ x6 <= x6M ==> &0 < ups_x x4 x5 x6) /\
         &0 < ups_x x2 x3 x4 /\
         &0 < x4 /\
         x1m <= x1M /\
         x6m <= x6M /\
         delta_x x1M x2 x3 x4 x5 x6M = &0 /\
         (!x6. x6m <= x6 /\ x6 <= x6M
              ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0)
         ==> (?x6. x6m <= x6 /\
                   x6 <= x6M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/
             (?x1. x1m < x1 /\ delta_x x1 x2 x3 x4 x5 x6m = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x6m`;`x6M`;`x5`;`x4`;`x3`;`x2`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]);
    BY(ASM_MESON_TAC[delta_x1_sym]);
  BY(MESON_TAC[Merge_ineq.delta_x_sym])
  ]);;
  (* }}} *)

let IVT_delta_x_full = 
prove_by_refinement(
  `!x1m x1M x2m x2M x3m x3M x4 x5m x5M x6m x6M.
    &0 < x4 /\
    (!x2 x3. x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M ==> &0 < ups_x x2 x3 x4) /\
    (!x5 x6. x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M ==> &0 < ups_x x4 x5 x6) /\
    x1m <= x1M /\ x2m <= x2M /\ x3m <= x3M /\ x5m <= x5M /\ x6m <= x6M /\
    delta_x x1M x2M x3M x4 x5M x6M = &0 /\
    (! x2 x3 x5 x6.
       x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M /\
       x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M ==>
       delta_x1 x1m x2 x3 x4 x5 x6 < &0) ==>
    (?x2 x3 x5 x6. x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M /\
       x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M /\
       delta_x x1m x2 x3 x4 x5 x6 = &0) \/
    (?x1. x1m < x1 /\ delta_x x1 x2m x3m x4 x5m x6m = &0)
`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  PROOF_BY_CONTR_TAC;
  RULE_ASSUM_TAC (REWRITE_RULE[DE_MORGAN_THM;NOT_EXISTS_THM;TAUT `~(a /\ b) <=> a ==> ~b`;TAUT `a ==> b ==> c <=> (a /\ b) ==> c`]);
  FIRST_X_ASSUM MP_TAC;
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x2m`;`x2M`;`x3M`;`x4`;`x5M`;`x6M`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[arith `x <= x`]);
    CONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[arith `x <= x`]);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[arith `x <= x`]);
  STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[arith `x <= x`]);
  INTRO_TAC IVT_delta_x_3 [`x1m`;`x1`;`x2m`;`x3m`;`x3M`;`x4`;`x5M`;`x6M`];
  ASM_REWRITE_TAC[];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[arith `x <= x`]);
    CONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[arith `x <= x`]);
    CONJ_TAC;
      BY(FIRST_X_ASSUM_ST `<` MP_TAC THEN REAL_ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[arith `x <= x`]);
  STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[arith `x <= x`]);
  INTRO_TAC IVT_delta_x_5 [`x1m`;`x1'`;`x2m`;`x3m`;`x4`;`x5m`;`x5M`;`x6M`];
  ASM_REWRITE_TAC[];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[arith `x <= x`]);
    CONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[arith `x <= x`]);
    CONJ_TAC;
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[arith `x <= x`]);
  STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[arith `x <= x`]);
  INTRO_TAC IVT_delta_x_6 [`x1m`;`x1''`;`x2m`;`x3m`;`x4`;`x5m`;`x6m`;`x6M`];
  ASM_REWRITE_TAC[];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[arith `x <= x`]);
    CONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[arith `x <= x`]);
    CONJ_TAC;
      BY(REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[arith `x <= x`]);
  STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[arith `x <= x`]);
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[];
  FIRST_X_ASSUM MATCH_MP_TAC;
  BY(REPLICATE_TAC 4 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let FORALL_BIJ_SQUARE = 
prove_by_refinement(
  `!P ym yM. &0 <= ym /\ &0 <= yM ==> 
    ((!x. ym*ym <= x /\ x <= yM*yM ==> P x) <=> 
    (!y. ym <= y /\ y <= yM ==> P (y*y)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC (TAUT `(a ==> b) /\ (b ==> a) ==> (a <=> b)`);
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
    GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `&0 <= x` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `y*y <= x` MP_TAC;
    BY(MESON_TAC[REAL_LE_POW_2;arith `x*x = x pow 2`;REAL_LE_TRANS]);
  REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `*` MP_TAC);
  TYPIFY_GOAL_THEN `x = sqrt x * sqrt x` (unlist ONCE_REWRITE_TAC);
    GMATCH_SIMP_TAC (GSYM SQRT_MUL);
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[arith `x * x = x pow 2`];
  GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND);
  GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND);
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC SQRT_POS_LE;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `x pow 2 = x*x`];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MATCH_MP_TAC;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let EXISTS_BIJ_SQUARE = 
prove_by_refinement(
  `!P ym yM. &0 <= ym /\ &0 <= yM ==> 
    ((?x. ym*ym <= x /\ x <= yM*yM /\ P x) <=> 
    (?y. ym <= y /\ y <= yM /\ P (y*y)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`];
  REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM];
  REWRITE_TAC[TAUT `~a \/ ~b \/ ~c <=> (a /\ b ==> ~c)`];
  MATCH_MP_TAC FORALL_BIJ_SQUARE;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let IVT_delta_y_full = 
prove_by_refinement(
  `!y1m y1M y2m y2M y3m y3M y4 y5m y5M y6m y6M.
    &0 < y4 /\
    &0 <= y1m /\ &0 <= y2m /\ &0 <= y3m /\ &0 <= y5m /\ &0 <= y6m /\
    (!y2 y3. y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M ==> &0 < ups_x (y2*y2) (y3*y3) (y4*y4)) /\
    (!y5 y6. y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M ==> &0 < ups_x (y4*y4) (y5*y5) (y6*y6)) /\
    y1m <= y1M /\ y2m <= y2M /\ y3m <= y3M /\ y5m <= y5M /\ y6m <= y6M /\
    delta_y y1M y2M y3M y4 y5M y6M = &0 /\
    (! y2 y3 y5 y6.
       y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M /\
       y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M ==>
       y_of_x delta_x1 y1m y2 y3 y4 y5 y6 < &0) ==>
    (?y2 y3 y5 y6. y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M /\
       y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M /\
       delta_y y1m y2 y3 y4 y5 y6 = &0) \/
    (?y1. y1m < y1 /\ delta_y y1 y2m y3m y4 y5m y6m = &0)
`,

  (* {{{ proof *)
  [

  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `&0 <= y2M /\ &0 <= y3M /\ &0 <= y5M /\ &0 <= y6M` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT (FIRST_X_ASSUM_ST `!` kill);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  INTRO_TAC IVT_delta_x_full [`y1m * y1m`;`y1M * y1M`;`y2m*y2m`;`y2M*y2M`;`y3m*y3m`;`y3M*y3M`;`y4*y4`;`y5m*y5m`;`y5M*y5M`;`y6m*y6m`;`y6M*y6M`];
  ANTS_TAC;
    ASM_REWRITE_TAC[GSYM Sphere.delta_y];
    CONJ_TAC;
      GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
      BY(ASM_REWRITE_TAC[]);
    CONJ_TAC;
      TYPIFY `!x2. y2m * y2m <= x2 /\ x2 <= y2M * y2M ==> !x3. y3m * y3m <= x3 /\ x3 <= y3M * y3M  ==> &0 < ups_x x2 x3 (y4 * y4)` ENOUGH_TO_SHOW_TAC;
        BY(MESON_TAC[]);
      REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC);
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    CONJ_TAC;
      TYPIFY `!x5.     y5m * y5m <= x5 /\ x5 <= y5M * y5M ==> !x6. y6m * y6m <= x6 /\ x6 <= y6M * y6M     ==> &0 < ups_x (y4 * y4) x5 x6` ENOUGH_TO_SHOW_TAC;
        BY(MESON_TAC[]);
      REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC);
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REPEAT (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE);
    ASM_SIMP_TAC[arith `&0 <= y ==> abs y = y`];
    TYPIFY `!x2 .     y2m * y2m <= x2 /\     x2 <= y2M * y2M ==> !x3.     y3m * y3m <= x3 /\     x3 <= y3M * y3M ==> !x5.     y5m * y5m <= x5 /\     x5 <= y5M * y5M ==> !x6.     y6m * y6m <= x6 /\     x6 <= y6M * y6M     ==> delta_x1 (y1m * y1m) x2 x3 (y4 * y4) x5 x6 < &0` ENOUGH_TO_SHOW_TAC;
      BY(MESON_TAC[]);
    REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC);
    REWRITE_TAC[GSYM Sphere.y_of_x];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  STRIP_TAC;
    DISJ1_TAC;
    TYPIFY `?y2.     y2m <= y2 /\     y2 <= y2M /\ ?y3.     y3m <= y3 /\     y3 <= y3M /\ ?y5.     y5m <= y5 /\     y5 <= y5M /\ ?y6.     y6m <= y6 /\     y6 <= y6M /\     delta_y y1m y2 y3 y4 y5 y6 = &0` ENOUGH_TO_SHOW_TAC;
      BY(MESON_TAC[]);
    REWRITE_TAC[Sphere.delta_y];
    GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
    ASM_REWRITE_TAC[];
    TYPIFY `x2` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
    ASM_REWRITE_TAC[];
    TYPIFY `x3` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
    ASM_REWRITE_TAC[];
    TYPIFY `x5` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
    ASM_REWRITE_TAC[];
    TYPIFY `x6` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISJ2_TAC;
  REWRITE_TAC[Sphere.delta_y];
  TYPIFY `sqrt x1` EXISTS_TAC;
  GMATCH_SIMP_TAC (GSYM SQRT_MUL);
  GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC REAL_LT_RSQRT;
  ASM_REWRITE_TAC[arith `y pow 2 = y*y`];
  FIRST_X_ASSUM_ST `<` MP_TAC;
  BY(MESON_TAC[arith `a < y ==> a <= y`;arith `y*y = y pow 2`;REAL_LE_POW_2;REAL_LE_TRANS])
  ]);;
  (* }}} *)

let REAL_WLOG_DS_LEMMA = 
prove_by_refinement(
  `!P. (!(y1:A) y2 y3 (y4:A) y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y3 y2 y4 y6 y5) /\
    (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y5 y6 y4 y2 y3) /\
    (!y1 y2 y3 y4 y5 y6. (y3 <= y2) /\ (y5 <= y2) /\ (y6 <= y2) 
         ==>
       P y1 y2 y3 y4 y5 y6) ==>
    (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  SUBGOAL_THEN `?a.  a IN {y2,y3,y5,y6} /\ (!x. x IN {y2,y3,y5,y6} ==> x <= a)` MP_TAC;
    MATCH_MP_TAC Merge_ineq.REAL_FINITE_MAX_EXISTS;
    BY(REWRITE_TAC[ FINITE_INSERT ; FINITE_EMPTY;NOT_INSERT_EMPTY]);
  REPEAT WEAK_STRIP_TAC;
  REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC);
  REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
  REWRITE_TAC[MESON[] `(!x. x = y2 \/ x = y3 \/ x = y5 \/ x = y6 ==> x <= a) = (y2 <= a /\ y3 <= a /\ y5 <= a /\ y6 <= a)`];
  BY(DISCH_THEN STRIP_ASSUME_TAC THEN ASM_MESON_TAC[])
  ]);;
  (* }}} *)

(*
let REAL_WLOG_DS2_LEMMA = prove_by_refinement(
`!P. (!(y1:A) y2 y3 (y4:A) y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y3 y2 y4 y6 y5) /\
    (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y5 y6 y4 y2 y3) /\
    (!y1 y2 y3 y4 y5 y6. (y3 <= y2) /\ (y5 <= y2) /\ (y6 <= y2) /\
       (y6 <= y3) 
         ==>
       P y1 y2 y3 y4 y5 y6) ==>
    (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
  (* {{{ proof *)
  [
  GEN_TAC;
  DISCH_TAC;
  MATCH_MP_TAC REAL_WLOG_DS_LEMMA;
  ASM_REWRITE_TAC[];
  BY(ASM_MESON_TAC[arith `y3 <= y6 \/ y6 <= y3`;arith `y3 <= y3`])
  ]);;
  (* }}} *)
*)

let WLOG_8673686234 = 
prove_by_refinement(
  `(!y1 y2 y3 y4 y5 y6. 
      y3 <= y2 /\ y5 <= y2 /\ y6 <= y2 ==>
      ineq [
  (sqrt8,y1,#3.0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (sqrt8,y4,&4 * h0);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
    ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
     (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
     (y4 < y1))) ==> (!y1 y2 y3 y4 y5 y6. ineq [
  (sqrt8,y1,#3.0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (sqrt8,y4,&4 * h0);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
    ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
     (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
     (y4 < y1)))`,

  (* {{{ proof *)
  [
  DISCH_TAC;
  MATCH_MP_TAC REAL_WLOG_DS_LEMMA;
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM kill;
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    REWRITE_TAC[Sphere.ineq];
    REWRITE_TAC[Merge_ineq.delta_y_sym];
    BY(REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Sphere.ineq];
  TYPIFY `delta_y y1 y5 y6 y4 y2 y3 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
    BY(MESON_TAC[Merge_ineq.delta_y_sym]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

(* Prove "8673686234" using inequalities 
"6170936724", "8673686234 a", "8673686234 b", "8673686234 c" *)

let LEMMA_8673686234 = 
prove_by_refinement(
  `
(!y1 y2 y3 y4 y5 y6. ineq [
    (&3,y1,&3);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (sqrt8,y4,&4 * h0);
    (&2,y5,#2.52);
      (&2,y6,#2.52)
  ]
  ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)) /\

(!y1 y2 y3 y4 y5 y6. ineq [
  (sqrt8,y1,#3.0);
    (&2,y2,#2.07);
    (&2,y3,#2.07);
    (sqrt8,y4,&4 * h0);
    (&2,y5,#2.07);
    (&2,y6,#2.07)
  ]
    ((y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 >   #2.75 * ((y1 + y4)/ &2 - sqrt8)) 
    )  ) /\

(!y1 y2 y3 y4 y5 y6. ineq [
  (sqrt8,y1,#3.0);
    (#2.07,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (#3.0,y4,#3.0);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
    ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
     (delta_y y1 y2 y3 y4 y5 y6 < &0)  )  ) /\

(!y1 y2 y3 y4 y5 y6. ineq [
  (sqrt8,y1,#3.0);
    (#2.07,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (sqrt8,y4,#3.0);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
    ((y2 + y3 + y5 + y6 - #7.99 >   #2.75 * ((y1 + y4)/ &2 - sqrt8)) \/
   (y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 >   #2.75 * ((y1 + y4)/ &2 - sqrt8)) \/
     (delta_y y1 y2 y3 y4 y5 y6 < &0)  )  )
==> (!y1 y2 y3 y4 y5 y6. ineq [
  (sqrt8,y1,#3.0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (sqrt8,y4,&4 * h0);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
    ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
     (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
     (y4 < y1))  )

`,

  (* {{{ proof *)
  [
  DISCH_TAC;
  MATCH_MP_TAC WLOG_8673686234;
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `delta_y` MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
  COMMENT "case a";
  ASM_CASES_TAC `y2 <= #2.07`;
    FIRST_X_ASSUM_ST `&2,y2,#2.07` MP_TAC;
    DISCH_THEN (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]);
    REWRITE_TAC[Sphere.ineq];
    REPEAT (FIRST_X_ASSUM_ST `y <= y2` MP_TAC);
    BY(REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `&2,y2,#2.07` kill;
  COMMENT "case c";
  ASM_CASES_TAC `y4 <= #3.0`;
    FIRST_X_ASSUM_ST `ineq` MP_TAC;
    DISCH_THEN (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]);
    REWRITE_TAC[Sphere.ineq];
    REPEAT (FIRST_X_ASSUM_ST `y <= y2` MP_TAC);
    BY(REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `ineq` kill;
  COMMENT "case b";
  ASM_CASES_TAC `delta_y y1 y2 y3 y4 y5 y6 < &0`;
    BY(ASM_REWRITE_TAC[Sphere.ineq]);
  ASM_CASES_TAC `y4 < y1`;
    BY(ASM_REWRITE_TAC[Sphere.ineq]);
  ASM_REWRITE_TAC[];
  COMMENT "ups";
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `&0 < ups_x (y1*y1) (y2*y2) (y6*y6)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Merge_ineq.UPS_X_POS;
    REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC);
    MP_TAC Flyspeck_constants.bounds;
    BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  TYPIFY `&0 < ups_x (y1*y1) (y3*y3) (y5*y5)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Merge_ineq.UPS_X_POS;
    REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC);
    MP_TAC Flyspeck_constants.bounds;
    BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  COMMENT "construct y4'";
  TYPIFY `?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC delta_y_root_exists;
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    MP_TAC Flyspeck_constants.bounds;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC IVT_delta_y_full [`#3.0`;`y4'`;`#2.07`;`y2`;`&2`;`y6`;`y1`;`&2`;`y5`;`&2`;`y3`];
  ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= #2.07 /\ &0 <= &2`];
  ANTS_TAC;
    FIRST_X_ASSUM_ST `ineq` kill;
    TYPIFY_GOAL_THEN `(!y2' y3' y5' y6'.       #2.07 <= y2' /\      y2' <= y2 /\      &2 <= y3' /\      y3' <= y6 /\      &2 <= y5' /\      y5' <= y5 /\      &2 <= y6' /\      y6' <= y3      ==> y_of_x delta_x1  #3.0 y2' y3' y1 y5' y6' < &0)` (unlist REWRITE_TAC);
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2'`;`y3'`;`y1`;`y5'`;`y6'`]);
      REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
      DISCH_THEN MATCH_MP_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    TYPIFY `delta_y y4' y2 y6 y1 y5 y3 = delta_y y1 y2 y3 y4' y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
      BY(MESON_TAC[Merge_ineq.delta_y_sym]);
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `ineq` kill;
    CONJ_TAC;
      BY(ASM_TAC THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC Merge_ineq.UPS_X_POS;
      ASM_REWRITE_TAC[];
      BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC Merge_ineq.UPS_X_POS;
      ASM_REWRITE_TAC[];
      BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  DISCH_THEN DISJ_CASES_TAC;
    FIRST_X_ASSUM (X_CHOOSE_THEN `y2':real` ASSUME_TAC);
    FIRST_X_ASSUM (X_CHOOSE_THEN `y6':real` ASSUME_TAC);
    FIRST_X_ASSUM (X_CHOOSE_THEN `y5':real` ASSUME_TAC);
    FIRST_X_ASSUM (X_CHOOSE_THEN `y3':real` ASSUME_TAC);
    FIRST_X_ASSUM (C INTRO_TAC [`y1`;`y2'`;`y3'`;`#3.0`;`y5'`;`y6'`]);
    ASM_REWRITE_TAC[Sphere.ineq;arith `~(&0 < &0)`;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    TYPIFY `delta_y y1 y2' y3' #3.0 y5' y6' = delta_y #3.0 y2' y6' y1 y5' y3'` (C SUBGOAL_THEN SUBST1_TAC);
      BY(MESON_TAC[Merge_ineq.delta_y_sym]);
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "second case: long diags";
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM_ST `delta_y` MP_TAC;
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[Sphere.delta_y;arith `&2 * &2 = &4`];
  TYPED_ABBREV_TAC  `u = y1' * y1' - &9` ;
  TYPIFY `y1' * y1' = &9 + u` (C SUBGOAL_THEN SUBST1_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  TYPED_ABBREV_TAC  `v = y1 * y1 - &8` ;
  TYPIFY `y1 * y1 = &8 + v` (C SUBGOAL_THEN SUBST1_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  TYPIFY `&0 <= u` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "u";
    REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`];
    GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
    BY(FIRST_X_ASSUM_ST `#3.0` MP_TAC THEN REAL_ARITH_TAC);
  TYPIFY `&0 <= v` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "v";
    TYPIFY_GOAL_THEN `!x. &0 <= x - &8 <=> sqrt8 * sqrt8 <= x` (unlist REWRITE_TAC);
      REWRITE_TAC[Nonlinear_lemma.sqrt8_2];
      BY(REAL_ARITH_TAC);
    GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
    REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `sqrt8` MP_TAC);
    BY(MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
  MATCH_MP_TAC (arith `&0 < -- x ==> ~(x = &0)`);
  TYPIFY `-- delta_x (&9 + u) (#2.07 * #2.07) (&4) (&8 + v) (&4) (&4)  = #51.81187204 +  #77.7208*u + &8* u pow 2 +  #78.4359*v + #17.7151*u*v +  u pow 2 *v + &9*v pow 2 + u* v pow 2` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[Sphere.delta_x];
    BY(REAL_ARITH_TAC);
  MATCH_MP_TAC (arith `&0 < x /\ &0 <= y ==> &0 < x + y`);
  CONJ_TAC;
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[arith `v pow 2 = v*v`];
  REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`));
  GMATCH_SIMP_TAC REAL_LE_MUL;
  REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL);
  ASM_REWRITE_TAC[];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let WLOG_5691615370 = 
prove_by_refinement(
  `(!y1 y2 y3 y4 y5 y6. ineq
  [
  (#3.0,y1,#3.0);
  (&2,y2,#2.52);
  (&2,y3,#2.52);
  (#3.0,y4,#3.0);
  (&2,y5,#2.52);
  (&2,y6,#2.52)
  ]
  ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472) \/
   (y2 < y3) \/ (y2 < y5) \/ (y2 < y6 ) \/ (y3 < y6))) ==>
  (!y1 y2 y3 y4 y5 y6. ineq
  [
  (#3.0,y1,#3.0);
  (&2,y2,#2.52);
  (&2,y3,#2.52);
  (#3.0,y4,#3.0);
  (&2,y5,#2.52);
  (&2,y6,#2.52)
  ]
  ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472)))`,

  (* {{{ proof *)
  [
  ONCE_REWRITE_TAC[MESON[] `!P. (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6) <=> (!y2 y3 y5 y6 y1 y4. P y1 y2 y3 y4 y5 y6)`];
  DISCH_TAC;
  MATCH_MP_TAC Terminal.REAL_WLOG_SQUARE2_LEMMA;
  CONJ_TAC;
    REPEAT GEN_TAC;
    REWRITE_TAC[Sphere.ineq;Merge_ineq.delta_y_sym];
    TYPIFY `delta_y y1 y5 y6 y4 y2 y2' = delta_y y1 y2 y2' y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
      BY(MESON_TAC[Merge_ineq.delta_y_sym]);
    REWRITE_TAC[REAL_ADD_AC];
    BY(MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Sphere.ineq];
  RULE_ASSUM_TAC (REWRITE_RULE[Sphere.ineq]);
  BY(ASM_MESON_TAC[arith `x <= y ==> ~(y < x)`])
  ]);;
  (* }}} *)


(* Use 5584033259 and 6170936724 and 5691615370  to prove the lemma. *)

let LEMMA_5691615370 = 
prove_by_refinement(
  `
(!y1 y2 y3 y4 y5 y6. ineq [
    (&3,y1,&4 * h0);
    (&2,y2,#2.472);
    (&2,y3,#2.472);
    (&3,y4,&4 * h0);
    (&2,y5,#2.472);
      (&2,y6,#2.472)
  ]
  ( y1 < &4 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 )) /\

 (!y1 y2 y3 y4 y5 y6. ineq [
    (&3,y1,&3);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (sqrt8,y4,&4 * h0);
    (&2,y5,#2.52);
      (&2,y6,#2.52)
  ]
  ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)) /\

(!y1 y2 y3 y4 y5 y6. ineq
  [
  (#3.0,y1,#3.0);
  (&2,y2,#2.52);
  (&2,y3,#2.52);
  (#3.0,y4,#3.0);
  (&2,y5,#2.52);
  (&2,y6,#2.52)
  ]
  ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472) \/
   (y2 < y3) \/ (y2 < y5) \/ (y2 < y6 ) \/ (y3 < y6))) ==>

(!y1 y2 y3 y4 y5 y6. ineq
  [
  (#3.0,y1,&4 * h0);
  (&2,y2,#2.52);
  (&2,y3,#2.52);
  (#3.0,y4,&4 * h0);
  (&2,y5,#2.52);
  (&2,y6,#2.52)
  ]
  ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472)))
  `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonf_ups_126];
  STRIP_TAC;
  FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP WLOG_5691615370));
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  ASM_CASES_TAC `delta_y y1 y2 y3 y4 y5 y6 < &0`;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  COMMENT "construct y4'";
  TYPIFY `?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC delta_y_root_exists;
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "bound 4 on diagonal";
  PROOF_BY_CONTR_TAC;
  TYPIFY `y2 <= #2.472 /\ y3 <= #2.472 /\ y5 <= #2.472 /\ y6 <= #2.472` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  TYPIFY `y1 < &4` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `y1 < &4` (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]);
    ASM_REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    DISCH_THEN MATCH_MP_TAC;
    BY(REPLICATE_TAC 17 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  INTRO_TAC IVT_delta_y_full [`#3.0`;`y4'`;`&2`;`y2`;`&2`;`y6`;`y1`;`&2`;`y5`;`&2`;`y3`];
  ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= &2`];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    FIRST_X_ASSUM_ST `ineq` kill;
    TYPIFY_GOAL_THEN `(!y2' y3' y5' y6'.      &2 <= y2' /\      y2' <= y2 /\      &2 <= y3' /\      y3' <= y6 /\      &2 <= y5' /\      y5' <= y5 /\      &2 <= y6' /\      y6' <= y3      ==> y_of_x delta_x1  #3.0 y2' y3' y1 y5' y6' < &0)` (unlist REWRITE_TAC);
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2'`;`y3'`;`y1`;`y5'`;`y6'`]);
      REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
      DISCH_THEN MATCH_MP_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
    TYPIFY `delta_y y4' y2 y6 y1 y5 y3 = delta_y y1 y2 y3 y4' y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
      BY(MESON_TAC[Merge_ineq.delta_y_sym]);
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `ineq` kill;
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    CONJ_TAC;
      GEN_TAC;
      X_GEN_TAC `y6':real`;
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC Merge_ineq.UPS_X_POS;
      BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    CONJ_TAC;
      GEN_TAC;
      X_GEN_TAC `y3':real`;
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC Merge_ineq.UPS_X_POS;
      BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  TYPIFY `!z1 z4.  #3.0 <= z1 /\ #3.0 <= z4 ==> delta_y z1 (&2) (&2) z4 (&2) (&2) < &0` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[Sphere.delta_y;arith `&2 * &2 = &4`];
    REPEAT WEAKER_STRIP_TAC;
    TYPED_ABBREV_TAC  `u = z1 * z1 - &9` ;
    TYPIFY `z1 * z1 = &9 + u` (C SUBGOAL_THEN SUBST1_TAC);
      BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
    TYPED_ABBREV_TAC  `v = z4 * z4 - &9` ;
    TYPIFY `z4 * z4 = &9 + v` (C SUBGOAL_THEN SUBST1_TAC);
      BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
    TYPIFY `&0 <= u` (C SUBGOAL_THEN ASSUME_TAC);
      EXPAND_TAC "u";
      REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`];
      GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `#3.0` MP_TAC) THEN REAL_ARITH_TAC);
    TYPIFY `&0 <= v` (C SUBGOAL_THEN ASSUME_TAC);
      EXPAND_TAC "v";
      REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`];
      GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `#3.0` MP_TAC) THEN REAL_ARITH_TAC);
    MATCH_MP_TAC (arith `&0 < -- x ==> x < &0`);
    TYPIFY `-- delta_x (&9 + u) (&4) (&4) (&9 + v) (&4) (&4)  = &162 + &99*u + &9*u*u + &99*v +  &20*u*v + u*u*v + &9*v*v +  u*v*v` (C SUBGOAL_THEN SUBST1_TAC);
      REWRITE_TAC[Sphere.delta_x];
      BY(REAL_ARITH_TAC);
    MATCH_MP_TAC (arith `&0 < x /\ &0 <= y ==> &0 < x + y`);
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`));
    REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL);
    ASM_REWRITE_TAC[];
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[DE_MORGAN_THM;NOT_EXISTS_THM];
  CONJ2_TAC;
    GEN_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`y1'`;`y1`]);
    ASM_REWRITE_TAC[];
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  GEN_TAC;
  X_GEN_TAC `y6':real`;
  GEN_TAC;
  X_GEN_TAC `y3':real`;
  REWRITE_TAC[GSYM DE_MORGAN_THM];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC IVT_delta_y_full [`#3.0`;`y1`;`&2`;`y2'`;`&2`;`y3'`;`#3.0`;`&2`;`y5'`;`&2`;`y6'`];
  ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= &2 /\ &0 < #3.0`];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    FIRST_X_ASSUM_ST `ineq` kill;
    TYPIFY_GOAL_THEN `(!y2 y3 y5 y6.      &2 <= y2 /\      y2 <= y2' /\      &2 <= y3 /\      y3 <= y3' /\      &2 <= y5 /\      y5 <= y5' /\      &2 <= y6 /\      y6 <= y6'      ==> y_of_x delta_x1  #3.0 y2 y3  #3.0 y5 y6 < &0)` (unlist REWRITE_TAC);
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2''`;`y3''`;`#3.0`;`y5''`;`y6''`]);
      REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
      DISCH_THEN MATCH_MP_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
    TYPIFY `delta_y y1 y2' y3' #3.0 y5' y6' = delta_y #3.0 y2' y6' y1 y5' y3'` (C SUBGOAL_THEN SUBST1_TAC);
      BY(MESON_TAC[Merge_ineq.delta_y_sym]);
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `ineq` kill;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC Merge_ineq.UPS_X_POS;
      BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC Merge_ineq.UPS_X_POS;
    BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  TYPIFY_GOAL_THEN `~(?y1.  #3.0 < y1 /\ delta_y y1 (&2) (&2)  #3.0 (&2) (&2) = &0)` (unlist REWRITE_TAC);
    REWRITE_TAC[NOT_EXISTS_THM];
    GEN_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`y1'`;`#3.0`]);
    BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  REWRITE_TAC[NOT_EXISTS_THM];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2''`;`y3''`;`#3.0`;`y5''`;`y6''`]);
  ASM_REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  BY(REPLICATE_TAC 37 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)


end;;