(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*                                                                           *)
(*      Author : TRIEU THI DIEP                                             *)
(* Date: 2010-05-14                                                           *)
(*      Number  : 2158872499                                                 *)
(*                                                                           *)
(* ========================================================================= *)

(*
This contains the second derivative calculation of  g(t) in calculation 2158872499.
*)

(*
changes: extension changed from .ml to .hl,
wrapped all files in a module.
needs -> flyspeck_needs.
merged two compute files,
open Sphere,
open Vukhacky_tactics,
replaced h0 with hz to avoid conflict with constant h0.
*)

flyspeck_needs "nonlinear/vukhacky_tactics.hl";;

module Compute_2158872499 = struct


  open Sphere;;
  open Vukhacky_tactics;;
  open Trigonometry1;;
  open Trigonometry2;;

(* ========================================================================== *)

let ATN_UPS_X_BREAKDOWN1 = 
prove_by_refinement (
 `!a b c.
     &0 < (a + b + c) * (a + b - c) * (b + c - a) * (c + a - b)
     ==> arclength a b c =
         pi / &2 +
         atn
         ((c * c - a * a - b * b) /
          sqrt ((a + b + c) * (a + b - c) * (b + c - a) * (c + a - b)))`,


[(REPEAT STRIP_TAC);
 (SUBGOAL_THEN `ups_x (a * a) (b * b) (c * c) = (a + b + c) * (a + b - c) * 
  (b + c - a) * (c + a - b)` ASSUME_TAC);
 (REWRITE_TAC[ups_x]);
 (REAL_ARITH_TAC);
 (REWRITE_TAC[arclength]);
 AP_TERM_TAC;
 (ASM_REWRITE_TAC[]);
 (ABBREV_TAC `S = (a + b + c) * (a + b - c) * (b + c - a) * (c + a - b)`);
 (SUBGOAL_THEN `&0 < sqrt S` ASSUME_TAC);
 (MATCH_MP_TAC SQRT_POS_LT);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[ATN2_BREAKDOWN])]);;
 
(* ========================================================================== *)

let compute_one_first = 
prove_by_refinement (
 `!y1 y2 s hz g x.
     &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
     &2 <= y2 /\ y2 <= &2 * hz /\
     s = {t | y1 - &4 < t /\ t < &4 - y2} /\
     g = (\t. arclength y1 (y2 + t) (&2)) /\ x IN s /\
     g' = (\x. --((y2 + x) pow 2 - y1 pow 2 + &4) /
       ((y2 + x) *
        sqrt
        ((y1 + (y2 + x) + &2) *
         (y1 + (y2 + x) - &2) *
         ((y2 + x) + &2 - y1) *
         (&2 + y1 - (y2 + x)))))
     ==> (g has_real_derivative g' x) (atreal x within s)`,


[(REPEAT STRIP_TAC);
 REWRITE_TAC[ASSUME `g' = (\x. --((y2 + x) pow 2 - y1 pow 2 + &4) /
       ((y2 + x) *
        sqrt
        ((y1 + (y2 + x) + &2) *
         (y1 + (y2 + x) - &2) *
         ((y2 + x) + &2 - y1) *
         (&2 + y1 - (y2 + x)))))`];
  (SUBGOAL_THEN `!t. t IN s ==> 
     &0 < (y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
          ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t))` ASSUME_TAC);

  (GEN_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);

   (SUBGOAL_THEN 
      `&0 < y1 + (y2 + t) - &2 /\ &0 < y1 + (y2 + t) + &2 /\
       &0 < (y2 + t) + &2 - y1 /\ &0 < &2 + y1 - (y2 + t)` ASSUME_TAC);
    ASM_REAL_ARITH_TAC;
  (ASM_MESON_TAC[REAL_LT_MUL]);

(* ========================================================================== *)
(*         SUBGOAL 3                                                          *)
(* ========================================================================== *)

 (ABBREV_TAC `f1 = (\t. (y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
                         ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t)))`);
 (ABBREV_TAC `f1' = &4 * (y2 + x) * (y1 pow 2 - (y2 + x) pow 2 + &4)`);
 (ABBREV_TAC `P ={x| &0 < x}`);
 (ABBREV_TAC `f2 = (\t. sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
                              ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t))))`);

  (SUBGOAL_THEN `f2 = (\t:real. sqrt (f1 t))` ASSUME_TAC);
  (EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN MESON_TAC[]); 

 (ABBREV_TAC `g2' = (\x. inv (&2 * sqrt x))`);
 (ABBREV_TAC `f2' = f1' * g2' ((f1:real->real) x)`);

 (SUBGOAL_THEN `(f2 has_real_derivative f2') (atreal x within s)`ASSUME_TAC);  
 (EXPAND_TAC "f2'" THEN PURE_REWRITE_TAC[ASSUME `f2 = (\t:real. sqrt (f1 t))`]);

  (SUBGOAL_THEN `(f1 has_real_derivative f1') (atreal x within s) /\ P (f1 x)` 
   ASSUME_TAC);
   STRIP_TAC;
  (EXPAND_TAC "f1" THEN EXPAND_TAC "f1'");
  (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM] THEN EXPAND_TAC "f1");
  (MP_TAC (ASSUME `(x:real) IN s`) THEN ASM_REWRITE_TAC[]);
  (FIRST_X_ASSUM MP_TAC);

  (SUBGOAL_THEN `!x. P x ==> 
    (sqrt has_real_derivative (g2':real->real) x) (atreal x)` ASSUME_TAC);
  (EXPAND_TAC "g2'" THEN REWRITE_TAC[BETA_THM]);
  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);  
  (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);
  (FIRST_X_ASSUM MP_TAC);

 (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);

(* ------------------------------------------------------------------------- *)

 (ABBREV_TAC `f3 = (\t. (&2 * &2 - y1 * y1 - (y2 + t) * (y2 + t)) / 
                      sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
                            ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t))))`);
 (ABBREV_TAC `h = (\t. (&2 * &2 - y1 * y1 - (y2 + t) * (y2 + t)))`);

 (SUBGOAL_THEN `f3 = (\t:real. h t / f2 t)` ASSUME_TAC);
 (EXPAND_TAC "f2" THEN EXPAND_TAC "h" THEN EXPAND_TAC "f3");
 (REWRITE_TAC[]);

 (SUBGOAL_THEN `(h has_real_derivative -- &2 * (y2 + x)) (atreal x within s) /\
                (f2 has_real_derivative f2') (atreal x within s) /\
               ~(f2 x = &0)` ASSUME_TAC);
 (REPEAT CONJ_TAC);

  (EXPAND_TAC "h" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
  (ASM_REWRITE_TAC[]);
  (ASM_REWRITE_TAC[]);
  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
  (MATCH_MP_TAC SQRT_POS_LT);
  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (SUBGOAL_THEN `(f3 has_real_derivative 
                 ((-- &2 * (y2 + x)) * f2 x - h x * f2') / f2 x pow 2)
                 (atreal x within s)` ASSUME_TAC);
 (PURE_REWRITE_TAC[ASSUME `f3 = (\t:real. h t / f2 t)`]);
 (FIRST_X_ASSUM MP_TAC);
 (REWRITE_TAC[HAS_REAL_DERIVATIVE_DIV_WITHIN]);

(* --------------------------------------------------------------------------*)

 (ABBREV_TAC `F1 = (\t. atn ((&2 * &2 - y1 * y1 - (y2 + t) * (y2 + t)) / 
                           sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
                            ((y2 + t) + &2 - y1)  * (&2 + y1 - (y2 + t)))))`);
 (ABBREV_TAC `f3' = ((-- &2 * (y2 + x)) * f2 x - h x * f2') / f2 x pow 2`);
 (ABBREV_TAC `h' = (\x. inv (&1 + x pow 2))`);

 (SUBGOAL_THEN `F1 = (\t:real. atn (f3 t))` ASSUME_TAC);
 (EXPAND_TAC "f3" THEN EXPAND_TAC "F1" THEN ASM_REWRITE_TAC[]);

 (SUBGOAL_THEN `(F1 has_real_derivative f3' * inv (&1 + f3 x pow 2)) 
                 (atreal x within s)` ASSUME_TAC);
 (REWRITE_TAC[ASSUME `F1 = (\t:real. atn (f3 t))`]);

  (SUBGOAL_THEN `(f3 has_real_derivative f3') (atreal x within s) /\ 
                   (:real) (f3 x)` ASSUME_TAC);
  (ASM_REWRITE_TAC[]);
  (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
  (FIRST_X_ASSUM MP_TAC);

  (SUBGOAL_THEN `!x. (:real) x ==> (atn has_real_derivative (h':real->real) x)
                                     (atreal x)` ASSUME_TAC);
  (EXPAND_TAC "h'" THEN REWRITE_TAC[BETA_THM]);
  (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);
  (FIRST_X_ASSUM MP_TAC);

  (SUBGOAL_THEN `inv (&1 + f3 (x:real) pow 2) = h' (f3 x)` ASSUME_TAC);
  (EXPAND_TAC "h'" THEN REWRITE_TAC[]);
 
 (REWRITE_TAC[ASSUME `inv (&1 + f3 (x:real) pow 2) = h'( f3 x)`]);
 (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);

(* --------------------------------------------------------------------------*)

 (SUBGOAL_THEN `f1 x = &4 * (y1 * (y2 + x)) pow 2 - 
                 (&2 * &2 - y1 * y1 - (y2 + x) * (y2 + x)) pow 2` ASSUME_TAC);
 (EXPAND_TAC "f1" THEN REAL_ARITH_TAC);

 (SUBGOAL_THEN `inv (&1 + f3 x pow 2) = 
                (f1 x) / (&4 * (y1 * (y2 + x)) pow 2)` ASSUME_TAC);
 (EXPAND_TAC "f3");
 (REWRITE_TAC[REAL_POW_DIV]);

 (SUBGOAL_THEN `&0 <= (y1 + (y2 + x) + &2) * (y1 + (y2 + x) - &2) *
                      ((y2 + x) + &2 - y1) * (&2 + y1 - (y2 + x))` ASSUME_TAC);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 (MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (SUBGOAL_THEN `sqrt ((y1 + (y2 + x) + &2) * (y1 + (y2 + x) - &2) *
        ((y2 + x) + &2 - y1) * (&2 + y1 - (y2 + x))) pow 2 = f1 x` ASSUME_TAC);
 (EXPAND_TAC "f1" THEN ASM_SIMP_TAC [SQRT_POW_2]);

 (PURE_ONCE_ASM_REWRITE_TAC[]);
 (ONCE_ASM_REWRITE_TAC[GSYM REAL_INV_DIV]);
 (AP_TERM_TAC);
 (ONCE_ASM_REWRITE_TAC[REAL_INV_DIV] THEN PURE_ONCE_ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC (REAL_ARITH `&1 = x - y ==> &1 + y = x `));
 (REWRITE_TAC [REAL_ARITH `x / y - z / y = (x - z) / y`]);
 (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
 (REWRITE_TAC[GSYM (ASSUME `f1 x = &4 * (y1 * (y2 + x)) pow 2 -
   (&2 * &2 - y1 * y1 - (y2 + x) * (y2 + x)) pow 2`)]);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(&0 = a)`));
 (MP_TAC (ASSUME `x:real IN s`));
 (EXPAND_TAC "f1" THEN ASM_REWRITE_TAC[]);

(* ========================================================================== *)

 (SUBGOAL_THEN ` ((-- &2 * (y2 + x)) * f2 x - h x * f2') = 
   -- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4) / f2 x`
 ASSUME_TAC);

 (ABBREV_TAC `X = ((-- &2 * (y2 + x)) * f2 x - h x * f2')`);
 (REWRITE_TAC[REAL_ARITH `x * y / z = (x * y) / z`]);
 (ABBREV_TAC 
   `Y = (-- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);

 (SUBGOAL_THEN `Y / f2 (x:real) = X <=> Y = X * f2 x` ASSUME_TAC);
 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 (REPLICATE_TAC 2 (ONCE_ASM_REWRITE_TAC[]) THEN MATCH_MP_TAC SQRT_POS_LT);
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 (ONCE_ASM_REWRITE_TAC[]);

 (EXPAND_TAC "X" THEN EXPAND_TAC "Y");
 (EXPAND_TAC "f2'" THEN EXPAND_TAC "h" THEN EXPAND_TAC "g2'");
 (ONCE_REWRITE_TAC[REAL_ARITH `(a - b) * c = a * c - b * c`]);

 (SUBGOAL_THEN `inv (&2 * sqrt (f1 x)) * f2 (x:real) = &1 / &2` ASSUME_TAC);
 (REWRITE_TAC[ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 (ONCE_REWRITE_TAC[REAL_ARITH `a * sqrt b = (a * (&2 * sqrt b)) / &2`]);
 (AP_THM_TAC THEN AP_TERM_TAC);
 (MATCH_MP_TAC REAL_MUL_LINV);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 (MATCH_MP_TAC REAL_LT_MUL);
 (REWRITE_TAC[REAL_ARITH `&0 < &2`]);
 (MATCH_MP_TAC SQRT_POS_LT);
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b) * c * d`]);
 (PURE_REWRITE_TAC[ASSUME `inv (&2 * sqrt (f1 x)) * f2 (x:real) = &1 / &2`]);
 (REWRITE_TAC[REAL_ARITH `(a * f2 x) * f2 x = a * (f2 (x:real) pow 2)`]);

 (SUBGOAL_THEN `f2 (x:real) pow 2 = f1 x` ASSUME_TAC);
 (REWRITE_TAC [ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 (MATCH_MP_TAC SQRT_POW_2);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (REWRITE_TAC[ASSUME `f2 (x:real) pow 2 = f1 x`]);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "Y" THEN EXPAND_TAC "f1'");
 REAL_ARITH_TAC;

(* ========================================================================= *)

 (SUBGOAL_THEN 
  `f3' * inv (&1 + f3 x pow 2) = 
   -- ((y2 + x) pow 2 - y1 pow 2 + &4) / ((y2 + x) * f2 x)` ASSUME_TAC);
 (EXPAND_TAC "f3'");
 (REWRITE_TAC[ASSUME 
  `inv (&1 + f3 x pow 2) = f1 x / (&4 * (y1 * (y2 + x)) pow 2)`]);
 (REWRITE_TAC[ASSUME `(-- &2 * (y2 + x)) * f2 x - h x * f2' =
      -- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4) / f2 x`]);

 (SUBGOAL_THEN `f2 (x:real) pow 2 = f1 x` ASSUME_TAC);
 (REWRITE_TAC [ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 (MATCH_MP_TAC SQRT_POW_2);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `f2 (x:real) pow 2 = f1 x`]);

 (ONCE_REWRITE_TAC [REAL_ARITH `a / b * c / d = (a / d) * c / b`]);
 (MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 /\ x = y ==> x * a = y`));
 STRIP_TAC;
 (MATCH_MP_TAC REAL_DIV_REFL);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (ABBREV_TAC `X = 
  (-- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4) / f2 x)`);
 (ABBREV_TAC 
   `Y = --((y2 + x) pow 2 - y1 pow 2 + &4) / ((y2 + x) * f2 x)`);
 (ABBREV_TAC `Z = (&4 * (y1 * (y2 + x)) pow 2)`);

 (SUBGOAL_THEN `X / Z = Y <=> X = Y * Z` ASSUME_TAC);
 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 (EXPAND_TAC "Z");
 (MATCH_MP_TAC REAL_LT_MUL);
 (REWRITE_TAC[REAL_ARITH `&0 < &4`]);
 (MATCH_MP_TAC REAL_POW_LT);
 (MATCH_MP_TAC REAL_LT_MUL);
 STRIP_TAC;
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC (REAL_ARITH `&0 <= y1 + y2 - &4 /\ y1 + y2 - &4 < s ==> &0 < s`));
 (STRIP_TAC);
 (MATCH_MP_TAC (REAL_ARITH `&2 <= y1 /\ &2 <= y2 ==> &0 <= y1 + y2 - &4`));
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (REAL_ARITH `y1 - &4 < x ==> y1 + y2 - &4 < y2 + x`));
 (MP_TAC (ASSUME `x:real IN s`));
 (REWRITE_TAC[ASSUME `s = {t | y1 - &4 < t /\ t < &4 - y2}`]);
 (PURE_REWRITE_TAC[IN_ELIM_THM]);
 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (ONCE_ASM_REWRITE_TAC[]);

 (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
 (REWRITE_TAC [REAL_ARITH `a * b / c = (a * b) / c`]); 
 (REWRITE_TAC[REAL_ARITH 
  `--((y2 + x) pow 2 - y1 pow 2 + &4) / ((y2 + x) * f2 x) *
   &4 *  (y1 * (y2 + x)) pow 2 =
   (-- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4)) * (y2 + x)
   / (f2 x * (y2 + x))`]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
 CONJ_TAC;
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 (MATCH_MP_TAC (REAL_ARITH `&0 <= y1 + y2 - &4 /\ y1 + y2 - &4 < s ==> &0 < s`));
 (STRIP_TAC);
 (MATCH_MP_TAC (REAL_ARITH `&2 <= y1 /\ &2 <= y2 ==> &0 <= y1 + y2 - &4`));
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (REAL_ARITH `y1 - &4 < x ==> y1 + y2 - &4 < y2 + x`));
 (MP_TAC (ASSUME `x:real IN s`));
 (REWRITE_TAC[ASSUME `s = {t | y1 - &4 < t /\ t < &4 - y2}`]);
 (PURE_REWRITE_TAC[IN_ELIM_THM]);
 (STRIP_TAC THEN ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 (ONCE_ASM_REWRITE_TAC[]);
 (ONCE_ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SQRT_POS_LT);
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

(* ========================================================================== *)

 (SUBGOAL_THEN 
  `(F1 has_real_derivative --((y2 + x) pow 2 - y1 pow 2 + &4) / 
   ((y2 + x) * f2 x)) (atreal x within s)` ASSUME_TAC);
 (ASM_MESON_TAC[]);

 (SUBGOAL_THEN `
  (F1 has_real_derivative --((y2 + x) pow 2 - y1 pow 2 + &4) /   
  ((y2 + x) * sqrt
           ((y1 + (y2 + x) + &2) *
            (y1 + (y2 + x) - &2) *
            ((y2 + x) + &2 - y1) *
            (&2 + y1 - (y2 + x)))))
      (atreal x within s)` ASSUME_TAC);
 (FIRST_X_ASSUM MP_TAC THEN EXPAND_TAC "f2");
 (REWRITE_TAC[]);

 (ABBREV_TAC `F2 = (\x:real. pi / &2 + F1 x)`);
 (ABBREV_TAC `pi_2 = (\x:real. pi / &2 )`);

 (SUBGOAL_THEN `(F2 has_real_derivative --((y2 + x) pow 2 - y1 pow 2 + &4) /
  ((y2 + x) *
   sqrt
   ((y1 + (y2 + x) + &2) *
    (y1 + (y2 + x) - &2) *
    ((y2 + x) + &2 - y1) *
    (&2 + y1 - (y2 + x)))))
 (atreal x within s)` ASSUME_TAC);

 (SUBGOAL_THEN `F2 = (\x:real. pi_2 x + F1 x)` ASSUME_TAC);
 (EXPAND_TAC "F2" THEN EXPAND_TAC "F1" THEN EXPAND_TAC "pi_2");
 (REWRITE_TAC[]);

 (REWRITE_TAC[ASSUME `F2 = (\x:real. pi_2 x + F1 x)`]);
 (ABBREV_TAC `F1' = (--((y2 + x) pow 2 - y1 pow 2 + &4) /
  ((y2 + x) *
   sqrt
   ((y1 + (y2 + x) + &2) *
    (y1 + (y2 + x) - &2) *
    ((y2 + x) + &2 - y1) *
    (&2 + y1 - (y2 + x)))))`);

 (SUBGOAL_THEN `((\x. pi_2 x + F1 x) has_real_derivative &0 + F1')
 (atreal x within s)` ASSUME_TAC);

 (SUBGOAL_THEN `(pi_2 has_real_derivative (&0)) (atreal x within s)`
   ASSUME_TAC);
 (EXPAND_TAC "pi_2");
 (REAL_DIFF_TAC THEN REAL_ARITH_TAC);

 (FIRST_X_ASSUM MP_TAC);
 (MP_TAC (ASSUME `(F1 has_real_derivative F1') (atreal x within s)`));
 (REWRITE_TAC[MESON[] `(a ==> b ==> c) <=> (b /\ a ==> c)`]);
 (MESON_TAC[HAS_REAL_DERIVATIVE_ADD]);
 (ASM_MESON_TAC[REAL_ARITH `&0 + a = a`]);


 (ABBREV_TAC `F1' = (--((y2 + x) pow 2 - y1 pow 2 + &4) /
  ((y2 + x) *
   sqrt
   ((y1 + (y2 + x) + &2) *
    (y1 + (y2 + x) - &2) *
    ((y2 + x) + &2 - y1) *
    (&2 + y1 - (y2 + x)))))`);

 (SUBGOAL_THEN 
  `(!x':real. (x':real) IN s /\ abs (x' - x) < &1 ==> 
   (F2:real -> real) x' = g x')` ASSUME_TAC);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]); 
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]); 
 (EXPAND_TAC "F2"); 
 (EXPAND_TAC "F1");
 (MATCH_MP_TAC ATN_UPS_X_BREAKDOWN1);
 (MP_TAC (ASSUME `x':real IN s`));
 (ASM_REWRITE_TAC[]);
 (MP_TAC (ASSUME `(F2 has_real_derivative F1') (atreal x within s)`));
 (MP_TAC (ASSUME `!x'. x' IN s /\ abs (x' - x) < &1 ==> (F2:real->real) x' = g x'`));
 (MP_TAC (ASSUME `x:real IN s`));
 (MP_TAC (REAL_ARITH `&0 < &1`));
 (MESON_TAC[HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN])]);;
(* ========================================================================= *)


let compute_one_second = 
prove_by_refinement (
 `!y1 y2 s hz g x.
     &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
     &2 <= y2 /\ y2 <= &2 * hz /\
     s = {t | y1 - &4 < t /\ t < &4 - y2} /\
     g = (\t. --((y2 + t) pow 2 - y1 pow 2 + &4) /
           ((y2 + t) *
            sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
            ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t)))))
     ==> (g has_real_derivative
          (-- &64 + &48 * y1 pow 2 - &12 * y1 pow 4 + y1 pow 6 +
          &80 * y2 pow 2 - &8 * y1 pow 2 * y2 pow 2 - &3 * y1 pow 4 * y2 pow 2 -
          &12 * y2 pow 4 + &3 * y1 pow 2 * y2 pow 4 - y2 pow 6) /
          (y2 pow 2 *  sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
          ups_x (y1 pow 2) (y2 pow 2) (&4)))
         (atreal (&0) within s)`,

[ REPEAT STRIP_TAC;

   (SUBGOAL_THEN `&0 IN s` ASSUME_TAC);
   (PURE_ASM_REWRITE_TAC[IN_ELIM_THM]);
   CONJ_TAC; 
     (REWRITE_TAC[REAL_ARITH `a - b < &0 <=> a < b`]);
     (MATCH_MP_TAC (REAL_ARITH `y1 <= &2 * hz /\ &2 * hz < &4 ==> y1 < &4`));
     (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);
     ASM_REAL_ARITH_TAC;

(* ========================================================================== *)

  (SUBGOAL_THEN  
    `!t. t IN s ==>  &0 < (y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
         ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t))` ASSUME_TAC);
  (GEN_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);

    (SUBGOAL_THEN `&0 < y1 + (y2 + t) - &2 /\ &0 < y1 + (y2 + t) + &2 /\ 
          &0 < (y2 + t) + &2 - y1 /\ &0 < &2 + y1 - (y2 + t)` ASSUME_TAC);
    (ASM_REAL_ARITH_TAC);
    (ASM_MESON_TAC[REAL_LT_MUL]);

 (ABBREV_TAC `f1 = (\t. --((y2 + t) pow 2 - y1 pow 2 + &4))`);
 (ABBREV_TAC `f2 = (\t. (y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
             ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t)))`);
 (ABBREV_TAC `f3 = (\t:real. sqrt (f2 t))`);
 (ABBREV_TAC `f4 = (\t:real. y2 + t)`);
 (ABBREV_TAC `f5 = (\t:real. f4 t * f3 t )`);

(SUBGOAL_THEN `&0 < f2 (&0)` ASSUME_TAC);
(EXPAND_TAC "f2" THEN MP_TAC (ASSUME`((&0):real) IN s`) THEN ASM_REWRITE_TAC[]);

(SUBGOAL_THEN `(f1 has_real_derivative -- &2 * y2) (atreal (&0) within s)`
  ASSUME_TAC);
(EXPAND_TAC "f1" THEN REAL_DIFF_TAC);
(REWRITE_TAC[ARITH_RULE `2 - 1 = 1`] THEN REAL_ARITH_TAC);

(ABBREV_TAC `f2' = &4 * y2 * (y1 pow 2 - y2 pow 2 + &4)`);
(ABBREV_TAC `P ={x| &0 < x}`);
(ABBREV_TAC `g3' = (\x. inv (&2 * sqrt x))`);
(ABBREV_TAC `f3' = f2' * g3' ((f2:real->real) (&0))`);

 (SUBGOAL_THEN 
    `(f3 has_real_derivative f3') (atreal (&0) within s)` ASSUME_TAC);
 (EXPAND_TAC "f3'" THEN EXPAND_TAC "f3");

(SUBGOAL_THEN `(f2 has_real_derivative f2') (atreal (&0) within s) /\ 
               P (f2 (&0))` MP_TAC);
  STRIP_TAC;

  (EXPAND_TAC "f2" THEN EXPAND_TAC "f2'");
  (REAL_DIFF_TAC THEN REWRITE_TAC[POW_2] THEN REAL_ARITH_TAC);
  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
  (ASM_REWRITE_TAC[]);

 (SUBGOAL_THEN 
    `!x. P x ==> (sqrt has_real_derivative (g3':real->real) x) (atreal x)`
     MP_TAC);
 (EXPAND_TAC "g3'" THEN REWRITE_TAC[BETA_THM]);
 (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);  
 (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);

(REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);

(* ========================================================================== *)

(SUBGOAL_THEN `(f5 has_real_derivative f4 (&0) * f3' + &1 * f3 (&0)) 
  (atreal (&0) within s)` ASSUME_TAC);

(SUBGOAL_THEN 
  `(f4 has_real_derivative &1) (atreal (&0) within s) /\
   (f3 has_real_derivative f3') (atreal (&0) within s)` MP_TAC);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "f4" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);

(EXPAND_TAC "f5");
(REWRITE_TAC[HAS_REAL_DERIVATIVE_MUL_WITHIN]);

(* ========================================================================= *)
(*          Derivative of f1 / f5                                            *) 
(* ========================================================================= *)

(SUBGOAL_THEN `g = (\t:real. f1 t / f5 t)` ASSUME_TAC);
(ASM_REWRITE_TAC[] THEN EXPAND_TAC "f5" THEN EXPAND_TAC "f1");
(EXPAND_TAC "f4" THEN EXPAND_TAC "f3" THEN EXPAND_TAC "f2" THEN REWRITE_TAC[]);

(REWRITE_TAC[ASSUME `g = (\t:real. f1 t / f5 t)`] THEN DEL_TAC);

(SUBGOAL_THEN `((\t. f1 t / f5 t) has_real_derivative
  ((-- &2 * y2) * f5 (&0) - f1 (&0) * (f4 (&0) * f3' + &1 * f3 (&0))) / 
  f5 (&0) pow 2) (atreal (&0) within s)` ASSUME_TAC);

(SUBGOAL_THEN 
  `(f1 has_real_derivative -- &2 * y2) (atreal (&0) within s) /\
   (f5 has_real_derivative f4 (&0) * f3' + &1 * f3 (&0))
    (atreal (&0) within s) /\ ~(f5 (&0) = &0)` MP_TAC);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
(EXPAND_TAC "f5" THEN MATCH_MP_TAC REAL_LT_MUL);
STRIP_TAC;

(EXPAND_TAC "f4" THEN ASM_REAL_ARITH_TAC);
(EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);

(REWRITE_TAC[HAS_REAL_DERIVATIVE_DIV_WITHIN]);

(* ========================================================================= *)

(SUBGOAL_THEN 
`((-- &2 * y2) * f5 (&0) - f1 (&0) * (f4 (&0) * f3' + &1 * f3 (&0))) /
 f5 (&0) pow 2 =
(-- &64 + &48 * y1 pow 2 - &12 * y1 pow 4 + y1 pow 6 +
    &80 * y2 pow 2 - &8 * y1 pow 2 * y2 pow 2 - &3 * y1 pow 4 * y2 pow 2 -
    &12 * y2 pow 4 + &3 * y1 pow 2 * y2 pow 4 - y2 pow 6) /
    (y2 pow 2 *  sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
    ups_x (y1 pow 2) (y2 pow 2) (&4))` ASSUME_TAC);

(EXPAND_TAC "f5");

(SUBGOAL_THEN `f4 (&0) = (y2:real)` ASSUME_TAC);
(EXPAND_TAC "f4" THEN REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH `a pow 4 = a pow 2 * a pow 2`]);
(REWRITE_TAC[REAL_ARITH `a pow 6 = a pow 2 * a pow 2 * a pow 2`]);
(REWRITE_TAC[REAL_MUL_LID]);
(REWRITE_TAC[REAL_ARITH `a - b * (c + d) = a - b * c - b * d`]);
(REWRITE_TAC[REAL_ARITH `(-- &2 * y2) * y2 * x = ((-- &2 * y2) * y2) * x`]);
(REWRITE_TAC[REAL_ARITH `a * f3 (&0) - b - c * f3 (&0) = (a - c) * f3 (&0) - b`]);

(SUBGOAL_THEN `(-- &2 * y2) * y2 - f1 (&0) = (&4 - y1 pow 2 - y2 pow 2)` ASSUME_TAC);
(EXPAND_TAC "f1" THEN REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);

(EXPAND_TAC "f3'" THEN EXPAND_TAC "g3'");

(SUBGOAL_THEN `sqrt (f2 (&0)) = f3 (&0)` ASSUME_TAC);
(EXPAND_TAC "f3" THEN REWRITE_TAC[]);
(REWRITE_TAC[ASSUME `sqrt (f2 (&0)) = f3 (&0)`]);

(SUBGOAL_THEN 
`(&4 - y1 pow 2 - y2 pow 2) * f3 (&0) -
 f1 (&0) * y2 * f2' * inv (&2 * f3 (&0)) =
 ((&4 - y1 pow 2 - y2 pow 2) * f3 (&0) pow 2 -
  f1 (&0) * &2 * y2 pow 2 * (y1 pow 2 - y2 pow 2 + &4)) /
 f3 (&0)` ASSUME_TAC);

(PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a - b) / c = a / c - b / c`]);
(MATCH_MP_TAC (REAL_ARITH `a = b /\ c = d ==> a - c = b - d`));
STRIP_TAC;

(REWRITE_TAC[REAL_POW_2; REAL_ARITH `(a * b * c) / d = (a * b) * c / d`]);
(MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 ==> b = b * a`));
(MATCH_MP_TAC REAL_DIV_REFL);
(EXPAND_TAC "f3");
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
(MATCH_MP_TAC SQRT_POS_LT);
(ASM_REWRITE_TAC[]);

(EXPAND_TAC "f2'" THEN REWRITE_TAC[REAL_POW_2]);
(REWRITE_TAC[REAL_ARITH 
 `f1 (&0) * y2 * (&4 * y2 * (y1 * y1 - y2 * y2 + &4)) * inv (&2 * f3 (&0)) = 
  (f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4)) * &2 * 
 inv (&2 * f3 (&0))`]) ;

(ABBREV_TAC `X = (f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4)) *
 &2 * inv (&2 * f3 (&0))`);
(ABBREV_TAC `Y = (f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4))`);
(ABBREV_TAC `Z = (f3:real->real) (&0)`);

(SUBGOAL_THEN `X = Y / Z <=> X * Z = Y` ASSUME_TAC);
(MATCH_MP_TAC REAL_EQ_RDIV_EQ THEN EXPAND_TAC "Z" THEN EXPAND_TAC "f3");
(MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);

(EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
(REWRITE_TAC[REAL_ARITH 
  `((f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4)) * &2 *
    inv (&2 * f3 (&0))) * f3 (&0) =
    (f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4)) * 
    (&2 * f3 (&0)) * inv (&2 * f3 (&0))`]);

(MATCH_MP_TAC( MESON[REAL_MUL_RID] `a = &1 ==> b * a = b`));
(MATCH_MP_TAC REAL_MUL_RINV);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
(MATCH_MP_TAC REAL_LT_MUL);
(REWRITE_TAC[REAL_ARITH `&0 < &2`]);
(EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);

(ABBREV_TAC `a = y1 pow 2`);
(ABBREV_TAC `b = y2 pow 2`);

(SUBGOAL_THEN 
 `((&4 - a - b) * f3 (&0) pow 2 - f1 (&0) * &2 * b * (a - b + &4)) = 
  -- &64 + &48 * a - &12 * a * a + a * a * a + &80 * b - &8 * a * b - 
  &3 * (a * a) * b - &12 * b * b + &3 * a * b * b - b * b * b` ASSUME_TAC);

(EXPAND_TAC "f3");
(SUBGOAL_THEN `sqrt (f2 (&0)) pow 2 = f2 (&0)` ASSUME_TAC);
(MATCH_MP_TAC SQRT_POW_2);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);

(SUBGOAL_THEN `f2 (&0) = &4 * a * b - (&4 - a - b) pow 2` ASSUME_TAC);
(EXPAND_TAC "f2" THEN EXPAND_TAC "a" THEN EXPAND_TAC "b");
REAL_ARITH_TAC;
(ASM_REWRITE_TAC[]);

(EXPAND_TAC "f1");
(REWRITE_TAC[REAL_ARITH `y + &0 = y`; ASSUME `y2 pow 2 = b`]);
REAL_ARITH_TAC;

(ASM_REWRITE_TAC[]);

(ABBREV_TAC `X' = (-- &64 + &48 * a - &12 * a * a +  a * a * a +  &80 * b - 
  &8 * a * b - &3 * (a * a) * b - &12 * b * b + &3 * a * b * b - b * b * b)`);

(SUBGOAL_THEN `ups_x a b (&4) = f2 (&0)` ASSUME_TAC);
(EXPAND_TAC "f2" THEN REWRITE_TAC[ups_x]);
(EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);

(ABBREV_TAC `Z' = X' / f3 (&0) / (y2 * f3 (&0)) pow 2`);
(ABBREV_TAC `Y' = (b * f3 (&0) * f2 (&0))`);

(SUBGOAL_THEN `Z' = X' / Y' <=> Z' * Y' = X'` ASSUME_TAC);
(MATCH_MP_TAC REAL_EQ_RDIV_EQ THEN EXPAND_TAC "Y'");
(MATCH_MP_TAC REAL_LT_MUL);
STRIP_TAC;
(EXPAND_TAC "b" THEN MATCH_MP_TAC REAL_POW_LT THEN ASM_REAL_ARITH_TAC);
(MATCH_MP_TAC REAL_LT_MUL THEN EXPAND_TAC "f3");
(ASM_SIMP_TAC [SQRT_POS_LT]);
(ASM_REWRITE_TAC[]);

(EXPAND_TAC "Z'" THEN EXPAND_TAC "Y'");
(REWRITE_TAC[REAL_ARITH `a / b * c = (a * c) / b`]);

(SUBGOAL_THEN `(X' * b * f3 (&0) * f2 (&0)) / f3 (&0) = X' * b * f2 (&0)` ASSUME_TAC);
(REWRITE_TAC[REAL_ARITH `(a * b * c * d) / f = (a * b * d) * (c / f)`] );
(MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 ==> b * a = b`));
(MATCH_MP_TAC REAL_DIV_REFL);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
(EXPAND_TAC "f3");
(MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);

(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_POW_2]);
(REWRITE_TAC[REAL_ARITH `(a * b) * a * b = a pow 2 * b pow 2`]);
(SUBGOAL_THEN `f3 (&0) pow 2 = f2 (&0)` ASSUME_TAC);
(EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POW_2);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[]);

(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH `(a * b) / c = a * (b / c)`]);
(MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 ==> b * a = b`));
(REWRITE_TAC[REAL_ARITH `a * b / c = (a * b) / c`]);
(MATCH_MP_TAC REAL_DIV_REFL);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
(MATCH_MP_TAC REAL_LT_MUL);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "b" THEN MATCH_MP_TAC REAL_POW_LT THEN ASM_REAL_ARITH_TAC);

(ASM_MESON_TAC[])]);;
(* ========================================================================= *)

let COMPUTE_DERIVATIVE_ONE = 
prove_by_refinement (
 `!y1 y2 s hz g x f.
     &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
     &2 <= y2 /\ y2 <= &2 * hz /\
     s = {t | y1 - &4 < t /\ t < &4 - y2} /\
     g = (\t. arclength y1 (y2 + t) (&2)) /\
     g' = (\t. --((y2 + t) pow 2 - y1 pow 2 + &4) /
                ((y2 + t) *
                sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
               ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t)))))
==>  (!x. x IN s ==> (g has_real_derivative g' x) (atreal x within s)) /\
     (g' has_real_derivative
          (-- &64 + &48 * y1 pow 2 - &12 * y1 pow 4 + y1 pow 6 +
          &80 * y2 pow 2 - &8 * y1 pow 2 * y2 pow 2 - &3 * y1 pow 4 * y2 pow 2 -
          &12 * y2 pow 4 + &3 * y1 pow 2 * y2 pow 4 - y2 pow 6) /
          (y2 pow 2 *  sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
          ups_x (y1 pow 2) (y2 pow 2) (&4)))
         (atreal (&0) within s)`,


[(REPEAT STRIP_TAC);
 (ASM_MESON_TAC[compute_one_first]);
 (ASM_MESON_TAC[compute_one_second])]);;

let compute_two_first = 
prove_by_refinement (
 `!y1 y2 s hz g x.
   &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\ 
   &2 <= y2 /\ y2 <= &2 * hz /\
   s = {t |  y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1} /\
   g = (\t. arclength (y1 + t) (y2 - t) (&2)) /\ x IN s /\
   g' = (\x. ((y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4)) / 
             ((y1 + x) * (y2 - x) * sqrt ((y1 + y2 + &2) * (y1 + y2 - &2) * 
             (y2 - &2 * x + &2 - y1) * (&2 + y1 + &2 * x - y2))))
     ==> (g has_real_derivative g' x) (atreal x within s)`,


[(REPEAT STRIP_TAC);
 (SUBGOAL_THEN `!t. t IN s ==> 
       &0 < ((y1 + t)+ (y2 - t) + &2) * ((y1 + t)+ (y2 - t) - &2) *
       ((y2 - t) + &2 - (y1 + t)) * (&2 + (y1 + t) - (y2 - t))`   ASSUME_TAC);
 (GEN_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);
 (SUBGOAL_THEN 
     `&0 < (y1 + t) + y2 - t + &2 /\ &0 < (y1 + t) + y2 - t - &2 /\
      &0 < y2 - t + &2 - (y1 + t) /\ &0 < &2 + (y1 + t) - (y2 - t)`ASSUME_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[REAL_LT_MUL]);
 (ABBREV_TAC 
  `f1 = (\t. ((y1 + t) + y2 - t + &2) * ((y1 + t) + y2 - t - &2) *
              (y2 - t + &2 - (y1 + t)) * (&2 + (y1 + t) - (y2 - t)))`);
 (ABBREV_TAC 
  `f1' = &4 * (y1 + y2 + &2) * (y1 + y2 - &2) * (y2 - y1 - &2 * x)`);
 (ABBREV_TAC `P ={x| &0 < x}`);
 (ABBREV_TAC 
  `f2 = (\t. sqrt (((y1 + t) + y2 - t + &2) * ((y1 + t) + y2 - t - &2) *
                   (y2 - t + &2 - (y1 + t)) * (&2 + (y1 + t) - (y2 - t))))`);
 (SUBGOAL_THEN `f2 = (\t:real. sqrt (f1 t))` ASSUME_TAC);
 (EXPAND_TAC "f1"  THEN EXPAND_TAC "f2" THEN MESON_TAC[]);
 (ABBREV_TAC `g2' = (\x. inv (&2 * sqrt x))`);
 (ABBREV_TAC `f2' = f1' * g2' ((f1:real->real) x)`);
 (SUBGOAL_THEN`(f2 has_real_derivative f2') (atreal x within s)` ASSUME_TAC);
 (EXPAND_TAC "f2'" THEN REWRITE_TAC[ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 (SUBGOAL_THEN `(f1 has_real_derivative f1')(atreal x within s) /\ P (f1 x)` 
  MP_TAC);
  STRIP_TAC;
 (EXPAND_TAC "f1'" THEN EXPAND_TAC "f1");
 (REAL_DIFF_TAC THEN REAL_ARITH_TAC); 
 (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM] THEN EXPAND_TAC "f1");
 (MP_TAC (ASSUME `(x:real) IN s`) THEN ASM_REWRITE_TAC[]);

 (SUBGOAL_THEN `!x. P x ==> (sqrt has_real_derivative g2' x) (atreal x)`MP_TAC);
 (EXPAND_TAC "g2'" THEN REWRITE_TAC[BETA_THM]);
 (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);  
 (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);
 (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);

 (ABBREV_TAC `f3 = (\t. (&2 * &2 - (y1 + t) * (y1 + t) - (y2 - t) * (y2 - t)) / 
    sqrt (((y1 + t) + (y2 - t) + &2) * ((y1 + t) + (y2 - t) - &2) *
           ((y2 - t) + &2 - (y1 + t)) * (&2 + (y1 + t) - (y2 - t))))`);
 (ABBREV_TAC 
   `h = (\t. (&2 * &2 - (y1 + t) * (y1 + t) - (y2 - t) * (y2 - t)))`);

 (SUBGOAL_THEN `(f3 has_real_derivative 
                 ((&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2') / f2 x pow 2)
                 (atreal x within s)` ASSUME_TAC);

 (SUBGOAL_THEN `f3 = (\t:real. h t / f2 t)` ASSUME_TAC);
 (EXPAND_TAC "f2" THEN EXPAND_TAC "h" THEN EXPAND_TAC "f3");
 (ASM_REWRITE_TAC[]);
  
 (SUBGOAL_THEN 
 `(h has_real_derivative &2 * (y2 - y1 - &2 * x)) (atreal x within s) /\
  (f2 has_real_derivative f2') (atreal x within s) /\ ~(f2 x = &0)` MP_TAC);
 (ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC);
 (EXPAND_TAC "h" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SQRT_POS_LT);
 (EXPAND_TAC "f1" THEN MP_TAC(ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (PURE_REWRITE_TAC[ASSUME `f3 = (\t:real. h t / f2 t)`]);
 (REWRITE_TAC[HAS_REAL_DERIVATIVE_DIV_WITHIN]);

 (ABBREV_TAC `F1 = (\t. atn
                       ((&2 * &2 - (y1 + t) * (y1 + t) - (y2 - t) * (y2 - t)) / 
                      sqrt
                        (((y1 + t) + (y2 - t) + &2) *
                        ((y1 + t) + (y2 - t) - &2) *
                        ((y2 - t) + &2 - (y1 + t)) *
                        (&2 + (y1 + t) - (y2 - t)))))`);
 (SUBGOAL_THEN `F1 = (\t:real. atn (f3 t))` ASSUME_TAC);
 (EXPAND_TAC "f3" THEN EXPAND_TAC "F1" THEN ASM_REWRITE_TAC[]);

 (ABBREV_TAC 
  `f3' = ((&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2') / f2 x pow 2`);
 (SUBGOAL_THEN 
 `(F1 has_real_derivative f3' * inv (&1 + f3 x pow 2)) (atreal x within s)`
 ASSUME_TAC);
 (REWRITE_TAC[ASSUME `F1 = (\t:real. atn (f3 t))`]);
 (SUBGOAL_THEN `(f3 has_real_derivative f3') (atreal x within s) /\ 
                 (:real) (f3 x)` MP_TAC);
 (ASM_REWRITE_TAC[] THEN MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
 (ABBREV_TAC `h' = (\x. inv (&1 + x pow 2))`);

 (SUBGOAL_THEN `!x. (:real) x ==> (atn has_real_derivative (h':real->real) x)
  (atreal x)` MP_TAC);
 (EXPAND_TAC "h'" THEN REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);

 (SUBGOAL_THEN `inv (&1 + f3 (x:real) pow 2) = h' (f3 x)` ASSUME_TAC);
 (EXPAND_TAC "h'" THEN REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `inv (&1 + f3 (x:real) pow 2) = h'( f3 x)`]);

 (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);

(* --------------------------------------------------------------------------*)
(*                  REDUCE derivative of F1                                  *)  
(* --------------------------------------------------------------------------*)

 (SUBGOAL_THEN `f1 x = (y1 + y2 + &2) *
                        (y1 + y2 - &2) *
                        (y2 - &2 * x + &2 - y1) *
                        (&2 + y1 + &2 * x - y2)`ASSUME_TAC);
 (EXPAND_TAC "f1" THEN REAL_ARITH_TAC);
 (SUBGOAL_THEN `inv (&1 + f3 x pow 2) = 
                (f1 x) / (&4 * ((y1 + x) * (y2 - x)) pow 2)` ASSUME_TAC);
 (EXPAND_TAC "f3" THEN REWRITE_TAC[REAL_POW_DIV]);

 (SUBGOAL_THEN `&0 <= ((y1 + x) + y2 - x + &2) * ((y1 + x) + y2 - x - &2) *
  (y2 - x + &2 - (y1 + x)) * (&2 + (y1 + x) - (y2 - x))` ASSUME_TAC);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 (MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (SUBGOAL_THEN `sqrt (((y1 + x) + y2 - x + &2) * ((y1 + x) + y2 - x - &2) *
   (y2 - x + &2 - (y1 + x)) * (&2 + (y1 + x) - (y2 - x))) pow 2 = f1 x`
 ASSUME_TAC);
 (EXPAND_TAC "f1" THEN ASM_SIMP_TAC [SQRT_POW_2]);

 (PURE_ONCE_ASM_REWRITE_TAC[]);
 (ONCE_ASM_REWRITE_TAC[GSYM REAL_INV_DIV]);
 (AP_TERM_TAC);
 (ONCE_ASM_REWRITE_TAC[REAL_INV_DIV] THEN PURE_ONCE_ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (REAL_ARITH `&1 = x - y ==> &1 + y = x `));
 (REWRITE_TAC [REAL_ARITH `x / y - z / y = (x - z) / y`]);
 (REWRITE_TAC[REAL_ARITH `&4 * ((y1 + x) * (y2 - x)) pow 2 -
  (&2 * &2 - (y1 + x) * (y1 + x) - (y2 - x) * (y2 - x)) pow 2 = 
  (y1 + y2 + &2) * (y1 + y2 - &2) * (y2 - &2 * x + &2 - y1) *
  (&2 + y1 + &2 * x - y2)`]);
 (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
 (REWRITE_TAC[GSYM (ASSUME `f1 x = (y1 + y2 + &2) * (y1 + y2 - &2) *
      (y2 - &2 * x + &2 - y1) * (&2 + y1 + &2 * x - y2)`)]);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(&0 = a)`));
 (MP_TAC (ASSUME `x:real IN s`) THEN EXPAND_TAC "f1" THEN ASM_REWRITE_TAC[]);

(* ========================================================================== *)

 (SUBGOAL_THEN `(&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2' = 
  &4 * (y1 + x) * (y2 - x) * (y2 - y1 - &2 * x) * 
  ((y2 + y1) pow 2 - &4) / f2 x` ASSUME_TAC);
 (ABBREV_TAC `X = (&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2'`);
 (REWRITE_TAC[REAL_ARITH `x * y / z = (x * y) / z`]);
 (ABBREV_TAC `Y = &4 * (y1 + x) * (y2 - x) * (y2 - y1 - &2 * x) * 
                   ((y2 + y1) pow 2 - &4)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);

 (SUBGOAL_THEN `Y / f2 (x:real) = X <=> Y = X * f2 x` ASSUME_TAC);
 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 (REPLICATE_TAC 2 (ONCE_ASM_REWRITE_TAC[]) THEN MATCH_MP_TAC SQRT_POS_LT);
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (ONCE_ASM_REWRITE_TAC[]);
 (EXPAND_TAC "X" THEN EXPAND_TAC "Y");
 (EXPAND_TAC "f2'" THEN EXPAND_TAC "h" THEN EXPAND_TAC "g2'");
 (ONCE_REWRITE_TAC[REAL_ARITH `(a - b) * c = a * c - b * c`]);

 (SUBGOAL_THEN `inv (&2 * sqrt (f1 x)) * f2 (x:real) = &1 / &2` ASSUME_TAC);
 (REWRITE_TAC[ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 (ONCE_REWRITE_TAC[REAL_ARITH `a * sqrt b = (a * (&2 * sqrt b)) / &2`]);
 (AP_THM_TAC THEN AP_TERM_TAC);
 (MATCH_MP_TAC REAL_MUL_LINV);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 (MATCH_MP_TAC REAL_LT_MUL);
 (REWRITE_TAC[REAL_ARITH `&0 < &2`]);
 (MATCH_MP_TAC SQRT_POS_LT);
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b) * c * d`]);
 (PURE_REWRITE_TAC[ASSUME `inv (&2 * sqrt (f1 x)) * f2 (x:real) = &1 / &2`]);
 (REWRITE_TAC[REAL_ARITH `(a * f2 x) * f2 x = a * (f2 (x:real) pow 2)`]);

 (SUBGOAL_THEN `f2 (x:real) pow 2 = f1 x` ASSUME_TAC);
 (REWRITE_TAC [ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 (MATCH_MP_TAC SQRT_POW_2);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (REWRITE_TAC[ASSUME `f2 (x:real) pow 2 = f1 x`]);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "f1'" THEN REAL_ARITH_TAC);

 (SUBGOAL_THEN 
  `f3' * inv (&1 + f3 x pow 2) = 
   (y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4) / ((y1 + x) * (y2 - x) * f2 x)` ASSUME_TAC);
 (EXPAND_TAC "f3'");
 (REWRITE_TAC[ASSUME `inv (&1 + f3 x pow 2) = 
                       f1 x / (&4 * ((y1 + x) * (y2 - x)) pow 2)`]);
 (REWRITE_TAC[ASSUME 
 `(&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2' = &4 * (y1 + x) * (y2 - x) * 
  (y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4) / f2 x`]);

 (SUBGOAL_THEN `f2 (x:real) pow 2 = f1 x` ASSUME_TAC);
 (REWRITE_TAC [ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 (MATCH_MP_TAC SQRT_POW_2);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `f2 (x:real) pow 2 = f1 x`]);

 (ONCE_REWRITE_TAC [REAL_ARITH `a / b * c / d = (a / d) * c / b`]);
 (MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 /\ x = y ==> x * a = y`));
  STRIP_TAC;

 (MATCH_MP_TAC REAL_DIV_REFL);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

 (ABBREV_TAC `X = (&4 * (y1 + x) * (y2 - x) * (y2 - y1 - &2 * x) * 
                   ((y2 + y1) pow 2 - &4) / f2 x)`);
 (ABBREV_TAC `Y = (y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4) / 
                   ((y1 + x) * (y2 - x) * f2 x)`);
 (ABBREV_TAC `Z = (&4 * ((y1 + x) * (y2 - x)) pow 2)`);

 (SUBGOAL_THEN `X / Z = Y <=> X = Y * Z` ASSUME_TAC);
 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 (EXPAND_TAC "Z" THEN MATCH_MP_TAC REAL_LT_MUL);
 (REWRITE_TAC[REAL_ARITH `&0 < &4`] THEN MATCH_MP_TAC REAL_POW_LT);
 (MATCH_MP_TAC REAL_LT_MUL);
 (MP_TAC (ASSUME `x:real IN s`));
 (PURE_REWRITE_TAC[ASSUME 
  `s = {t |  y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1}`]);
 (REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);

 (MATCH_MP_TAC (REAL_ARITH `&0 <= y1 + &2 * x /\ &2 <= y1 ==> &0 < y1 + x`));
 (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC (REAL_ARITH `&2 * x < &2 * y ==> &0 < y - x`));
 (MATCH_MP_TAC (REAL_ARITH 
   `a < y2 + &2 - y1 /\ y2 + &2 - y1 <= b ==> a < b`));
 (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);

 (ONCE_ASM_REWRITE_TAC[]);
 (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
 (REWRITE_TAC [REAL_ARITH `a * b / c = (a * b) / c`]); 
 (REWRITE_TAC[REAL_ARITH `((y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4)) / 
  ((y1 + x) * (y2 - x) * f2 x) * &4 * ((y1 + x) * (y2 - x)) pow 2 =
  (&4 * (y1 + x) * (y2 - x) * (y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4)) *
  ((y1 + x) * (y2 - x)) / (f2 x * (y1 + x) * (y2 - x))`]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
 CONJ_TAC;
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 (MATCH_MP_TAC REAL_LT_MUL THEN MP_TAC (ASSUME `x:real IN s`));
 (PURE_REWRITE_TAC[ASSUME 
  `s = {t |  y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1}`]);
 (REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);

 (MATCH_MP_TAC (REAL_ARITH `&0 <= y1 + &2 * x /\ &2 <= y1 ==> &0 < y1 + x`));
 (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC (REAL_ARITH `&2 * x < &2 * y ==> &0 < y - x`));
 (MATCH_MP_TAC (REAL_ARITH 
   `a < y2 + &2 - y1 /\ y2 + &2 - y1 <= b ==> a < b`));
 (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);

 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 (ONCE_ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[]);
 (MATCH_MP_TAC SQRT_POS_LT);
 (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);

(* ========================================================================== *)

 (SUBGOAL_THEN 
  `(F1 has_real_derivative ((y2 - y1 - &2 * x) *
      ((y2 + y1) pow 2 - &4)) / ((y1 + x) * (y2 - x) * f2 x))
      (atreal x within s)` ASSUME_TAC);
 (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);
 (ASM_MESON_TAC[]);

 (SUBGOAL_THEN 
  `(F1 has_real_derivative g' x) (atreal x within s)` ASSUME_TAC);
 (REWRITE_TAC[ASSUME 
  `g' = (\x. ((y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4)) /
           ((y1 + x) * (y2 - x) *
            sqrt
            ((y1 + y2 + &2) *
             (y1 + y2 - &2) *
             (y2 - &2 * x + &2 - y1) *
             (&2 + y1 + &2 * x - y2))))`]);
 (FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]);

 (ABBREV_TAC `F2 = (\x:real. pi / &2 + F1 x)`);
 (ABBREV_TAC `pi_2 = (\x:real. pi / &2 )`);

 (SUBGOAL_THEN `(F2 has_real_derivative g' x)(atreal x within s)` MP_TAC);
 (SUBGOAL_THEN `F2 = (\x:real. pi_2 x + F1 x)` ASSUME_TAC);
 (EXPAND_TAC "F2" THEN EXPAND_TAC "F1" THEN EXPAND_TAC "pi_2");
 (REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `F2 = (\x:real. pi_2 x + F1 x)`]);
 (SUBGOAL_THEN `((\x. pi_2 x + F1 x) has_real_derivative &0 + g' x)
 (atreal x within s)` ASSUME_TAC);

 (SUBGOAL_THEN `(pi_2 has_real_derivative (&0)) (atreal x within s)` MP_TAC);
 (EXPAND_TAC "pi_2" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);

 (MP_TAC (ASSUME `(F1 has_real_derivative g' x) (atreal x within s)`));
 (REWRITE_TAC[MESON[] `(a ==> b ==> c) <=> (b /\ a ==> c)`]);
 (MESON_TAC[HAS_REAL_DERIVATIVE_ADD]);
 (ASM_MESON_TAC[REAL_ARITH `&0 + a = a`]);

 (SUBGOAL_THEN `(!x':real. (x':real) IN s /\ abs (x' - x) < &1 ==> 
                            (F2:real -> real) x' = g x')` MP_TAC);
 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]); 
 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN EXPAND_TAC "F2" THEN EXPAND_TAC "F1");
 (MATCH_MP_TAC ATN_UPS_X_BREAKDOWN1);
 (MP_TAC (ASSUME `x':real IN s`) THEN ASM_REWRITE_TAC[]);

 (MP_TAC (ASSUME `x:real IN s`));
 (MP_TAC (REAL_ARITH `&0 < &1`));
 (MESON_TAC[HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN])]);;
(* ========================================================================== *)
(*        SECOND LEMMA                                                        *)
(* ========================================================================== *)

let compute_two_second = 
prove_by_refinement (
 `!y1 y2 s hz g x.
     &1 <= hz /\ hz < &2 /\
     &2 <= y1 /\ y1 <= &2 * hz /\
     &2 <= y2 /\ y2 <= &2 * hz /\
     s = {t | y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1} /\
     g =
     (\t. ((y2 - y1 - &2 * t) * ((y2 + y1) pow 2 - &4)) /
          ((y1 + t) *
           (y2 - t) *
           sqrt
           ((y1 + y2 + &2) *
            (y1 + y2 - &2) *
            (y2 - &2 * t + &2 - y1) *
            (&2 + y1 + &2 * t - y2))))
     ==> (g has_real_derivative
          (sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
           (-- &4 * y1 pow 2 +
            y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
            &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
            y2 pow 4)) /
          (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2))
         (atreal (&0) within s)`,


[(REWRITE_TAC[REAL_ARITH `a * b * sqrt c = (a * b) * sqrt c`]);
 (REPEAT STRIP_TAC);

  (SUBGOAL_THEN `&0 IN s` ASSUME_TAC);
  (PURE_ASM_REWRITE_TAC[IN_ELIM_THM; REAL_MUL_RZERO]);
   ASM_REAL_ARITH_TAC;

(* ========================================================================== *)

  (SUBGOAL_THEN  `!t. t IN s ==>  &0 < (y1 + y2 + &2) * (y1 + y2 - &2) * 
                          (y2 - &2 * t + &2 - y1) * (&2 + y1 + &2 * t - y2)`
     ASSUME_TAC);

  (GEN_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);

    (SUBGOAL_THEN `&0 < y1 + y2 - &2 /\ &0 < y1 + y2 + &2 /\ 
       &0 < y2 - &2 * t + &2 - y1 /\ &0 < &2 + y1 + &2 * t - y2` ASSUME_TAC);
     ASM_REAL_ARITH_TAC;
    (ASM_MESON_TAC[REAL_LT_MUL]);

(* -------------------------------------------------------------------------- *)

(ABBREV_TAC `f1 = (\t. (y2 - y1 - &2 * t) * ((y2 + y1) pow 2 - &4))`);
(ABBREV_TAC `f2 = (\t. (y1 + y2 + &2) * (y1 + y2 - &2) *
             (y2 - &2 * t + &2 - y1) * (&2 + y1 + &2 * t - y2))`);
(ABBREV_TAC `f3 = (\t:real. sqrt (f2 t))`);
(ABBREV_TAC `f4 = (\t:real. (y1 + t) * (y2 - t))`);
(ABBREV_TAC `f5 = (\t:real. f4 t * f3 t )`);

(SUBGOAL_THEN `&0 < f2 (&0)` ASSUME_TAC);
(EXPAND_TAC "f2" THEN MP_TAC (ASSUME `((&0):real) IN s`));
(ASM_REWRITE_TAC[]);

(SUBGOAL_THEN `(f1 has_real_derivative -- &2 * ((y2 + y1) pow 2 - &4))
                 (atreal (&0) within s)` ASSUME_TAC);
(EXPAND_TAC "f1" THEN REAL_DIFF_TAC);
 REAL_ARITH_TAC;

(ABBREV_TAC `f2' = &4 * (y2 - y1) * ((y2 + y1) pow 2 - &4)`);
(ABBREV_TAC `P ={x| &0 < x}`);
(ABBREV_TAC `g3' = (\x. inv (&2 * sqrt x))`);
(ABBREV_TAC `f3' = f2' * g3' ((f2:real->real) (&0))`);

  (SUBGOAL_THEN 
    `(f3 has_real_derivative f3') (atreal (&0) within s)` ASSUME_TAC);
  (EXPAND_TAC "f3'" THEN EXPAND_TAC "f3");

  (SUBGOAL_THEN 
     `(f2 has_real_derivative f2') (atreal (&0) within s) /\ P (f2 (&0))` 
   MP_TAC);
   STRIP_TAC;

  (EXPAND_TAC "f2" THEN EXPAND_TAC "f2'");
  (REAL_DIFF_TAC THEN REWRITE_TAC[POW_2] THEN REAL_ARITH_TAC);
  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `!x. P x ==> (sqrt has_real_derivative (g3':real->real) x) (atreal x)`
     MP_TAC);
  (EXPAND_TAC "g3'" THEN REWRITE_TAC[BETA_THM]);
  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);  
  (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);

(REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);

(* ========================================================================== *)

(SUBGOAL_THEN `(f5 has_real_derivative f4 (&0) * f3' + (y2 - y1) * f3 (&0)) 
  (atreal (&0) within s)` ASSUME_TAC);
(EXPAND_TAC "f5");

(SUBGOAL_THEN 
  `(f4 has_real_derivative y2 - y1) (atreal (&0) within s) /\
   (f3 has_real_derivative f3') (atreal (&0) within s)` MP_TAC);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "f4" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);

(REWRITE_TAC[HAS_REAL_DERIVATIVE_MUL_WITHIN]);

(* ========================================================================= *)
(*          Derivative of f1 / f5                                            *) 
(* ========================================================================= *)

(SUBGOAL_THEN `g = (\t:real. f1 t / f5 t)` ASSUME_TAC);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "f5" THEN EXPAND_TAC "f1");
(EXPAND_TAC "f4" THEN EXPAND_TAC "f3" THEN EXPAND_TAC "f2");
(REWRITE_TAC[]);

(REWRITE_TAC[ASSUME `g = (\t:real. f1 t / f5 t)`] THEN DEL_TAC);

(SUBGOAL_THEN `((\t. f1 t / f5 t) has_real_derivative
  ((-- &2 * ((y2 + y1) pow 2 - &4)) * f5 (&0) - f1 (&0) * 
  (f4 (&0) * f3' + (y2 - y1) * f3 (&0))) / 
  f5 (&0) pow 2) (atreal (&0) within s)` ASSUME_TAC);

(SUBGOAL_THEN 
  `(f1 has_real_derivative -- &2 * ((y2 + y1) pow 2 - &4)) 
   (atreal (&0) within s) /\
   (f5 has_real_derivative f4 (&0) * f3' + (y2 - y1) * f3 (&0))
    (atreal (&0) within s) /\ ~(f5 (&0) = &0)` MP_TAC);

(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
(EXPAND_TAC "f5" THEN MATCH_MP_TAC REAL_LT_MUL);
 STRIP_TAC;

(EXPAND_TAC "f4" THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REAL_ARITH_TAC);
(EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);

(REWRITE_TAC[HAS_REAL_DERIVATIVE_DIV_WITHIN]);

(* ========================================================================= *)

(SUBGOAL_THEN 
`((-- &2 * ((y2 + y1) pow 2 - &4)) * f5 (&0) -
  f1 (&0) * (f4 (&0) * f3' + (y2 - y1) * f3 (&0))) /
 f5 (&0) pow 2 =
 (sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
  (-- &4 * y1 pow 2 +
   y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
   &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
   y2 pow 4)) /
 (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2)` ASSUME_TAC);

(REWRITE_WITH `ups_x (y1 pow 2) (y2 pow 2) (&4) = f2 (&0)`);
(REWRITE_TAC[ups_x] THEN EXPAND_TAC "f2");
 REAL_ARITH_TAC;

(EXPAND_TAC "f5");

(SUBGOAL_THEN `f4 (&0) = y1 * y2` ASSUME_TAC);
(EXPAND_TAC "f4" THEN REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);


(REWRITE_TAC[REAL_ARITH `a - b * (c + d) = a - b * c - b * d`]);
(REWRITE_TAC[REAL_ARITH `(-- &2 * m) * n * x = ((-- &2 * m) * n) * x`]);
(REWRITE_TAC[REAL_ARITH `f1 (&0) * (y2 - y1) * f3 (&0) = 
                          (f1 (&0) * (y2 - y1)) * f3 (&0)`]);
(REWRITE_TAC[REAL_ARITH `a * f3 (&0) - b - c * f3 (&0) = (a - c) * f3 (&0) - b`]);
(SUBGOAL_THEN 
  `((-- &2 * ((y2 + y1) pow 2 - &4)) * y1) * y2 - f1 (&0) * (y2 - y1) = 
    -- (y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)` ASSUME_TAC);   
(EXPAND_TAC "f1" THEN REAL_ARITH_TAC);

(ASM_REWRITE_TAC[]);
(EXPAND_TAC "f3'" THEN EXPAND_TAC "g3'");

(SUBGOAL_THEN `sqrt (f2 (&0)) = f3 (&0)` ASSUME_TAC);
(EXPAND_TAC "f3" THEN REWRITE_TAC[]);
(REWRITE_TAC[ASSUME `sqrt (f2 (&0)) = f3 (&0)`]);

(SUBGOAL_THEN 
`(--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) * f3 (&0) -
  f1 (&0) * (y1 * y2) * f2' * inv (&2 * f3 (&0)) =
 ((--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) * f3 (&0) pow 2 -
  f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) /
 f3 (&0)` ASSUME_TAC);

(PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a - b) / c = a / c - b / c`]);
(MATCH_MP_TAC (REAL_ARITH `a = b /\ c = d ==> a - c = b - d`));
 STRIP_TAC;

(REWRITE_TAC[REAL_POW_2; REAL_ARITH `(a * b * c) / d = (a * b) * c / d`]);
(MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 ==> b = b * a`));
(MATCH_MP_TAC REAL_DIV_REFL);
(EXPAND_TAC "f3");
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
(MATCH_MP_TAC SQRT_POS_LT);
(ASM_REWRITE_TAC[]);

(EXPAND_TAC "f2'");
(REWRITE_TAC[REAL_ARITH 
 `f1 (&0) * (y1 * y2) * (&4 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) *
  inv (&2 * f3 (&0)) = 
  f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4) * &2 * 
  inv (&2 * f3 (&0))`]) ;
(ABBREV_TAC 
  `X =  f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4) * &2 * 
  inv (&2 * f3 (&0))`);
(ABBREV_TAC 
 `Y = f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)`);
(ABBREV_TAC `Z = (f3:real->real) (&0)`);

(SUBGOAL_THEN `X = Y / Z <=> X * Z = Y` ASSUME_TAC);
(MATCH_MP_TAC REAL_EQ_RDIV_EQ THEN EXPAND_TAC "Z" THEN EXPAND_TAC "f3");
(MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);

(EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
(REWRITE_TAC[REAL_ARITH `(x1 * x2 * x3 * x4 * x5 * &2 * b) * c  =
                           (x1 * x2 * x3 * x4 * x5) * (&2 * c) * b`]);
(MATCH_MP_TAC( MESON[REAL_MUL_RID] `a = &1 ==> b * a = b`));
(MATCH_MP_TAC REAL_MUL_RINV);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
(MATCH_MP_TAC REAL_LT_MUL);
(REWRITE_TAC[REAL_ARITH `&0 < &2`]);
(EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);

(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_POW_MUL]);
(EXPAND_TAC "f3");
(REWRITE_WITH `sqrt (f2 (&0)) pow 2 = f2 (&0)`);
(MATCH_MP_TAC SQRT_POW_2);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[]);

(REWRITE_TAC[REAL_ARITH `a / b / c = a / c / b`]);
(ABBREV_TAC `A = ((--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) * 
   f2 (&0) - f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) /
  ((y1 pow 2 * y2 pow 2) * f2 (&0))`);
(ABBREV_TAC `B = (sqrt (f2 (&0)) * (-- &4 * y1 pow 2 +
   y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
   &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
   y2 pow 4)) /
   (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2)`);

(SUBGOAL_THEN `A/ sqrt (f2 (&0)) = B <=> A = B * sqrt (f2 (&0))` ASSUME_TAC);
(MATCH_MP_TAC REAL_EQ_LDIV_EQ);
(MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
(ONCE_ASM_REWRITE_TAC[]);
(EXPAND_TAC "A" THEN EXPAND_TAC "B");
(REWRITE_TAC[REAL_ARITH `(a * b) / c * d = (b * a * d) / c`]);
(ONCE_REWRITE_TAC[GSYM REAL_POW_2]);
(REWRITE_WITH `sqrt (f2 (&0)) pow 2 = f2 (&0)`);
(MATCH_MP_TAC SQRT_POW_2);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[]);


(ABBREV_TAC `C = ((--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) * 
   f2 (&0) - f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) /
  ((y1 pow 2 * y2 pow 2) * f2 (&0))`);
(ABBREV_TAC `D = ((-- &4 * y1 pow 2 +
   y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
   &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
   y2 pow 4) *
  f2 (&0))`);
(ABBREV_TAC `E = (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2)`);


(SUBGOAL_THEN `C = D / E <=> C * E = D` ASSUME_TAC);
(MATCH_MP_TAC REAL_EQ_RDIV_EQ);
(EXPAND_TAC "E");
(MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC);
(MATCH_MP_TAC REAL_POW_LT);
(ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 < a`]);
(MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC);
(MATCH_MP_TAC REAL_POW_LT);
(ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 < a`]);
(MATCH_MP_TAC REAL_POW_LT);
(MATCH_MP_TAC (REAL_ARITH `b < a ==> &0 < a - b`));
(SUBGOAL_THEN ` -- &2 < y1 - y2 /\ y1 - y2 < &2` ASSUME_TAC);
(ASM_REAL_ARITH_TAC);
(REWRITE_TAC[REAL_ARITH `&4 = (&2) pow 2`]);
(REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);
(ASM_REAL_ARITH_TAC);

(ONCE_ASM_REWRITE_TAC[]); 
(EXPAND_TAC "C" THEN EXPAND_TAC "D" THEN EXPAND_TAC "E");
(REWRITE_TAC[REAL_ARITH `a / b * c = (a * c) / b`]);

(REWRITE_WITH `(((--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) * f2 (&0) -
   f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) *
  y1 pow 2 *
  y2 pow 2 *
  (&4 - (y1 - y2) pow 2) pow 2) = ((-- &4 * y1 pow 2 +
  y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
  &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
  y2 pow 4) *
 f2 (&0)) * ((y1 pow 2 * y2 pow 2) * f2 (&0))`);

(EXPAND_TAC "f2" THEN EXPAND_TAC "f1");
(REAL_ARITH_TAC);

(ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);
(MATCH_MP_TAC (MESON [REAL_MUL_RID] `a = &1 ==> b * a = b`));
(MATCH_MP_TAC REAL_DIV_REFL);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a =  &0)`));


(MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC);
(MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC);
(MATCH_MP_TAC REAL_POW_LT);
(ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 < a`]);
(MATCH_MP_TAC REAL_POW_LT);
(ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 < a`]);
(ASM_REWRITE_TAC[]);

(ASM_MESON_TAC[])]);;
(* ========================================================================= *)

let COMPUTE_DERIVATIVE_TWO = 
prove_by_refinement (
 `!y1 y2 s hz g x f.
     &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
     &2 <= y2 /\ y2 <= &2 * hz /\
   s = {t |  y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1} /\
   g = (\t. arclength (y1 + t) (y2 - t) (&2)) /\ x IN s /\
   g' =
     (\t. ((y2 - y1 - &2 * t) * ((y2 + y1) pow 2 - &4)) /
          ((y1 + t) *
           (y2 - t) *
           sqrt
           ((y1 + y2 + &2) *
            (y1 + y2 - &2) *
            (y2 - &2 * t + &2 - y1) *
            (&2 + y1 + &2 * t - y2))))
==>  (!x. x IN s ==> (g has_real_derivative g' x) (atreal x within s)) /\
     (g' has_real_derivative
          (sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
           (-- &4 * y1 pow 2 +
            y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
            &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
            y2 pow 4)) /
          (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2))
         (atreal (&0) within s)`,


[(REPEAT STRIP_TAC);
 (ASM_MESON_TAC[compute_two_first]);
 (ASM_MESON_TAC[compute_two_second])]);;

end;;