(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*          COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA                       *)
(*                                                                           *)
(*                  LEMMA ABOUT DERIVATIVES                                  *)
(*                                                                           *)
(*      Authour : VU KHAC KY                                                 *)
(*                                                                           *)
(* ========================================================================= *)

flyspeck_needs "trigonometry/euler_complement.hl";;

module Euler_multivariate = struct 

open Sphere;;
open Trigonometry1;;
open Trigonometry2;;
open Prove_by_refinement;;
open Delta_x;;
open Euler_complement;;

(* ========================================================================= *)
(*                                                                           *)
(*                    SOME NECESSARY LEMMAS                                  *)
(*                                                                           *)
(* ========================================================================= *)

(* ========================================================================= *)
(*         LEMMA 1                                                           *)
(* ========================================================================= *)

let REDUCE_WITH_DIV_Euler_lemma = 
prove_by_refinement 
 (`!x y z . ~ (y = &0) /\ ~ (z = &0) ==> x * y / (z * y) = x / z`,

[ (REPEAT STRIP_TAC);
 (MATCH_MP_TAC REAL_EQ_LCANCEL_IMP);
 (EXISTS_TAC `z:real`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[REAL_ARITH `a * b * c = (a * c) * b`]);

  (SUBGOAL_THEN `z * x / z = x` ASSUME_TAC);
  (MATCH_MP_TAC REAL_DIV_LMUL);
  (ASM_REWRITE_TAC[]);

 (PURE_ONCE_ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (MESON[REAL_MUL_LID] `a = &1 ==> a * b = b`));
 (REWRITE_TAC[REAL_ARITH `a * b / c = (a * b) / c`]);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
 (ASM_REWRITE_TAC[])]);;

(* ========================================================================= *)
(*         LEMMAS MODIFIED FROM j.HARRISON FILES                             *)
(* ========================================================================= *)

let HAS_REAL_DERIVATIVE_ZERO_CONSTANT2 = 
prove (

`!f a b c s.
         is_realinterval s /\ (a IN s) /\
         (!x. x IN s ==> (f has_real_derivative &0) (atreal x within s))  /\
         (f a = c )
         ==> (!x. x IN s ==> f x = c)`,

  MP_TAC HAS_REAL_DERIVATIVE_ZERO_CONSTANT THEN 
  MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)

let HAS_REAL_DERIVATIVE_CHAIN2 = 
prove
  (`!P f g x s.
      (!x. P x ==> (g has_real_derivative g' x) (atreal x))
      ==> ((f has_real_derivative f') (atreal x within s) /\ P (f x))
               ==> ((\x. g (f x)) has_real_derivative f' * g' (f x))
                   (atreal x within s) `,

   REPEAT GEN_TAC THEN 
   MP_TAC HAS_REAL_DERIVATIVE_CHAIN THEN
   MESON_TAC[]);;
(* ========================================================================= *)
(*         LEMMAS ABOUT INTERVALS                                            *)
(* ========================================================================= *)


let INTERVAL_DIVIDE_Euler_lemma = 
prove_by_refinement 
 (`!c. &0 < (&4 - c) * c ==> &0 < c /\ c < &4`,

[(REPEAT STRIP_TAC);

  (MATCH_MP_TAC (REAL_ARITH `~(&0 <= -- x) ==> &0 < x`));
  STRIP_TAC;
    (SUBGOAL_THEN `(&4 - c) * (-- c) < &0` ASSUME_TAC);
    ASM_REAL_ARITH_TAC;
    (SUBGOAL_THEN `&0 <= (&4 - c) * (-- c)` ASSUME_TAC);
    (MATCH_MP_TAC REAL_LE_MUL);
    (ASM_REWRITE_TAC[]);
    ASM_REAL_ARITH_TAC;
  ASM_REAL_ARITH_TAC;

  (MATCH_MP_TAC (REAL_ARITH `~(&0 <= x - &4) ==> x < &4`));
  STRIP_TAC;
    (SUBGOAL_THEN `(c - &4) * c < &0` ASSUME_TAC);
    ASM_REAL_ARITH_TAC;
    (SUBGOAL_THEN `&0 <= (c - &4) * c` ASSUME_TAC);
    (MATCH_MP_TAC REAL_LE_MUL);
    (ASM_REWRITE_TAC[]);
    ASM_REAL_ARITH_TAC;
  ASM_REAL_ARITH_TAC]);;
(* ---------------------------------------------------------------------------*)

let SQRT_RULE_Euler_lemma = 
prove 
 (`!x y. x pow 2 = y /\ &0 <= x ==> x = sqrt y`,

 REPEAT STRIP_TAC THEN 
 REWRITE_TAC[GSYM (ASSUME `x pow 2 = y`);REAL_POW_2] THEN   
 ASM_SIMP_TAC[SQRT_MUL] THEN
 ASM_MESON_TAC[GSYM REAL_POW_2;SQRT_POW_2]);;

let REAL_INTERVAL_Euler_lemma = 
prove
( `!a b.  let P1 = {x| x < a} in 
          let P2 = {x| a < x} in
          let P3 = {x| a < x /\ x < b} in
        is_realinterval P1 /\ is_realinterval P2 /\ is_realinterval P3`,

 REPEAT GEN_TAC THEN
 REPEAT LET_TAC THEN 
 EXPAND_TAC "P1" THEN EXPAND_TAC "P2" THEN EXPAND_TAC "P3" THEN
 REWRITE_TAC[is_realinterval] THEN 
 REWRITE_TAC[IN_ELIM_THM] THEN REAL_ARITH_TAC);;
(* ========================================================================= *)
(*         FIRST LEMMA ABOUT DERIVATIVE                                      *)
(* ========================================================================= *)

  
let DERIVATIVE_WRT_C1_Euler_lemma = 
prove_by_refinement (

 `!P. is_realinterval P /\ (&2) IN P /\
   (!x. x IN P ==> ~ (x = &0) /\ ~ (&4 - x = &0)) ==>
   (!c. c IN P ==> --pi / &2 - &2 * atn (&1 - c / &2) + 
                  &2 * atn ((&4 - c) / c) = &0) `,


[ (GEN_TAC THEN STRIP_TAC);
 (MATCH_MP_TAC HAS_REAL_DERIVATIVE_ZERO_CONSTANT2 THEN EXISTS_TAC `&2`);
 (ASM_REWRITE_TAC[]); 
 (REWRITE_TAC[REAL_ARITH `&1 - &2 / &2 = &0`;ATN_0]);
 (REWRITE_TAC[REAL_ARITH 
   `(--a / &2 - &2 * &0 + &2 * s = &0) <=> s = a / &4`]);
 (REWRITE_TAC[REAL_ARITH `(&4 - &2) / &2 = &1`;ATN_1]);
 (GEN_TAC THEN STRIP_TAC);

   (SUBGOAL_THEN `~(c = &0) /\ ~(&4 - c = &0)` ASSUME_TAC);
    (* Subgoal 1 *)
   (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
   (UP_ASM_TAC THEN STRIP_TAC);

 (ABBREV_TAC 
  `f = (\c. --pi / &2 - &2 * atn (&1 - c / &2) + &2 * atn ((&4 - c) / c))`);
 (ABBREV_TAC `F1 = (\c. atn (&1 - c / &2))`);
 (ABBREV_TAC `F2 = (\c. atn ((&4 - c) / c))`);

   (SUBGOAL_THEN 
    `f = (\c:real. --pi / &2 - &2 * F1 c + &2 * F2 c)` ASSUME_TAC);
    (* Subgoal 2 *)
   (EXPAND_TAC "f" THEN EXPAND_TAC "F1" THEN EXPAND_TAC "F2");
   (MESON_TAC[]);

 (ASM_REWRITE_TAC[] THEN DEL_TAC);
 (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);

   (SUBGOAL_THEN 
    `!c. (:real) c ==> (atn has_real_derivative (g':real->real) c) (atreal c)`
     ASSUME_TAC);  
    (* Subgoal 3 *) 
   (EXPAND_TAC "g'");
   (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);

(* ------------------------------------------------------------------------- *)
(*    Compute the derivative of F1                                           *)
(* ------------------------------------------------------------------------- *)

 (ABBREV_TAC `f1 = (\c. &1 - c / &2)`);

   (SUBGOAL_THEN `F1 = (\c:real.  atn (f1 c))` ASSUME_TAC);
    (* Subgoal 4 *)
   (EXPAND_TAC "F1" THEN EXPAND_TAC "f1" THEN MESON_TAC[]);

   (SUBGOAL_THEN 
    `(F1 has_real_derivative (-- &1 / &2) * g' ((f1:real -> real) c)) 
     (atreal c within P)` ASSUME_TAC);
    (* Subgoal 5 *)
   (ONCE_ASM_REWRITE_TAC[]);

     (SUBGOAL_THEN 
      `(f1 has_real_derivative -- &1 / &2) (atreal c within P) /\ 
       (:real) (f1 c)` ASSUME_TAC);
      (* Subgoal 5.1 *)
     CONJ_TAC;  (* break into 2 subgoal 5.1.1 & 5.1.2 *)
       (EXPAND_TAC "f1" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC); (*End 5.1.1*) 
       (MESON_TAC[EQ_UNIV;IN_UNIV; IN]); (* End 5.1.2 *)
       (* End subgoal 5.1 *)

   (UP_ASM_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC);
   (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
   (MESON_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
    (* End subgoal 5 *)

   (SUBGOAL_THEN 
    `-- &1 / &2 / (&2 - c + c * c / &4) = -- &1 / &2 * g' ((f1:real -> real) c)`
     ASSUME_TAC);
    (* Subgoal 6 *)
   (EXPAND_TAC "g'" THEN EXPAND_TAC "f1");
   (REWRITE_TAC[REAL_ARITH 
    `&1 + (&1 - c / &2) pow 2 = &2 - c + c * c / &4`]);
   (ABBREV_TAC `m = -- &1 / &2`);
   (ABBREV_TAC `n = (&2 - c + c * c / &4)`);
      
     (SUBGOAL_THEN `m = (m * inv n) * n  ==> (m / n = m * inv n)` ASSUME_TAC);
     (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (b ==> a)`));
     (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
     (EXPAND_TAC "n"); 
     (REWRITE_TAC[REAL_ARITH 
     `&2 - c + c * c / &4 = &1 + (&1 - c / &2) pow 2 `]);
     (MATCH_MP_TAC (REAL_ARITH `&0 <= a ==> &0 < &1 + a`));
     (REWRITE_TAC[REAL_LE_POW_2]);

   (FIRST_X_ASSUM MATCH_MP_TAC);
   (REWRITE_TAC[GSYM REAL_MUL_ASSOC]);
   (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> a = a * x`)); 
   (MATCH_MP_TAC REAL_MUL_LINV);
   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
   (EXPAND_TAC "n"); 
   (REWRITE_TAC[REAL_ARITH 
    `&2 - c + c * c / &4 = &1 + (&1 - c / &2) pow 2 `]);
   (MATCH_MP_TAC (REAL_ARITH `&0 <= a ==> &0 < &1 + a`));
   (REWRITE_TAC[REAL_LE_POW_2]);

   (SUBGOAL_THEN 
    `(F1 has_real_derivative -- &1 / &2 / (&2 - c + c * c / &4)) 
     (atreal c within P)` ASSUME_TAC);
    (* Subgoal 7 *)
   (ASM_MESON_TAC[]);
  
 (UP_ASM_TAC THEN REPLICATE_TAC 4 DEL_TAC THEN REPEAT DISCH_TAC);
 SWITCH_TAC;

(* ------------------------------------------------------------------------- *)
(*    Compute the derivative of F2                                           *)
(* ------------------------------------------------------------------------- *)

 (ABBREV_TAC `f2 = (\c. (&4 - c) / c)`);

   (SUBGOAL_THEN `F2 = (\c:real.  atn (f2 c))` ASSUME_TAC);
    (* Subgoal 8 *)
   (EXPAND_TAC "F2" THEN EXPAND_TAC "f2" THEN MESON_TAC[]);

   (SUBGOAL_THEN 
    `(F2 has_real_derivative (-- &4 / (c * c)) * g' ((f2:real -> real) c)) 
     (atreal c within P)` ASSUME_TAC);
    (* Subgoal 9 *)
   (ONCE_ASM_REWRITE_TAC[]);

     (SUBGOAL_THEN 
      `(f2 has_real_derivative (-- &4 / (c * c))) (atreal c within P) /\ 
       (:real) (f2 c)` ASSUME_TAC);
      (* Subgoal 9.1 *)
     CONJ_TAC;  (* Break into 2 subgoals *)
  
       (EXPAND_TAC "f2" THEN REAL_DIFF_TAC);
       (ASM_REWRITE_TAC[]);   
       (REWRITE_TAC[REAL_POW_2]);   
       (AP_THM_TAC THEN AP_TERM_TAC);
       REAL_ARITH_TAC;
       (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);

   (UP_ASM_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC);
   (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
   (MESON_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);

   (SUBGOAL_THEN 
    `-- &1 / &2 / (&2 - c + c * c / &4) =
     -- &4 / (c * c) * g' ((f2:real -> real) c)` ASSUME_TAC);
    (* Subgoal 10 *)
   (EXPAND_TAC "g'" THEN EXPAND_TAC "f2");
   (REWRITE_TAC[REAL_POW_DIV]);

     (SUBGOAL_THEN
      `&1 + (&4 - c) pow 2 / c pow 2 = (&16 - &8 * c + &2 * c * c) / (c * c)`
      ASSUME_TAC);
     (REWRITE_TAC[REAL_ARITH 
      `(&16 - &8 * c + &2 * c * c) = c * c + (&4 - c) pow 2`]);
     (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
     (REWRITE_TAC[REAL_POW_2]);
     (AP_THM_TAC THEN AP_TERM_TAC);   
     (REWRITE_TAC[EQ_SYM_EQ]);
     (MATCH_MP_TAC (REAL_DIV_REFL));
     (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(x \/ y) <=> ~ x /\ ~ y`]);
     (ASM_REWRITE_TAC[]);

   (ASM_REWRITE_TAC[]);
   (REWRITE_TAC[REAL_INV_DIV]);
   (REWRITE_TAC[REAL_ARITH `t / x * y / z = (y / x) * (t / z)`]);
  
     (SUBGOAL_THEN `(c * c) / (c * c) = &1` ASSUME_TAC);
     (MATCH_MP_TAC (REAL_DIV_REFL));
     (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(x \/ y) <=> ~ x /\ ~ y`]);
     (ASM_REWRITE_TAC[]);

   (ASM_REWRITE_TAC[REAL_MUL_LID]);
   (REWRITE_TAC[REAL_ARITH 
    `&16 - &8 * c + &2 * c * c = (&2 - c + c * c / &4) * &8`]);
   (REWRITE_TAC[REAL_ARITH `-- &4 = (-- &1 / &2) * &8`]);
   (REWRITE_TAC[EQ_SYM_EQ]);

   (ABBREV_TAC `m = -- &1 / &2`);
   (ABBREV_TAC `n = (&2 - c + c * c / &4)`);
   (REWRITE_TAC[REAL_ARITH `(a * b) / c = a * (b / c)`]);
   (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
   (REWRITE_TAC[REAL_ARITH `~ (&8 = &0)`]);
   (EXPAND_TAC "n");
   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
   (REWRITE_TAC[REAL_ARITH 
     `&2 - c + c * c / &4 = &1 + (&1 - c / &2) pow 2 `]);
   (MATCH_MP_TAC (REAL_ARITH `&0 <= a ==> &0 < &1 + a`));
   (REWRITE_TAC[REAL_LE_POW_2]);

   (SUBGOAL_THEN 
    `(F2 has_real_derivative
     -- &1 / &2 / (&2 - c + c * c / &4))(atreal c within P)` ASSUME_TAC);
    (* Subgoal 11 *)    
   (ASM_MESON_TAC[]);

 (UP_ASM_TAC THEN REPLICATE_TAC 5 DEL_TAC THEN DISCH_TAC);

(* ------------------------------------------------------------------------- *)
(*    Compute the derivative of f                                            *)
(* ------------------------------------------------------------------------- *)

 (ABBREV_TAC `f' = -- &1 / &2 / (&2 - c + c * c / &4)`);
 (ABBREV_TAC `F3 = (\c:real. F1 c - F2 c)`);

   (SUBGOAL_THEN 
    `(F3 has_real_derivative &0) (atreal c within P)` ASSUME_TAC);
   (EXPAND_TAC "F3");
   (ASM_MESON_TAC[HAS_REAL_DERIVATIVE_SUB; REAL_ARITH `a - a = &0`]);

 (ABBREV_TAC `2F3 = (\c:real. &2 * F3 c)`);

   (SUBGOAL_THEN 
    `(2F3 has_real_derivative (&2) * (&0)) (atreal c within P)` ASSUME_TAC);
   (EXPAND_TAC "2F3");
   (DEL_TAC THEN UP_ASM_TAC);
   (MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN);
   (MESON_TAC[]);

   (SUBGOAL_THEN 
   `(\c:real. --pi / &2 - &2 * F1 c + &2 * F2 c) = (\c:real. --pi / &2 - 2F3 c)`
    ASSUME_TAC);
   (EXPAND_TAC "2F3");
   (EXPAND_TAC "F3");
   (REWRITE_TAC[REAL_ARITH `a - &2 * (x - y) = a - &2 * x + &2 * y`]);

 (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);

   (SUBGOAL_THEN `((\c. --pi / &2) has_real_derivative &0)
                   (atreal c within P)` ASSUME_TAC);
   (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
  
 (UP_ASM_TAC THEN UP_ASM_TAC);
 (MP_TAC HAS_REAL_DERIVATIVE_SUB);
 (MESON_TAC [REAL_ARITH `&2 * &0 = &0 /\ &0 - &0 = &0`;   
   HAS_REAL_DERIVATIVE_SUB])]);;




let DERIVATIVE_WRT_A_Euler_lemma = 
prove_by_refinement (
 `! a b c.
  let d = ups_x a b c - a * b * c in 
 ((&0 < d) /\ (&0 < a /\ &0 < b /\ &0 < c) /\ 
              (a < &4 /\ b < &4 /\ c < &4) ==>
 pi / &2 - atn ((-- &2 * a + &2 * b + &2 * c - b * c) / (&2 * sqrt d)) +
 pi / &2 - atn ((-- &2 * b + &2 * c + &2 * a - c * a) / (&2 * sqrt d)) +
 pi / &2 - atn ((-- &2 * c + &2 * a + &2 * b - a * b) / (&2 * sqrt d)) - pi =
 pi - &2 * atn ((&8 - a - b - c) / sqrt d))`,


[ (REPEAT GEN_TAC THEN LET_TAC THEN STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH ` pi / &2 - x + pi / &2 - y + pi / &2 - z - pi = 
   pi - t <=> -- pi / &2 - x - y - z + t = &0`]);

 (ABBREV_TAC `s = {(x:real) | &0 < ups_x x b c - x * b * c }`);


(* ========================================================================= *)
(*                             The main subgoal.                             *) 
(* ========================================================================= *)

 (SUBGOAL_THEN `!a. (a IN s) ==> --pi / &2 -
 atn
  ((-- &2 * a + &2 * b + &2 * c - b * c) /
  (&2 * sqrt (ups_x a b c - a * b * c))) -
 atn
 ((-- &2 * b + &2 * c + &2 * a - c * a) /
  (&2 * sqrt (ups_x a b c - a * b * c))) -
 atn
 ((-- &2 * c + &2 * a + &2 * b - a * b) /
  (&2 * sqrt (ups_x a b c - a * b * c))) +
 &2 * atn ((&8 - a - b - c) / sqrt (ups_x a b c - a * b * c)) =
 &0` ASSUME_TAC);

 (MATCH_MP_TAC HAS_REAL_DERIVATIVE_ZERO_CONSTANT2 THEN EXISTS_TAC 
  `b + c - (b * c) / & 2`);
 (REPEAT CONJ_TAC);   (* Break into 3 Subgoals *) 

  (EXPAND_TAC "s");
  (ASM_MESON_TAC[EULER_TRIANGLE_REAL_INTERVAL]);  (* End subgoal 1 *)

(* ------------------------------------------------------------------------- *)
(*                b + c - (b * c) / &2 IN s                                  *)
(* ------------------------------------------------------------------------- *)
                  
  (EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM]);
  (ABBREV_TAC `a' = b + c - (b * c) / &2`);
  (MATCH_MP_TAC (REAL_ARITH `&0 < d /\ d <= x ==> &0 < x`));
  (ASM_REWRITE_TAC[]);
  (EXPAND_TAC "d" THEN REWRITE_TAC[ups_x]);
  (ONCE_REWRITE_TAC [REAL_ARITH `a <= b <=> &0 <= b - a `]);

    (SUBGOAL_THEN 
      `(--a' * a' - b * b - c * c + &2 * a' * c + &2 * a' * b + &2 * b * c) -
       a' * b * c -
       ((--a * a - b * b - c * c + &2 * a * c + &2 * a * b + &2 * b * c) -
       a * b * c) =
       (a - a') pow 2`
      ASSUME_TAC);
    (EXPAND_TAC "a'" THEN REAL_ARITH_TAC);

  (ASM_REWRITE_TAC[]);
  (ASM_MESON_TAC[REAL_LE_POW_2]);

(* ========================================================================= *)
(*                                                                           *)
(*                 BEGIN COMPUTE DERIVATIVES                                 *)
(*                                                                           *)
(* ========================================================================= *)
 (GEN_TAC THEN DISCH_TAC); 
 (ABBREV_TAC `Da = (-- &2 * a' + &2 * b + &2 * c - b * c)`); 
 (ABBREV_TAC `Db = (-- &2 * b + &2 * c + &2 * a' - a' * c)`); 
 (ABBREV_TAC `Dc = (-- &2 * c + &2 * a' + &2 * b - a' * b)`); 
 (ABBREV_TAC `D' = ups_x a' b c - a' * b * c`);

  (SUBGOAL_THEN `&0 < D'` ASSUME_TAC);
  (* Subgoal 3.1 *)

  (REPLICATE_TAC 5 UP_ASM_TAC THEN EXPAND_TAC "s");
  (PURE_ASM_REWRITE_TAC[IN_ELIM_THM] THEN MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*  Subgoal 3.2                                                              *)
(*         Derivative of sqrt (ups_x x b c - x * b * c)                      *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `G = (\x.  sqrt (ups_x x b c - x * b * c))`); 
 (ABBREV_TAC `G' = (-- &2 * a' + &2 * b + &2 * c - b * c) * 
                    inv (&2 * sqrt (ups_x a' b c - a' * b * c))`); 
 (SUBGOAL_THEN ` (G has_real_derivative G') (atreal a' within s)` ASSUME_TAC); 
 (ABBREV_TAC `f = (\x. ups_x x b c - x * b * c)`);
  
  (SUBGOAL_THEN `G = (\x:real. sqrt (f x))` ASSUME_TAC);
    (* Subgoal 3.2.1 *)
  (EXPAND_TAC "f" THEN ASM_REWRITE_TAC[]);
 
 (ABBREV_TAC `g' = (\x. inv (&2 * sqrt x))`); 
 (ABBREV_TAC `f' = -- &2 * a' + &2 * b + &2 * c - b * c`);
 
 (SUBGOAL_THEN `G' = f' * (g' ((f:real->real) a'))` ASSUME_TAC);
    (* Subgoal 3.2.2 *)
  (EXPAND_TAC "G'" THEN EXPAND_TAC "f'");
  (EXPAND_TAC "g'" THEN EXPAND_TAC "f" );
  (REWRITE_TAC[]);
   
 (ABBREV_TAC `P = {x:real | &0 < x}`);

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

  (SUBGOAL_THEN 
   `(f has_real_derivative f') (atreal a' within s) /\ 
    (P:real->bool) ((f:real->real) a')`
     ASSUME_TAC);
    (* Subgoal 3.2.4 *)
  CONJ_TAC;  

    (* Subgoal 3.2.4.1 *)
  (EXPAND_TAC "f" THEN EXPAND_TAC "f'");
  (REWRITE_TAC[ups_x]);
  (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
    (* Subgoal 3.2.4.2 *)
  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);

    (SUBGOAL_THEN `!x. (x:real) IN s ==> &0 < f x` ASSUME_TAC);
      (* Subgoal 3.2.4.1.1 *)
    (EXPAND_TAC "s" THEN REWRITE_TAC[IN_ELIM_THM]);
    (EXPAND_TAC "f" THEN MESON_TAC[]);
    (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);

  (ONCE_ASM_REWRITE_TAC[]);
    (* End Subgoal 3.2.4 *)
 
 (REPLICATE_TAC 2 UP_ASM_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2 THEN MESON_TAC[]);
(* --------------------------------------------------------------------------*)
(*  Subgoal 3.3                                                              *)
(*         Derivative of &2 * sqrt (ups_x x b c - x * b * c)                 *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `2G = (\x.  &2 * sqrt (ups_x x b c - x * b * c))`);
 
 (SUBGOAL_THEN 
  `(2G has_real_derivative &2 * G') (atreal a' within s)` ASSUME_TAC);

  (SUBGOAL_THEN `2G = (\x:real. &2 * G x)` ASSUME_TAC);
  (EXPAND_TAC "2G" THEN EXPAND_TAC "G" THEN MESON_TAC[]);
 
 (PURE_ONCE_ASM_REWRITE_TAC[]); 
 (DEL_TAC THEN DEL_TAC ); 
 (FIRST_X_ASSUM MP_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN THEN MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*  Subgoal 3.4                                                              *)
(*         Derivative of  (-- &2 * x + &2 * b + &2 * c - b * c) /            *)
(*                          &2 * sqrt (ups_x x b c - x * b * c)              *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `f1 = (\x. -- &2 * x + &2 * b + &2 * c - b * c)`); 
 (ABBREV_TAC `F12 = (\x. (-- &2 * x + &2 * b + &2 * c - b * c) /
        (&2 * sqrt (ups_x x b c - x * b * c)))`); 
 (SUBGOAL_THEN 
  `(F12 has_real_derivative (-- &2 * 2G (a':real) - (f1 a' * &2 * G')) / 
    2G a' pow 2) (atreal a' within s)` 
   ASSUME_TAC);

  (SUBGOAL_THEN ` F12 = (\x:real. f1 x / 2G x)` ASSUME_TAC);
    (* Subgoal 3.4.1 *)
  (EXPAND_TAC "F12" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f1");
  (ASM_REWRITE_TAC[]);
 
 (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `(f1 has_real_derivative -- &2) (atreal a' within s) /\
     (2G has_real_derivative &2 * G') (atreal a' within s) /\
    ~(2G a' = &0)`
    ASSUME_TAC);
  (* Subgoal 3.4.2 *) 
  (ASM_REWRITE_TAC[]);
  (REPEAT CONJ_TAC);  (* Break into 2 subgoals *)

    (EXPAND_TAC "f1" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
    (EXPAND_TAC "2G");
    (MATCH_MP_TAC 
      (MESON[REAL_ENTIRE] `~ (x = &0) /\ ~ (y = &0) ==> ~ (x * y = &0)`));
    (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);
 
 (FIRST_X_ASSUM MP_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN); 
 (MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*  Subgoal 3.5                                                              *)
(*         Derivative of  atn ((-- &2 * a + &2 * b + &2 * c - b * c) /       *)
(*                          &2 * sqrt (ups_x x b c - x * b * c))             *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `F1 = (\x. atn ((-- &2 * x + &2 * b + &2 * c - b * c) / (&2 * 
   sqrt (ups_x x b c - x * b * c))))`);
 
 (SUBGOAL_THEN 
   `(F1 has_real_derivative
    (-- &2 * 2G a' - f1 a' * &2 * G') / 2G a' pow 2 * inv (&1 + F12 a' pow 2))
    (atreal a' within s)`
  ASSUME_TAC);

  (SUBGOAL_THEN `F1 = (\x. atn (F12 (x:real)))` ASSUME_TAC);
    (* Subgoal 3.5.1 *)
  (EXPAND_TAC "F1" THEN EXPAND_TAC "F12");
  (REWRITE_TAC[]);
 
 (PURE_ONCE_ASM_REWRITE_TAC[]); 
 (REPLICATE_TAC 2 DEL_TAC); 
 (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`); 
 (ABBREV_TAC `f' = (-- &2 * 2G (a':real) - f1 a' * &2 * G') / 2G a' pow 2`);

  (SUBGOAL_THEN 
    `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
    ASSUME_TAC);
    (* Subgoal 3.5.3 *)
  (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
  (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);

  (SUBGOAL_THEN `(F12 has_real_derivative f') (atreal a' within s) /\ 
                   (:real) ((F12:real->real) a')` 
     ASSUME_TAC);
  (ASM_REWRITE_TAC[]);
  (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);

  (SUBGOAL_THEN 
   `inv (&1 + F12 a' pow 2) = g' ((F12:real-> real) a')`
     ASSUME_TAC);
    (* Subgoal 3.5.2 *)
  (EXPAND_TAC "F12" THEN EXPAND_TAC "g'");
  (MESON_TAC[]);
 
 (ONCE_ASM_REWRITE_TAC[]);
 DEL_TAC ; 
 (REPLICATE_TAC 2 UP_ASM_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2); 
 (MESON_TAC[]);

(* ========================================================================= *)
(*           THIS PART TO TO REDUCE THE DERIVATIVE OF F1                     *)
(*             Derivative of  F1 is  -- &1 / sqrt d                          *)  
(* ========================================================================= *)

(* --------------------------------------------------------------------------*)
(*     Subgoal 3.6                                                           *)
(*                 (&2 * sqrt D') pow 2 = &4 * D'                            *)
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN `(&2 * sqrt D') pow 2 = &4 * D'` ASSUME_TAC);
  (REWRITE_TAC[REAL_POW_2]);
  (REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * b = &4 * (a * b)`]);
  (REWRITE_TAC[GSYM REAL_POW_2]);
  AP_TERM_TAC;
  (MATCH_MP_TAC SQRT_POW_2 THEN ASM_REAL_ARITH_TAC);

(* --------------------------------------------------------------------------*)
(*     Subgoal 3.7                                                           *)
(*               Reduce:  inv (&1 + F12 a' pow 2)                            *)
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN 
    `inv (&1 + F12 (a':real) pow 2)  = (&4 * D') / (&4 * D' + Da pow 2)`   
     ASSUME_TAC);
  (EXPAND_TAC "F12");  
  (REWRITE_TAC[REAL_POW_DIV]);
  (ASM_REWRITE_TAC[]);
  (REWRITE_TAC[MESON[REAL_INV_DIV] 
     `(&4 * D') / (&4 * D' + Da pow 2) = 
      inv ((&4 * D' + Da pow 2) / (&4 * D'))`]);
  AP_TERM_TAC;
  (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
  (AP_THM_TAC THEN AP_TERM_TAC);
  (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
  (REWRITE_TAC[MESON[] `~(a = b) <=> ~(b = a)`;REAL_ENTIRE;
                 MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
  ASM_REAL_ARITH_TAC;

(* --------------------------------------------------------------------------*)
(*     Subgoal 3.8                                                           *)
(*               Reduce:  Derivative of F1                                   *)
(* --------------------------------------------------------------------------*)
 
 (SUBGOAL_THEN 
   `(F1 has_real_derivative -- &1 / sqrt D') (atreal a' within s)`
   ASSUME_TAC);

  (SUBGOAL_THEN `2G (a':real) = &2 * sqrt D'` ASSUME_TAC);
    (* Subgoal 3.8.1 *)
  (EXPAND_TAC "2G" THEN EXPAND_TAC "D'");
  (REWRITE_TAC[]);

  (SUBGOAL_THEN `f1 (a':real) = (Da:real)` ASSUME_TAC);  
    (* Subgoal 3.8.2 *)
  (EXPAND_TAC "f1" THEN EXPAND_TAC "Da");
  (REWRITE_TAC[]);

  (SUBGOAL_THEN `&0 < sqrt D'` ASSUME_TAC);
    (* Subgoal 3.8.3 *)
  (MATCH_MP_TAC SQRT_POS_LT);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `(-- &2 * 2G (a':real) - f1 a' * &2 * G') / 2G a' pow 2 *
     inv (&1 + F12 a' pow 2) = 
     -- &1 / sqrt D'` 
    ASSUME_TAC);
    (* Subgoal 3.8.4 *)
  (ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ARITH `(a / b * b / c) = (a / b * b) / c`]);
  (SIMP_TAC[REAL_DIV_RMUL]);

    (SUBGOAL_THEN `~(&4 * D' = &0)` ASSUME_TAC);
      (* Subgoal 3.8.4.1 *)    
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
    (MATCH_MP_TAC REAL_LT_MUL);
    ASM_REAL_ARITH_TAC;      

  (ABBREV_TAC `M = (-- &2 * &2 * sqrt D' - Da * &2 * G')`);

    (SUBGOAL_THEN `G' = Da * inv (&2 * sqrt D')` ASSUME_TAC);  
      (* Subgoal 3.8.4.2 *)
    (EXPAND_TAC "G'" THEN EXPAND_TAC "Da" THEN EXPAND_TAC "D'");
    (AP_THM_TAC THEN AP_TERM_TAC);
    (EXPAND_TAC "f1" THEN REAL_ARITH_TAC);

    (SUBGOAL_THEN `M = -- (&4 * D' + Da pow 2) / sqrt D'` ASSUME_TAC);
      (* Subgoal 3.8.4.3 *)
    (EXPAND_TAC "M");
    (REWRITE_TAC[REAL_ARITH `-- &2 * &2 * x = -- &4 * x`]);
    (ONCE_ASM_REWRITE_TAC[]);
    (ABBREV_TAC `X = -- &4 * sqrt D' - Da * &2 * Da * inv (&2 * sqrt D')`);
    (ABBREV_TAC `Y = --(&4 * D' + Da pow 2)`);
    (ABBREV_TAC `Z = sqrt D'`);
    
       (SUBGOAL_THEN `X * Z = Y ==> X = Y / Z ` ASSUME_TAC);
         (* Subgoal 3.8.4.3.1 *)
       (ASM_SIMP_TAC[REAL_EQ_RDIV_EQ]);
    
    (FIRST_X_ASSUM MATCH_MP_TAC);
    (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
    (REWRITE_TAC[REAL_SUB_RDISTRIB; REAL_NEG_ADD]);
    (REWRITE_TAC[REAL_ARITH ` (a * b * a * c) * d = a pow 2 * c * b * d`]);

      (SUBGOAL_THEN `inv (&2 * sqrt D') * &2 * sqrt D' = &1` ASSUME_TAC);
      (MATCH_MP_TAC REAL_MUL_LINV);
      (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
      (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
      (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
      (MATCH_MP_TAC SQRT_POS_LT);
      (ASM_REWRITE_TAC[]);

    (ASM_REWRITE_TAC[]);
    (REWRITE_TAC[REAL_ARITH `a - b = a + --b`;REAL_MUL_RID]);
    (AP_THM_TAC THEN AP_TERM_TAC);
    (REWRITE_TAC[REAL_ARITH `(--a * b) * c = -- (a * (b * c))`]);
    (REPEAT AP_TERM_TAC);
    (REWRITE_TAC[GSYM REAL_POW_2]);
    (EXPAND_TAC "Z");
    (MATCH_MP_TAC SQRT_POW_2);
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
    (ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `M / (&4 * D') * &4 * D' = M` ASSUME_TAC);
      (* Subgoal 3.8.4.4 *)
    (ASM_MESON_TAC[REAL_DIV_RMUL]);

  (ONCE_ASM_REWRITE_TAC[]);
  (ONCE_ASM_REWRITE_TAC[]);
  (ASM_REWRITE_TAC [REAL_ARITH `a / b / c = a / c / b`]);
  (AP_THM_TAC THEN AP_TERM_TAC);
  (MATCH_MP_TAC (REAL_ARITH `a / a = &1 ==> -- a / a = -- &1`));
  (MATCH_MP_TAC REAL_DIV_REFL);
  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
  (MATCH_MP_TAC REAL_LTE_ADD);
  (REWRITE_TAC[REAL_LE_POW_2]);
  (MATCH_MP_TAC REAL_LT_MUL);
  (ASM_REWRITE_TAC[]);
  (REAL_ARITH_TAC);
    (* End of subgoal 3.8.4 *)
 
 (ASM_MESON_TAC[]);

(* Delete unnecessary assumptions in assumption list  *)
 
 (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC); 
 (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC); 
 (REPEAT DISCH_TAC);


(* ================ END DIFF F1 ============================================ *)

(* --------------------------------------------------------------------------*)
(*  Subgoal 3.9                                                              *)
(*         Derivative of  (-- &2 * b + &2 * c + &2 * a - c * a) /            *)
(*                          &2 * sqrt (ups_x x b c - x * b * c)              *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `f2 = (\x. -- &2 * b + &2 * c + &2 * x - c * x)`); 
 (ABBREV_TAC `F22 = (\x. (-- &2 * b + &2 * c + &2 * x - c * x) / (&2 * 
  sqrt (ups_x x b c - x * b * c)))`);

  (SUBGOAL_THEN 
    `(F22 has_real_derivative ((&2 - c) * 2G (a':real) - 
     f2 a' * &2 * G') / 2G a' pow 2) (atreal a' within s)`
     ASSUME_TAC);

    (SUBGOAL_THEN ` F22 = (\x:real. f2 x / 2G x )` ASSUME_TAC);
      (* Subgoal 3.9.1 *)
    (EXPAND_TAC "F22" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f2");   
    (ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `(f2 has_real_derivative &2 - c) (atreal a' within s) /\
                     (2G has_real_derivative &2 * G') (atreal a' within s) /\
                    ~(2G a' = &0)` ASSUME_TAC);
      (* Subgoal 3.9.2 *) 
    (ASM_REWRITE_TAC[]);
    (REPEAT CONJ_TAC);  (* Break into 2 subgoals *)

    (EXPAND_TAC "f2" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
    (EXPAND_TAC "2G");
    (MATCH_MP_TAC 
      (MESON[REAL_ENTIRE] `~ (x = &0) /\ ~ (y = &0) ==> ~ (x * y = &0)`));
    (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);
 
 (ASM_REWRITE_TAC[]); 
 (FIRST_X_ASSUM MP_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN); 
 (MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*  Subgoal 3.10                                                             *)
(*         Derivative of  atn ((-- &2 * b + &2 * c + &2 * a - c * a) /       *)
(*                          &2 * sqrt (ups_x x b c - x * b * c))             *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `F2 = (\x. atn ((-- &2 * b + &2 * c + &2 * x - c * x) /(&2 *    
   sqrt (ups_x x b c - x * b * c))))`);
  
 (SUBGOAL_THEN `(F2 has_real_derivative
  ((&2 - c) * 2G a' - f2 a' * &2 * G') / 2G a' pow 2 * inv (&1 + F22 a' pow 2))
  (atreal a' within s)`
   ASSUME_TAC);

  (SUBGOAL_THEN `F2 = (\x. atn (F22 (x:real)))` ASSUME_TAC);
    (* Subgoal 3.10.1 *) 
  (EXPAND_TAC "F2" THEN EXPAND_TAC "F22");
  (REWRITE_TAC[]); 
 
 (PURE_ONCE_ASM_REWRITE_TAC[]); 
 (REPLICATE_TAC 2 DEL_TAC); 
 (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`); 
 (ABBREV_TAC `f' = ((&2 - c) * 2G a' - f2 a' * &2 * G') / 
                    2G (a':real) pow 2`);

  (SUBGOAL_THEN 
    `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
    ASSUME_TAC);
    (* Subgoal 3.10.2 *)
  (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
  (REWRITE_TAC[EQ_UNIV;HAS_REAL_DERIVATIVE_ATN]);

  (SUBGOAL_THEN `(F22 has_real_derivative f') (atreal a' within s) /\ 
                   (:real) ((F22:real->real) a')` 
     ASSUME_TAC);
  (ASM_REWRITE_TAC[]);
  (MESON_TAC[EQ_UNIV;IN_UNIV;IN]);

  (SUBGOAL_THEN 
   `inv (&1 + F22 a' pow 2) = g' ((F22:real-> real) a')`
     ASSUME_TAC);
    (* Subgoal 3.10.3 *)
  (EXPAND_TAC "F22" THEN EXPAND_TAC "g'");
  (REWRITE_TAC[]);
 
 (ONCE_ASM_REWRITE_TAC[]);
 DEL_TAC ; 
 (REPLICATE_TAC 2 UP_ASM_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2); 
 (MESON_TAC[]);

(* ========================================================================= *)
(*           THIS PART TO TO REDUCE THE DERIVATIVE OF F2                     *)
(*             Derivative of  F2 is  ..... / sqrt d                          *)  
(* ========================================================================= *)

(* --------------------------------------------------------------------------*)
(*     Subgoal 3.11                                                           *)
(*                 (&2 * sqrt D') pow 2 = &4 * D'                            *)
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN `(&2 * sqrt D') pow 2 = &4 * D'` ASSUME_TAC);
  (REWRITE_TAC[REAL_POW_2]);
  (REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * b = &4 * (a * b)`]);
  (REWRITE_TAC[GSYM REAL_POW_2]);
  AP_TERM_TAC;
  (MATCH_MP_TAC SQRT_POW_2 THEN ASM_REAL_ARITH_TAC);

(* --------------------------------------------------------------------------*)
(*     Subgoal 3.12                                                           *)
(*               Reduce:  inv (&1 + F22 a' pow 2)                            *)
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN 
    `inv (&1 + F22 (a':real) pow 2)  = (&4 * D') / (&4 * D' + Db pow 2)`   
     ASSUME_TAC);
  (EXPAND_TAC "F22");  
  (REWRITE_TAC[REAL_POW_DIV]);
  (ASM_REWRITE_TAC[]);
  (REWRITE_TAC[MESON[REAL_INV_DIV] 
     `(&4 * D') / (&4 * D' + Db pow 2) = 
      inv ((&4 * D' + Db pow 2) / (&4 * D'))`]);
  AP_TERM_TAC;
  (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
  (EXPAND_TAC "Db");
  (REWRITE_TAC[REAL_ARITH `a + b + c - x * y = a + b + c - y * x`]);
  (AP_THM_TAC THEN AP_TERM_TAC);
  (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
  (REWRITE_TAC[MESON[] `~(a = b) <=> ~(b = a)`;REAL_ENTIRE;
                 MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
  ASM_REAL_ARITH_TAC;


(* --------------------------------------------------------------------------*)
(*     Subgoal 3.13                                                          *)
(*               Reduce:  Derivative of F2                                   *)
(* --------------------------------------------------------------------------*)
 
 (SUBGOAL_THEN 
   `(F2 has_real_derivative 
    (-- &2 * c + &2 * a' + &2 * b - a' * b) / (a' * (&4 - a')) / sqrt D')
    (atreal a' within s)`
   ASSUME_TAC);

  (SUBGOAL_THEN `2G (a':real) = &2 * sqrt D'` ASSUME_TAC);
    (* Subgoal 3.13.1 *)
  (EXPAND_TAC "2G" THEN EXPAND_TAC "D'");
  (REWRITE_TAC[]);

  (SUBGOAL_THEN `f2 (a':real) = (Db:real)` ASSUME_TAC);  
    (* Subgoal 3.13.2 *)
  (EXPAND_TAC "f2" THEN EXPAND_TAC "Db");
  (REAL_ARITH_TAC);

  (SUBGOAL_THEN `&0 < sqrt D'` ASSUME_TAC);
    (* Subgoal 3.13.3 *)
  (MATCH_MP_TAC SQRT_POS_LT);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN `
    ((&2 - c) * 2G a' - f2 a' * &2 * G') / 2G a' pow 2 *
    inv (&1 + F22 a' pow 2) = 
    (-- &2 * c + &2 * a' + &2 * b - a' * b) / (a' * (&4 - a')) / sqrt D' `
    ASSUME_TAC);
    (* Subgoal 3.13.4 *)
  (ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ARITH `(a / b * b / c) = (a / b * b) / c`]);
  (SIMP_TAC[REAL_DIV_RMUL]);


    (SUBGOAL_THEN `~(&4 * D' = &0)` ASSUME_TAC);
      (* Subgoal 3.13.4.1 *)    
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
    (MATCH_MP_TAC REAL_LT_MUL);
    ASM_REAL_ARITH_TAC;      

  (ABBREV_TAC `M = (&2 - c) * &2 * sqrt D' - Db * &2 * G'`);

    (SUBGOAL_THEN `G' = Da * inv (&2 * sqrt D')` ASSUME_TAC);  
      (* Subgoal 3.13.4.2 *)
    (EXPAND_TAC "G'" THEN EXPAND_TAC "Da" THEN EXPAND_TAC "D'");
    (REWRITE_TAC[]);

    (SUBGOAL_THEN `M = ((&4 - &2 * c) * D' - Da * Db) / sqrt D'` ASSUME_TAC);
      (* Subgoal 3.13.4.3 *)
    (EXPAND_TAC "M");
    (REWRITE_TAC[REAL_ARITH `(&2 - c) * &2 * x = (&4 - &2 * c) * x`]);
    (ONCE_ASM_REWRITE_TAC[]);
    (ABBREV_TAC `X = (&4 - &2 * c) * sqrt D' - 
                       Db * &2 * Da * inv (&2 * sqrt D')`);
    (ABBREV_TAC `Y = (&4 - &2 * c) * D' - Da * Db`);
    (ABBREV_TAC `Z = sqrt D'`);
    
       (SUBGOAL_THEN `X * Z = Y ==> X = Y / Z ` ASSUME_TAC);
         (* Subgoal 3.13.4.3.1 *)
       (ASM_SIMP_TAC[REAL_EQ_RDIV_EQ]);


    (FIRST_X_ASSUM MATCH_MP_TAC);
    (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
    (ABBREV_TAC `m = &4 - &2 * c`);
    (REWRITE_TAC[REAL_SUB_RDISTRIB;REAL_NEG_ADD]);
    (REWRITE_TAC[REAL_ARITH ` (a * b * c * d) * e = (c * a) * (d * b * e)`]);

      (SUBGOAL_THEN `inv (&2 * sqrt D') * &2 * sqrt D' = &1` ASSUME_TAC);
         (* Subgoal 3.13.4.3.2 *)
      (MATCH_MP_TAC REAL_MUL_LINV);
      (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
      (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
      (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
      (ASM_REWRITE_TAC[]);

    (PURE_ONCE_ASM_REWRITE_TAC[]);
    (EXPAND_TAC "Y");
    (REWRITE_TAC[REAL_MUL_RID]);
    (AP_THM_TAC THEN AP_TERM_TAC);
    (EXPAND_TAC "m" THEN EXPAND_TAC "Z");
    (REWRITE_TAC[REAL_ARITH `(a * b) * c = a * b * c`]);
    (REPEAT AP_TERM_TAC);
    (REWRITE_TAC[GSYM REAL_POW_2]);
    (MATCH_MP_TAC SQRT_POW_2);
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
    (ASM_REWRITE_TAC[]);
      (* End of Subgoal 3.13.4.3 *)


    (SUBGOAL_THEN `M / (&4 * D') * &4 * D' = M` ASSUME_TAC);
      (* Subgoal 3.13.4.4 *)
    (ASM_SIMP_TAC[REAL_DIV_RMUL]);

  (PURE_ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);  

    (SUBGOAL_THEN 
      `M = ((-- &2 * c + &2 * a' + &2 * b - a' * b) * (&4 - c) * c)/ sqrt D'`
       ASSUME_TAC);
      (* Subgoal 3.13.4.5 *)
    (ONCE_ASM_REWRITE_TAC[]);
    (AP_THM_TAC THEN AP_TERM_TAC);
    (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
    (EXPAND_TAC "Da" THEN EXPAND_TAC "Db" THEN EXPAND_TAC "f2");
    (EXPAND_TAC "Dc");
    REAL_ARITH_TAC;

  (UP_ASM_TAC THEN DEL_TAC THEN REPEAT DISCH_TAC);
  (ONCE_ASM_REWRITE_TAC[]);
  (EXPAND_TAC "Dc");
  (REWRITE_TAC[REAL_ARITH `a / b / c = a / c / b`]);
  (AP_THM_TAC THEN AP_TERM_TAC);

    (SUBGOAL_THEN 
       `&4 * D' + Db pow 2 = a' * (&4 - a') * (&4 - c) * c` ASSUME_TAC);
      (* Subgoal 3.13.4.6 *)      
    (EXPAND_TAC "Db" THEN EXPAND_TAC "f2" THEN REWRITE_TAC[POW_2] );
    (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
     REAL_ARITH_TAC;
  
  (ONCE_ASM_REWRITE_TAC[]);
  (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);

     (* --------------------------------------------------------------- *)
     (*       ~ ( c = &4) /\ ~ (c = &0)                                 *)
     (* --------------------------------------------------------------- *)

      (SUBGOAL_THEN `~ (c = &4) /\ ~ (c = &0)` ASSUME_TAC);
      ASM_REAL_ARITH_TAC;
      (SUBGOAL_THEN `~ ((&4 - c) * c = &0)` ASSUME_TAC); 
      (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
      (ASM_REWRITE_TAC[REAL_ARITH ` ~(a - b = &0) <=> ~ (a = b)`]);

      (* --------------------------------------------------------------- *)
      (*       ~ ( a' = &4) /\ ~ (a' = &0)                               *)
      (* --------------------------------------------------------------- *)

      (SUBGOAL_THEN `~ (a' = &4) /\ ~ (a' = &0)` ASSUME_TAC);
      (REPEAT STRIP_TAC);  (* 2 Subgoals *)

        (SUBGOAL_THEN ` D' = -- ((c + b - &4) pow 2)` ASSUME_TAC);
        (EXPAND_TAC "D'" );
        (REWRITE_TAC[ups_x]);
        (ONCE_ASM_REWRITE_TAC[]);
        REAL_ARITH_TAC;
        (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
        (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
        (MESON_TAC[REAL_LE_POW_2]);
        (MP_TAC (ASSUME `&0 < D'`));      
        (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);


        (SUBGOAL_THEN ` D' = -- ((c - b) pow 2)` ASSUME_TAC);
        (EXPAND_TAC "D'" );
        (REWRITE_TAC[ups_x]);
        (ONCE_ASM_REWRITE_TAC[]);
        REAL_ARITH_TAC;
        (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
        (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
        (MESON_TAC[REAL_LE_POW_2]);
        (MP_TAC (ASSUME `&0 < D'`));      
        (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);


     (SUBGOAL_THEN `~ (a' * (&4 - a') = &0)` ASSUME_TAC);
     (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
     (ASM_REWRITE_TAC[REAL_ARITH ` ~(a - b = &0) <=> ~ (a = b)`]);

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

  (ABBREV_TAC `x = -- &2 * c + &2 * a' + &2 * b - a' * b`);
  (ABBREV_TAC `y = (&4 - c) * c`);
  (REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);
  (ABBREV_TAC `z = a' * (&4 - a')`);
  (ASM_SIMP_TAC[REDUCE_WITH_DIV_Euler_lemma]);
  (ASM_MESON_TAC[]);
 
 (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC); 
 (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC THEN REPEAT DISCH_TAC);

(* ================ END DIFF 2 ============================================= *)



(* --------------------------------------------------------------------------*)
(* Subgoal 14                                                                *)
(*         Derivative of  (-- &2 * c + &2 * a + &2 * b - a * b) /            *)
(*                          &2 * sqrt (ups_x x b c - x * b * c)              *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `f3 = (\x. -- &2 * c + &2 * x + &2 * b - x * b)`); 
 (ABBREV_TAC `F32 = (\x. (-- &2 * c + &2 * x + &2 * b - x * b) /
        (&2 * sqrt (ups_x x b c - x * b * c)))`);

  (SUBGOAL_THEN 
    `(F32 has_real_derivative ((&2 - b) * 2G (a':real) - 
     f3 a' * &2 * G') / 2G a' pow 2) (atreal a' within s)`
     ASSUME_TAC);

    (SUBGOAL_THEN ` F32 = (\x:real. f3 x / 2G x )` ASSUME_TAC);
      (* Subgoal 3.14.1 *)
    (EXPAND_TAC "F32" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f3");   
    (ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `(f3 has_real_derivative &2 - b) (atreal a' within s) /\
                     (2G has_real_derivative &2 * G') (atreal a' within s) /\
                    ~(2G a' = &0)` ASSUME_TAC);
      (* Subgoal 3.14.2 *) 
    (ASM_REWRITE_TAC[]);
    (REPEAT CONJ_TAC);  (* Break into 2 subgoals *)

    (EXPAND_TAC "f3" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
    (EXPAND_TAC "2G");
    (MATCH_MP_TAC 
      (MESON[REAL_ENTIRE] `~ (x = &0) /\ ~ (y = &0) ==> ~ (x * y = &0)`));
    (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);
 
 (ASM_REWRITE_TAC[]); 
 (FIRST_X_ASSUM MP_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN); 
 (MESON_TAC[]);


(* --------------------------------------------------------------------------*)
(*  Subgoal 3.15                                                             *)
(*         Derivative of  atn ((-- &2 * c + &2 * a + &2 * b - a * b) /       *)
(*                          &2 * sqrt (ups_x x b c - x * b * c))             *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `F3 = (\x. atn ((-- &2 * c + &2 * x + &2 * b - x * b) /(&2 *    
   sqrt (ups_x x b c - x * b * c))))`);
  
 (SUBGOAL_THEN `(F3 has_real_derivative
  ((&2 - b) * 2G a' - f3 a' * &2 * G') / 2G a' pow 2 * inv (&1 + F32 a' pow 2))
  (atreal a' within s)`
   ASSUME_TAC);

  (SUBGOAL_THEN `F3 = (\x. atn (F32 (x:real)))` ASSUME_TAC);
    (* Subgoal 3.15.1 *) 
  (EXPAND_TAC "F3" THEN EXPAND_TAC "F32");
  (REWRITE_TAC[]); 
 
 (PURE_ONCE_ASM_REWRITE_TAC[]); 
 (REPLICATE_TAC 2 DEL_TAC); 
 (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`); 
 (ABBREV_TAC `f' = ((&2 - b) * 2G a' - f3 a' * &2 * G') / 
                    2G (a':real) pow 2`);

  (SUBGOAL_THEN 
    `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
    ASSUME_TAC);
    (* Subgoal 3.15.2 *)
  (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
  (REWRITE_TAC[EQ_UNIV;HAS_REAL_DERIVATIVE_ATN]);

  (SUBGOAL_THEN `(F32 has_real_derivative f') (atreal a' within s) /\ 
                   (:real) ((F32:real->real) a')` 
     ASSUME_TAC);
  (ASM_REWRITE_TAC[]);
  (MESON_TAC[EQ_UNIV;IN_UNIV;IN]);

  (SUBGOAL_THEN 
   `inv (&1 + F32 a' pow 2) = g' ((F32:real-> real) a')`
     ASSUME_TAC);
    (* Subgoal 3.15.3 *)
  (EXPAND_TAC "F32" THEN EXPAND_TAC "g'");
  (REWRITE_TAC[]);
 
 (ONCE_ASM_REWRITE_TAC[]);
    DEL_TAC ; 
 (REPLICATE_TAC 2 UP_ASM_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2); 
 (MESON_TAC[]);

(* ========================================================================= *)
(*           THIS PART TO TO REDUCE THE DERIVATIVE OF F3                     *)
(*             Derivative of  F3 is  ..... / sqrt d                          *)  
(* ========================================================================= *)


(* --------------------------------------------------------------------------*)
(*     Subgoal 3.16                                                          *)
(*                 (&2 * sqrt D') pow 2 = &4 * D'                            *)
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN `(&2 * sqrt D') pow 2 = &4 * D'` ASSUME_TAC);
  (REWRITE_TAC[REAL_POW_2]);
  (REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * b = &4 * (a * b)`]);
  (REWRITE_TAC[GSYM REAL_POW_2]);
      AP_TERM_TAC;
  (MATCH_MP_TAC SQRT_POW_2 THEN ASM_REAL_ARITH_TAC);

(* --------------------------------------------------------------------------*)
(*     Subgoal 3.17                                                          *)
(*               Reduce:  inv (&1 + F32 a' pow 2)                            *)
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN 
    `inv (&1 + F32 (a':real) pow 2)  = (&4 * D') / (&4 * D' + Dc pow 2)`   
     ASSUME_TAC);
  (EXPAND_TAC "F32");  
  (REWRITE_TAC[REAL_POW_DIV]);
  (ASM_REWRITE_TAC[]);
  (REWRITE_TAC[MESON[REAL_INV_DIV] 
     `(&4 * D') / (&4 * D' + Dc pow 2) = 
      inv ((&4 * D' + Dc pow 2) / (&4 * D'))`]);
      AP_TERM_TAC;
  (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
  (EXPAND_TAC "Dc");
  (REWRITE_TAC[REAL_ARITH `a + b + c - x * y = a + b + c - y * x`]);
  (AP_THM_TAC THEN AP_TERM_TAC);
  (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
  (REWRITE_TAC[MESON[] `~(a = b) <=> ~(b = a)`;REAL_ENTIRE;
                 MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
      ASM_REAL_ARITH_TAC;

(* --------------------------------------------------------------------------*)
(*     Subgoal 3.18                                                          *)
(*               Reduce:  Derivative of F3                                   *)
(* --------------------------------------------------------------------------*)
 
 (SUBGOAL_THEN 
   `(F3 has_real_derivative 
    (-- &2 * b + &2 * a' + &2 * c - a' * c) / (a' * (&4 - a')) / sqrt D')
    (atreal a' within s)`
   ASSUME_TAC);

  (SUBGOAL_THEN `2G (a':real) = &2 * sqrt D'` ASSUME_TAC);
    (* Subgoal 3.18.1 *)
  (EXPAND_TAC "2G" THEN EXPAND_TAC "D'");
  (REWRITE_TAC[]);

  (SUBGOAL_THEN `f3 (a':real) = (Dc:real)` ASSUME_TAC);  
    (* Subgoal 3.18.2 *)
  (EXPAND_TAC "f3" THEN EXPAND_TAC "Dc");
  (REAL_ARITH_TAC);

  (SUBGOAL_THEN `&0 < sqrt D'` ASSUME_TAC);
    (* Subgoal 3.18.3 *)
  (MATCH_MP_TAC SQRT_POS_LT);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN `
    ((&2 - b) * 2G a' - f3 a' * &2 * G') / 2G a' pow 2 *
    inv (&1 + F32 a' pow 2) = 
    (-- &2 * b + &2 * a' + &2 * c - a' * c) / (a' * (&4 - a')) / sqrt D' `
    ASSUME_TAC);
    (* Subgoal 3.18.4 *)
  (ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ARITH `(a / b * b / c) = (a / b * b) / c`]);
  (SIMP_TAC[REAL_DIV_RMUL]);

    (SUBGOAL_THEN `~(&4 * D' = &0)` ASSUME_TAC);
      (* Subgoal 3.18.4.1 *)    
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
    (MATCH_MP_TAC REAL_LT_MUL);
    (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);      

  (ABBREV_TAC `M = (&2 - b) * &2 * sqrt D' - Dc * &2 * G'`);

    (SUBGOAL_THEN `G' = Da * inv (&2 * sqrt D')` ASSUME_TAC);  
      (* Subgoal 3.18.4.2 *)
    (EXPAND_TAC "G'" THEN EXPAND_TAC "Da" THEN EXPAND_TAC "D'");
    (REWRITE_TAC[]);

    (SUBGOAL_THEN `M = ((&4 - &2 * b) * D' - Da * Dc) / sqrt D'` ASSUME_TAC);
      (* Subgoal 3.18.4.3 *)
    (EXPAND_TAC "M");
    (REWRITE_TAC[REAL_ARITH `(&2 - b) * &2 * x = (&4 - &2 * b) * x`]);
    (ONCE_ASM_REWRITE_TAC[]);
    (ABBREV_TAC `X = (&4 - &2 * b) * sqrt D' - 
                       Dc * &2 * Da * inv (&2 * sqrt D')`);
    (ABBREV_TAC `Y = (&4 - &2 * b) * D' - Da * Dc`);
    (ABBREV_TAC `Z = sqrt D'`);
    
      (SUBGOAL_THEN `X * Z = Y ==> X = Y / Z ` ASSUME_TAC);
         (* Subgoal 3.18.4.3.1 *)
      (ASM_SIMP_TAC[REAL_EQ_RDIV_EQ]);

    (FIRST_X_ASSUM MATCH_MP_TAC);
    (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
    (ABBREV_TAC `m = &4 - &2 * b`);
    (REWRITE_TAC[REAL_SUB_RDISTRIB;REAL_NEG_ADD]);
    (REWRITE_TAC[REAL_ARITH ` (a * b * c * d) * e = (c * a) * (d * b * e)`]);

     (SUBGOAL_THEN `inv (&2 * sqrt D') * &2 * sqrt D' = &1` ASSUME_TAC);
         (* Subgoal 3.18.4.3.2 *)
     (MATCH_MP_TAC REAL_MUL_LINV);
     (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
     (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
     (ASM_REWRITE_TAC[]);

    (PURE_ONCE_ASM_REWRITE_TAC[]);
    (EXPAND_TAC "Y");
    (REWRITE_TAC[REAL_MUL_RID]);
    (AP_THM_TAC THEN AP_TERM_TAC);
    (EXPAND_TAC "m" THEN EXPAND_TAC "Z");
    (REWRITE_TAC[REAL_ARITH `(a * b) * c = a * b * c`]);
    (REPEAT AP_TERM_TAC);
    (REWRITE_TAC[GSYM REAL_POW_2]);
    (MATCH_MP_TAC SQRT_POW_2);
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
    (ASM_REWRITE_TAC[]);
      (* End of Subgoal 3.18.4.3 *)

    (SUBGOAL_THEN `M / (&4 * D') * &4 * D' = M` ASSUME_TAC);
      (* Subgoal 3.18.4.4 *)
    (ASM_SIMP_TAC[REAL_DIV_RMUL]);
  
  (PURE_ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);  

    (SUBGOAL_THEN 
      `M = ((-- &2 * b + &2 * a' + &2 * c - a' * c) * (&4 - b) * b)/ sqrt D'`
       ASSUME_TAC);
      (* Subgoal 3.18.4.5 *)
    (ONCE_ASM_REWRITE_TAC[]);
    (AP_THM_TAC THEN AP_TERM_TAC);
    (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
    (EXPAND_TAC "Da" THEN EXPAND_TAC "Dc" THEN EXPAND_TAC "f3");
    REAL_ARITH_TAC;

  (UP_ASM_TAC THEN DEL_TAC THEN REPEAT DISCH_TAC);
  (ONCE_ASM_REWRITE_TAC[]);
  (EXPAND_TAC "Dc");
  (REWRITE_TAC[REAL_ARITH `a / b / c = a / c / b`]);
  (AP_THM_TAC THEN AP_TERM_TAC);

    (SUBGOAL_THEN 
       `&4 * D' + f3 a' pow 2 = a' * (&4 - a') * (&4 - b) * b` ASSUME_TAC);
      (* Subgoal 3.18.4.6 *)      
    (EXPAND_TAC "f3" THEN REWRITE_TAC[POW_2] );
    (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
   REAL_ARITH_TAC;

  (ONCE_ASM_REWRITE_TAC[]);
  (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);

     (* --------------------------------------------------------------- *)
     (*       ~ ( b = &4) /\ ~ (b = &0)                                 *)
     (* --------------------------------------------------------------- *)

    (SUBGOAL_THEN `~ (b = &4) /\ ~ (b = &0)` ASSUME_TAC);
    (ASM_REAL_ARITH_TAC);

     (SUBGOAL_THEN `~ ((&4 - b) * b = &0)` ASSUME_TAC); 
     (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
     (ASM_REWRITE_TAC[REAL_ARITH ` ~(a - b = &0) <=> ~ (a = b)`]);

      (* --------------------------------------------------------------- *)
      (*       ~ ( a' = &4) /\ ~ (a' = &0)                               *)
      (* --------------------------------------------------------------- *)

     (SUBGOAL_THEN `~ (a' = &4) /\ ~ (a' = &0)` ASSUME_TAC);
     (REPEAT STRIP_TAC);  (* 2 Subgoals *)

        (SUBGOAL_THEN ` D' = -- ((c + b - &4) pow 2)` ASSUME_TAC);
        (EXPAND_TAC "D'" );
        (REWRITE_TAC[ups_x]);
        (ONCE_ASM_REWRITE_TAC[]);
         REAL_ARITH_TAC;
        (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
        (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
        (MESON_TAC[REAL_LE_POW_2]);
        (MP_TAC (ASSUME `&0 < D'`));
        (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);

        (SUBGOAL_THEN ` D' = -- ((c - b) pow 2)` ASSUME_TAC);
        (EXPAND_TAC "D'" );
        (REWRITE_TAC[ups_x]);
        (ONCE_ASM_REWRITE_TAC[]);
         REAL_ARITH_TAC;
        (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
        (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
        (MESON_TAC[REAL_LE_POW_2]);
        (MP_TAC (ASSUME `&0 < D'`));
        (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);

     (SUBGOAL_THEN `~ (a' * (&4 - a') = &0)` ASSUME_TAC);
     (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
     (ASM_REWRITE_TAC[REAL_ARITH ` ~(a - b = &0) <=> ~ (a = b)`]);

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

  (ABBREV_TAC `x = -- &2 * b + &2 * a' + &2 * c - a' * c`);
  (ABBREV_TAC `y = (&4 - b) * b`);
  (REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);
  (ABBREV_TAC `z = a' * (&4 - a')`);
  (ASM_SIMP_TAC[REDUCE_WITH_DIV_Euler_lemma]);
  (ASM_MESON_TAC[]);
 
 (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC); 
 (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC THEN REPEAT DISCH_TAC);

(* ================ END DIFF 3 ============================================= *)


(* --------------------------------------------------------------------------*)
(*    Subgoal 3.19.                                                          *)
(*       Derivative of  (&8 - a - b - c) / sqrt (ups_x a b c - a * b * c)    *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `f4 = (\x. (&8 - x - b - c))`); 
 (ABBREV_TAC `F42 = (\x. (&8 - x - b - c) / sqrt (ups_x x b c - x * b * c))`);
 
 (SUBGOAL_THEN 
  `(F42 has_real_derivative (-- &1 * G a' - f4 a' * G') / G a' pow 2)
   (atreal a' within s)`
   ASSUME_TAC);

  (SUBGOAL_THEN ` F42 = (\x:real. f4 x / G x)` ASSUME_TAC);
    (* Subgoal 3.19.1  *)
  (EXPAND_TAC "F42" THEN EXPAND_TAC "G" THEN EXPAND_TAC "f4");
  (REWRITE_TAC[]);
 
 (PURE_ONCE_ASM_REWRITE_TAC[] THEN REPLICATE_TAC 2 DEL_TAC);

  (SUBGOAL_THEN `(f4 has_real_derivative -- &1) (atreal a' within s) /\
                   (G has_real_derivative G') (atreal a' within s) /\
                   ~(G a' = &0)` ASSUME_TAC);
    (* Subgoal 3.19.2 *)
  (ASM_REWRITE_TAC[]);
  CONJ_TAC;  (* Break into 2 subgoals *)
  
    (EXPAND_TAC "f4" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
      (* End one of 2 subgoals *)
    (EXPAND_TAC "G");
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);
 
 (FIRST_X_ASSUM MP_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN); 
 (MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*    Subgoal 3.20.                                                          *)
(*  Derivative of  atn ((&8 - a - b - c) / sqrt (ups_x a b c - a * b * c))   *) 
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC 
  `F4 = (\x. atn ((&8 - x - b - c) / (sqrt (ups_x x b c - x * b * c))))`);
 
 (SUBGOAL_THEN 
  `(F4 has_real_derivative
    (-- &1 * G a' - f4 a' * G') / G a' pow 2 * inv (&1 + F42 a' pow 2))
   (atreal a' within s)`
  ASSUME_TAC);

  (SUBGOAL_THEN `F4 = (\x. atn (F42 (x:real)))` ASSUME_TAC);
    (* Subgoal 3.20.1 *)
  (EXPAND_TAC "F4" THEN EXPAND_TAC "F42");
  (REWRITE_TAC[]); 
 
 (PURE_ONCE_ASM_REWRITE_TAC[]); 
 (REPLICATE_TAC 2 DEL_TAC); 
 (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`); 
 (ABBREV_TAC `f' = ( -- &1 * G (a':real) - f4 a' * G') / G  a' pow 2`);

  (SUBGOAL_THEN 
     `inv (&1 + F42 a' pow 2) = g' ((F42:real-> real) a')`
     ASSUME_TAC);
    (* Subgoal 3.20.2 *)
  (EXPAND_TAC "F42" THEN EXPAND_TAC "g'");
  (REWRITE_TAC[]);

  (SUBGOAL_THEN 
   `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
     ASSUME_TAC);
    (* Subgoal 3.20.3 *)
  (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
  (REWRITE_TAC[EQ_UNIV;HAS_REAL_DERIVATIVE_ATN]);

  (SUBGOAL_THEN 
   `(F42 has_real_derivative f') (atreal a' within s) /\ 
    (:real) ((F42:real->real) a')`
    ASSUME_TAC);
    (* Subgoal 3.20.4 *)
  (ASM_REWRITE_TAC[]);
  (MESON_TAC[EQ_UNIV;IN_UNIV;IN]);
 
 (ONCE_ASM_REWRITE_TAC[]); 
 (REPLICATE_TAC 2 UP_ASM_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2); 
 (MESON_TAC[]);


(* ========================================================================= *)
(*           THIS PART TO TO REDUCE THE DERIVATIVE OF F4                     *)
(*             Derivative of  F4 is  ..... ........                          *)  
(* ========================================================================= *)
(*          Subgoal 3.21                                                     *)
(* ------------------------------------------------------------------------- *)
 
 (SUBGOAL_THEN 
   `(F4 has_real_derivative (a' - b - c) / &2 / (&4 - a') / sqrt D')
    (atreal a' within s)`
  ASSUME_TAC);

  (SUBGOAL_THEN `G (a':real) = sqrt D'` ASSUME_TAC);
    (* Subgoal 3.21.1 *)
  (EXPAND_TAC "G" THEN EXPAND_TAC "D'");
  (REWRITE_TAC[]);
 
 (ABBREV_TAC `D4 = &8 - a' - b - c`);

  (SUBGOAL_THEN `f4 (a':real) = (D4:real)` ASSUME_TAC);  
    (* Subgoal 3.21.2 *)
  (EXPAND_TAC "f4" THEN EXPAND_TAC "D4");
  (REWRITE_TAC[]);

  (SUBGOAL_THEN `&0 < sqrt D'` ASSUME_TAC);
    (* Subgoal 3.21.3 *)
  (MATCH_MP_TAC SQRT_POS_LT);
  (ASM_REWRITE_TAC[]); 

  (SUBGOAL_THEN 
   `(-- &1 * G a' - f4 a' * G') / G a' pow 2 * inv (&1 + F42 a' pow 2) =
    (a' - b - c) / &2 / (&4 - a') / sqrt D'`
    ASSUME_TAC);
    (* Subgoal 3.21.4 *)
  (ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `sqrt D' pow 2 = D'` ASSUME_TAC);
      (* Subgoal 3.21.4.1 *)
    (MATCH_MP_TAC SQRT_POW_2);
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
    (ASM_REWRITE_TAC[]);
 
    (SUBGOAL_THEN 
      `inv (&1 + F42 (a':real) pow 2)  = D' / (D' + D4 pow 2)` ASSUME_TAC);
      (* Subgoal 3.21.4.2 *)
    (EXPAND_TAC "F42");
    (ONCE_ASM_REWRITE_TAC[]);
    (REWRITE_TAC[REAL_POW_DIV]);
    (ONCE_ASM_REWRITE_TAC[]);
    (PURE_ONCE_REWRITE_TAC[GSYM REAL_INV_DIV]);
    AP_TERM_TAC;
    (PURE_ONCE_REWRITE_TAC[REAL_INV_DIV]);
    (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
    (AP_THM_TAC THEN AP_TERM_TAC);    
    (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
    (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (&0 = a)`));
    (ASM_REWRITE_TAC[]);    

  (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC THEN DEL_TAC);
  (PURE_REWRITE_TAC[REAL_ARITH `-- &1 * x = -- x`]);
  (ABBREV_TAC `M = -- sqrt D' - D4 * G'`);

    (SUBGOAL_THEN
      `D' + D4 pow 2 = (&4 - a') * (&4 - b) * (&4 - c)` ASSUME_TAC);
      (* Subgoal 3.21.4.3 *)
    (EXPAND_TAC "D4");
    (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
    (EXPAND_TAC "f4");
    REAL_ARITH_TAC;
 
    (SUBGOAL_THEN `G' = Da * inv (&2 * sqrt D')` ASSUME_TAC);  
      (* Subgoal 3.21.4.4 *)
    (EXPAND_TAC "G'" THEN EXPAND_TAC "Da");
    (REPEAT AP_TERM_TAC);
    (ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN 
     `M = (a' - b - c) * ((&4 - b) * (&4 - c)) / &2 / sqrt D'` ASSUME_TAC);
      (* Subgoal 3.21.4.5 *)
    (EXPAND_TAC "M");
    (UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN REPEAT DISCH_TAC);
    (ONCE_ASM_REWRITE_TAC[]);
    (ABBREV_TAC `X = --sqrt D' - D4 * Da * inv (&2 * sqrt D') `);
    (REWRITE_TAC[REAL_ARITH `a * (b * c) / d / e = ((a * b * c) / d) / e`]);
    (ABBREV_TAC `Y = ((a' - b - c) * (&4 - b) * (&4 - c)) / &2`);
    (ABBREV_TAC `Z = sqrt D'`);

     (SUBGOAL_THEN `X * Z = Y ==> X = Y / Z ` ASSUME_TAC);
        (* Subgoal 3.21.4.5.1 *)
     (ASM_SIMP_TAC[REAL_EQ_RDIV_EQ]);

    (FIRST_ASSUM MATCH_MP_TAC);
    (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
    (REWRITE_TAC[REAL_SUB_RDISTRIB]);

     (SUBGOAL_THEN `--sqrt D' * sqrt D' = -- D'` ASSUME_TAC);
        (* Subgoal 3.21.4.5.2 *)
     (MATCH_MP_TAC (REAL_ARITH `a * b = c ==> -- a * b = -- c`));
     (REWRITE_TAC[GSYM REAL_POW_2]);
     (MATCH_MP_TAC SQRT_POW_2);
     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
     (ASM_REWRITE_TAC[]);

     (SUBGOAL_THEN 
        `(D4 * Da * inv (&2 * sqrt D')) * sqrt D' = D4 * Da / &2` ASSUME_TAC);
        (* Subgoal 3.21.4.5.3 *)
     (REWRITE_TAC[REAL_INV_MUL]);
     (REWRITE_TAC[REAL_ARITH 
       `(a * b * c * d) * e = (a * b * c) * (d * e)`]);
         
         (SUBGOAL_THEN `inv (sqrt D') * sqrt D' = &1 ` ASSUME_TAC);
         (MATCH_MP_TAC REAL_MUL_LINV);
         (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
         (MATCH_MP_TAC SQRT_POS_LT);
         (ASM_REWRITE_TAC[]);

     (ASM_REWRITE_TAC[REAL_MUL_RID]);
      REAL_ARITH_TAC;

    (ASM_REWRITE_TAC[]);
    (EXPAND_TAC "D'" THEN EXPAND_TAC "D4" THEN EXPAND_TAC "Da");
    (REWRITE_TAC[ups_x]);
    (EXPAND_TAC "f4");
    (REAL_ARITH_TAC);
   (* End Subgoal 3.21.4.5 *)

  (REWRITE_TAC[REAL_ARITH `a / b * c / d = (a / b * c) / d`]);

    (SUBGOAL_THEN `(M / D' * D') = M` ASSUME_TAC);
    (MATCH_MP_TAC REAL_DIV_RMUL);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ ( x = &0) `));
    (ASM_REWRITE_TAC[]);

  (ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ARITH `(a * x / b / c) / d = (a * x / d) / b / c`]);
  (AP_THM_TAC THEN AP_TERM_TAC);
  (ONCE_REWRITE_TAC[REAL_ARITH ` a/ &2 / b = a / b / &2`]);
  (AP_THM_TAC THEN AP_TERM_TAC);
  (ABBREV_TAC `S = (&4 - b) * (&4 - c)`);

        (* ----------------------------------------------------- *)
        (*       ~ ( c = &4)                                     *)
        (* ----------------------------------------------------- *)
         (SUBGOAL_THEN `~ (&4 - b = &0) /\ ~ (&4 - c = &0)` ASSUME_TAC);
          ASM_REAL_ARITH_TAC;

        (* ----------------------------------------------------- *)
        (*        ~ (a' = &4)                                     *)
        (* ----------------------------------------------------- *)

         (SUBGOAL_THEN `~ (&4 - a' = &0)` ASSUME_TAC);
         (MATCH_MP_TAC (REAL_ARITH `~ (x = &4) ==> ~ (&4 - x = &0)`));
          STRIP_TAC;
         
           (SUBGOAL_THEN ` D' = -- ((b + c - &4) pow 2)` ASSUME_TAC);
           (EXPAND_TAC "D'" );
           (REWRITE_TAC[ups_x]);
           (ONCE_ASM_REWRITE_TAC[]);
            REAL_ARITH_TAC;

           (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
           (ASM_REWRITE_TAC[REAL_ARITH `-- a <= &0 <=> &0 <= a`]);
           (MESON_TAC[REAL_LE_POW_2]);

           (MP_TAC (ASSUME `&0 < D'`));
           (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);

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

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

    (SUBGOAL_THEN `~ (S = &0)` ASSUME_TAC);
    (EXPAND_TAC "S");
    (REWRITE_TAC [REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b `]);
    (ASM_REWRITE_TAC[]);

  (ASM_MESON_TAC[REDUCE_WITH_DIV_Euler_lemma]);
    (* End of subgoal  *)
 
 (ASM_MESON_TAC[]); 
 (UP_ASM_TAC); 
 (DEL_TAC THEN UP_ASM_TAC); 
 (DEL_TAC THEN DEL_TAC THEN DEL_TAC); 
 (REPEAT DISCH_TAC);


(* ================ END DIFF 4 ============================================== *)


(* ========================================================================= *)
(*               END OF THE FIRST GOAL                                       *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(*          Subgoal 3.22                                                     *)
(* ------------------------------------------------------------------------- *)
 
 (ABBREV_TAC `FUNCTION = (\a. --pi / &2 -
       atn
       ((-- &2 * a + &2 * b + &2 * c - b * c) /
        (&2 * sqrt (ups_x a b c - a * b * c))) -
       atn
       ((-- &2 * b + &2 * c + &2 * a - c * a) /
        (&2 * sqrt (ups_x a b c - a * b * c))) -
       atn
       ((-- &2 * c + &2 * a + &2 * b - a * b) /
        (&2 * sqrt (ups_x a b c - a * b * c))) +
       &2 * atn ((&8 - a - b - c) / sqrt (ups_x a b c - a * b * c)))`);

  (SUBGOAL_THEN 
    `FUNCTION = (\(a:real). --pi / &2 - F1 a - F2 a - F3 a + &2 * F4 a)`
     ASSUME_TAC);
  (EXPAND_TAC "FUNCTION");
  (EXPAND_TAC "F1" THEN EXPAND_TAC "F2");
  (EXPAND_TAC "F3" THEN EXPAND_TAC "F4");
  (REWRITE_TAC[]); 
 
 (ABBREV_TAC `F1' = -- &1 / sqrt D'`); 
 (ABBREV_TAC `F2' = 
  (-- &2 * c + &2 * a' + &2 * b - a' * b) / (a' * (&4 - a')) / sqrt D'`); 
 (ABBREV_TAC `F3' = 
  (-- &2 * b + &2 * a' + &2 * c - a' * c) / (a' * (&4 - a')) / sqrt D'`); 
 (ABBREV_TAC `F4' = (a' - b - c) / &2 / (&4 - a') / sqrt D'`);

(* ------------------------------------------------------------------------- *)
(*          Subgoal 3.23                                                     *)
(* ------------------------------------------------------------------------- *)

  (SUBGOAL_THEN ` &0 - F1' - F2' - F3' + &2 * F4' = &0` ASSUME_TAC);
  (EXPAND_TAC "F1'" THEN EXPAND_TAC "F2'");
  (EXPAND_TAC "F3'" THEN EXPAND_TAC "F4'");
  (REWRITE_TAC[REAL_ARITH `&0 - a - b - c + d = &0 <=> a + b + c = d `]);
  (REWRITE_TAC[REAL_ARITH `a / x + b / x = (a + b) / x`]);
  (REWRITE_TAC[REAL_ARITH `a * b / c / d / e  = ((a * b / c) / d) / e`]);
  (AP_THM_TAC THEN AP_TERM_TAC);
  (REWRITE_TAC[REAL_ARITH 
      `(-- &2 * c + &2 * a' + &2 * b - a' * b) + 
        -- &2 * b + &2 * a' + &2 * c - a' * c = 
        a' * (&4 - b - c)`]);

    (* --------------------------------------------------------------- *)
    (*       ~ ( a' = &4) /\ ~ (a' = &0)                               *)
    (* --------------------------------------------------------------- *)

    (SUBGOAL_THEN `~ (&4 - a' = &0) /\ ~ (a' = &0)` ASSUME_TAC);
    (REWRITE_TAC[REAL_ARITH `~ (&4 - a' = &0) <=> ~ (a' = &4)`]);
    (REPEAT STRIP_TAC);  (* 2 Subgoals *)

     (SUBGOAL_THEN ` D' = -- ((c + b - &4) pow 2)` ASSUME_TAC);
     (EXPAND_TAC "D'" );
     (REWRITE_TAC[ups_x]);
     (ONCE_ASM_REWRITE_TAC[]);
      REAL_ARITH_TAC;
     (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
     (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
     (MESON_TAC[REAL_LE_POW_2]);
     (MP_TAC (ASSUME `&0 < D'`));
     (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);

     (SUBGOAL_THEN ` D' = -- ((c - b) pow 2)` ASSUME_TAC);
     (EXPAND_TAC "D'" );
     (REWRITE_TAC[ups_x]);
     (ONCE_ASM_REWRITE_TAC[]);
      REAL_ARITH_TAC;
     (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
     (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
     (MESON_TAC[REAL_LE_POW_2]);
     (MP_TAC (ASSUME `&0 < D'`));
     (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);

    (SUBGOAL_THEN `~ (a' * (&4 - a') = &0)` ASSUME_TAC);
    (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
    (ASM_REWRITE_TAC[]);

  (REWRITE_TAC[REAL_ARITH `&2 * x / &2 = x`]);

    (SUBGOAL_THEN `-- &1 = -- (&4 - a') / (&4 - a')` ASSUME_TAC);
    (MATCH_MP_TAC (REAL_ARITH `(a = b/c) ==> (-- a = -- b/c)`));
    (ASM_SIMP_TAC[REAL_DIV_REFL]);
  
  (ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ARITH `(-- x /y + z = t / y) <=> (z = (t + x) / y)`]);
  (REWRITE_TAC[REAL_ARITH `a - x - y + z - a = z - x - y`]);
  (REWRITE_TAC[REAL_ARITH `(x * y) / (x * z) = y * x / (z * x)`]); 
  (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
  (ASM_REWRITE_TAC[]);
 
 (UP_ASM_TAC THEN REPLICATE_TAC 4 DEL_TAC); 
 (REPLICATE_TAC 5 (UP_ASM_TAC THEN DEL_TAC)); 
 (REPEAT DISCH_TAC);

(* ------------------------------------------------------------------------- *)
(*          Subgoal 3.24                                                     *)
(* ------------------------------------------------------------------------- *)
 
 (ABBREV_TAC `FUNC1 = (\(a:real). F1 a + F2 a + F3 a)`); 
 (ABBREV_TAC `FUNC2 = (\(a:real). --pi / &2 + &2 * F4 a)`);

  (SUBGOAL_THEN 
     `(FUNC1 has_real_derivative F1' + F2' + F3') (atreal a' within s)`
     ASSUME_TAC);
  (ABBREV_TAC `X = (\(a:real). F2 a + F3 a)`);
  (ABBREV_TAC `X' = F2' + F3'`);

    (SUBGOAL_THEN 
      `(X has_real_derivative X') (atreal a' within s)` ASSUME_TAC);
      (* Subgoal 3.24.1 *)  
    (EXPAND_TAC "X" THEN EXPAND_TAC "X'");
    (ASM_SIMP_TAC[HAS_REAL_DERIVATIVE_ADD]);

    (SUBGOAL_THEN `FUNC1 = (\(a:real). F1 a + X a)` ASSUME_TAC);
      (* Subgoal 3.24.2 *)  
    (EXPAND_TAC "X");
    (ASM_REWRITE_TAC[]);

    (ASM_REWRITE_TAC[]);
    (ASM_SIMP_TAC[HAS_REAL_DERIVATIVE_ADD]);

(* ------------------------------------------------------------------------- *)
(*          Subgoal 3.25                                                     *)
(* ------------------------------------------------------------------------- *)

  (SUBGOAL_THEN 
    `(FUNC2 has_real_derivative &0 + &2 * F4') (atreal a' within s)`
     ASSUME_TAC);
  (ABBREV_TAC `X = (\(a:real). -- pi / &2)`);
  (ABBREV_TAC `Y = (\(a:real). &2 * F4 a)`);

    (SUBGOAL_THEN 
     `(X has_real_derivative &0) (atreal a' within s)` ASSUME_TAC);
      (* Subgoal 3.25.1 *)  
    (EXPAND_TAC "X");
    (REAL_DIFF_TAC);
    (REWRITE_TAC[]);

    (SUBGOAL_THEN 
      `(Y has_real_derivative &2 * F4') (atreal a' within s)` ASSUME_TAC);
      (* Subgoal 3.25.2 *)  
    (EXPAND_TAC "Y");
    (MATCH_MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN);
    (ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `FUNC2 = (\(a:real). X a + Y a)` ASSUME_TAC);
      (* Subgoal 3.25.3 *)  
    (EXPAND_TAC "X" THEN EXPAND_TAC "Y");
    (ASM_REWRITE_TAC[]);

  (ASM_REWRITE_TAC[]);
  (ASM_SIMP_TAC[HAS_REAL_DERIVATIVE_ADD]);

(* ------------------------------------------------------------------------- *)
(*          Subgoal 3.26                                                     *)
(* ------------------------------------------------------------------------- *)

  (SUBGOAL_THEN `FUNCTION = (\(a:real). FUNC2 a - FUNC1 a)` ASSUME_TAC);
  (EXPAND_TAC "FUNC1" THEN EXPAND_TAC "FUNC2");
  (REWRITE_TAC[REAL_ARITH `(a + b) - (c + d + e) = a - c - d - e + b`]);
  (ASM_REWRITE_TAC[]);

(* ------------------------------------------------------------------------- *)
(*          Subgoal 3.27                                                     *)
(* ------------------------------------------------------------------------- *)

  (SUBGOAL_THEN 
   `(FUNCTION has_real_derivative &0 - F1' - F2' - F3' + &2 * F4')
    (atreal a' within s)`
    ASSUME_TAC);
  (REWRITE_TAC[REAL_ARITH `a - c - d - e + b = (a + b) - (c + d + e)`]);
  (ASM_MESON_TAC[HAS_REAL_DERIVATIVE_SUB]);
 
 (ASM_MESON_TAC[]);


(* ========================================================================= *)
(*                                                                           *)
(*                 FINISH COMPUTE FIRST DERIVATIVES                          *)
(*                                                                           *)
(* ========================================================================= *)


(* ------------------------------------------------------------------------- *)
(*       SUBGOAL 4.1                                                         *)
(*       ~ ( c = &4) /\ ~ (c = &0)                                           *)
(* ------------------------------------------------------------------------- *)

  (SUBGOAL_THEN `~ (c = &4) /\ ~ (c = &0)` ASSUME_TAC);
  ASM_REAL_ARITH_TAC;

(* ------------------------------------------------------------------------- *)
(*       SUBGOAL 4.2                                                         *)
(*                     Reduce the expression                                 *)
(* ------------------------------------------------------------------------- *)
 
 (PURE_REWRITE_TAC[REAL_ARITH 
  `&8 - (b + c - (b * c) / &2) - b - c = 
   &8 + (b * c) / &2 - &2 * b  - &2 * c`]); 
 (PURE_REWRITE_TAC[REAL_ARITH 
    `-- &2 * (b + c - (b * c) / &2) + &2 * b + &2 * c - b * c = &0 `]); 
 (REWRITE_TAC[REAL_ARITH `&0 * x = &0 /\ &0 / x = &0`; 
               ATN_0; REAL_ARITH `a - &0 = a`]); 
 (PURE_REWRITE_TAC[REAL_ARITH 
  `-- &2 * b + &2 * c + &2 * (b + c - (b * c) / &2) - 
   c * (b + c - (b * c) / &2) = 
  (&1 - b / &2) * (&4 - c) * c `]); 
 (PURE_REWRITE_TAC[REAL_ARITH 
  `-- &2 * c + &2 * (b + c - (b * c) / &2) + 
   &2 * b - (b + c - (b * c) / &2) * b = 
   (&1 - c / &2) * (&4 - b) * b`]); 
 (PURE_REWRITE_TAC[ups_x]); 
 (PURE_REWRITE_TAC[REAL_ARITH 
   `(--(b + c - (b * c) / &2) * (b + c - (b * c) / &2) - b * b - c * c +
    &2 * (b + c - (b * c) / &2) * c +
    &2 * (b + c - (b * c) / &2) * b +
    &2 * b * c) -
    (b + c - (b * c) / &2) * b * c = 
   (((&4 - b) * b) * (&4 - c) * c) / &4`]);
 

(* ------------------------------------------------------------------------- *)
(*       SUBGOAL 4.                                                           *)
(*                                                                            *)
(* ------------------------------------------------------------------------- *)

 
 (SUBGOAL_THEN 
  `!r b. c IN r /\
     is_realinterval r /\
     b IN r /\
     (!y. y IN r ==> &0 < ((&4 - y) * y) * (&4 - c) * c)
     ==> --pi / &2 -
         atn
         (((&1 - b / &2) * (&4 - c) * c) /
          (&2 * sqrt ((((&4 - b) * b) * (&4 - c) * c) / &4))) -
         atn
         (((&1 - c / &2) * (&4 - b) * b) /
          (&2 * sqrt ((((&4 - b) * b) * (&4 - c) * c) / &4))) +
         &2 *
         atn
         ((&8 + (b * c) / &2 - &2 * b - &2 * c) /
          sqrt ((((&4 - b) * b) * (&4 - c) * c) / &4)) =
         &0`
 ASSUME_TAC);
 
 (REPEAT GEN_TAC  THEN STRIP_TAC);
 SWITCH_TAC; 
 (FIRST_X_ASSUM MP_TAC THEN SPEC_TAC (`b':real`, `x:real`) ); 
 (MATCH_MP_TAC HAS_REAL_DERIVATIVE_ZERO_CONSTANT2 THEN EXISTS_TAC `c:real`); 
 (ASM_REWRITE_TAC[]); 
 STRIP_TAC;  (* Break into 2 Subgoals *)
 
  (* The first one *)
  (ABBREV_TAC `C = (&4 - c) * c`);
  (ABBREV_TAC 
     `FUNCTION = (\x. --pi / &2 -
           atn
           (((&1 - x / &2) * C) / (&2 * sqrt ((((&4 - x) * x) * C) / &4))) -
           atn
           (((&1 - c / &2) * (&4 - x) * x) /
            (&2 * sqrt ((((&4 - x) * x) * C) / &4))) +
           &2 *
           atn
           ((&8 + (x * c) / &2 - &2 * x - &2 * c) /
            sqrt ((((&4 - x) * x) * C) / &4)))`);
  (ABBREV_TAC 
    `F1 = (\x. atn 
    (((&1 - x / &2) * C) / (&2 * sqrt ((((&4 - x) * x) * C) / &4))))`);
  (ABBREV_TAC 
    `F2 = (\x. atn
           (((&1 - c / &2) * (&4 - x) * x) / 
            (&2 * sqrt ((((&4 - x) * x) * C) / &4))))`);
  (ABBREV_TAC 
    `F3 = (\x. atn
           ((&8 + (x * c) / &2 - &2 * x - &2 * c) /
            sqrt ((((&4 - x) * x) * C) / &4)))`);

  (SUBGOAL_THEN 
    `FUNCTION = (\(x:real). --pi / &2 - F1 x - F2 x + &2 * F3 x)`
     ASSUME_TAC);
  (EXPAND_TAC "F1" THEN EXPAND_TAC "F2" THEN EXPAND_TAC "F3");
  (EXPAND_TAC "FUNCTION");
  (REWRITE_TAC[]);
 
 (GEN_TAC THEN DISCH_TAC);


(* ------------------------------------------------------------------------- *)
(*       SUBGOAL 4.                                                           *)
(*                                                                            *)
(* ------------------------------------------------------------------------- *)
 
 (ABBREV_TAC `D' = (((&4 - x) * x) * C) / &4`);
  (SUBGOAL_THEN `&0 < D'` ASSUME_TAC);
    (* Subgoal *) 
  (EXPAND_TAC "D'" THEN DEL_TAC);
  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 < a / &4`));
   UP_ASM_TAC;
  (ASM_MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*         Derivativ of sqrt ((((&4 - x) * x) * C) / &4)                *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `G = (\x.  sqrt ((((&4 - x) * x) * C) / &4))`); 
 (ABBREV_TAC `G' = 
  (((&4 - &2 * x) * C) / &4) * inv (&2 * sqrt ((((&4 - x) * x) * C) / &4))`);
  
  (SUBGOAL_THEN `(G has_real_derivative G') (atreal x within r)` ASSUME_TAC);
    (* Subgoal *)

  (ABBREV_TAC `f = (\x. (((&4 - x) * x) * C) / &4)`);

    (SUBGOAL_THEN `G = (\x:real. sqrt (f x))` ASSUME_TAC);
      (* Subgoal *)
    (EXPAND_TAC "f" THEN ASM_REWRITE_TAC[]);

  (ABBREV_TAC `g' = (\x. inv (&2 * sqrt x))`);
  (ABBREV_TAC `f' = ((&4 - &2 * x) * C)/ &4 `);
  (ABBREV_TAC `P = {x:real | &0 < x}`);

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

    (SUBGOAL_THEN 
       `(f has_real_derivative f') (atreal x within r) /\ 
        (P:real->bool) (f x)` ASSUME_TAC);
      (* Subgoal *)

      CONJ_TAC;   
       (EXPAND_TAC "f" THEN EXPAND_TAC "f'");
       (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
       (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
       (EXPAND_TAC "f");
       (ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `G' = f' * (g' ((f:real->real) x))` ASSUME_TAC);
      (* Subgoal *)
    (EXPAND_TAC "G'" THEN EXPAND_TAC "f'");
    (EXPAND_TAC "g'" THEN EXPAND_TAC "f" );
    (REWRITE_TAC[]);
    
  (ONCE_ASM_REWRITE_TAC[]);
  (DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2 THEN MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*         Derivative of &2 * sqrt ((((&4 - x) * x) * C) / &4)           *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `2G = (\x.  &2 * sqrt ((((&4 - x) * x) * C) / &4))`);
  (SUBGOAL_THEN 
    `(2G has_real_derivative &2 * G') (atreal x within r)` ASSUME_TAC);
  
    (SUBGOAL_THEN `2G = (\x:real. &2 * G x)` ASSUME_TAC);
    (EXPAND_TAC "2G" THEN EXPAND_TAC "G" THEN MESON_TAC[]); 
  
  (ONCE_ASM_REWRITE_TAC[]);
  (DEL_TAC THEN DEL_TAC );
  (FIRST_X_ASSUM MP_TAC);
  (MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN THEN MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*         Derivative of  ((&1 - x / &2) * C) /                          *)
(*            (&2 * sqrt ((((&4 - x) * x) * C) / &4))                    *)  
(* --------------------------------------------------------------------------*)
 
 (ABBREV_TAC `f1 = (\x. (&1 - x / &2) * C)`); 
 (ABBREV_TAC `F12 = 
  (\x. ((&1 - x / &2) * C) / (&2 * sqrt ((((&4 - x) * x) * C) / &4)))`);

  (SUBGOAL_THEN 
    `(F12 has_real_derivative
     ((-- &1 / &2 * C) * 2G x - f1 x * &2 * G') / 2G x pow 2)
     (atreal x within r)`
     ASSUME_TAC);

    (SUBGOAL_THEN `F12 = (\x:real.  f1 x / 2G x)` ASSUME_TAC);
      (* Subgoal *) 
    (EXPAND_TAC "F12" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f1");
    (REWRITE_TAC[]);

  (ASM_REWRITE_TAC[] THEN DEL_TAC);

    (SUBGOAL_THEN 
      `(f1 has_real_derivative (-- &1 / &2) * C) (atreal x within r) /\ 
       (2G has_real_derivative &2 * G') (atreal x within r) /\ ~(2G x = &0)`
       ASSUME_TAC);
      (*  Subgoal *)
    (ASM_REWRITE_TAC[]);    
     CONJ_TAC;  (* Break into 2 subgoals *)

      (EXPAND_TAC "f1" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
      (EXPAND_TAC "2G");
      (MATCH_MP_TAC (MESON[REAL_ENTIRE] 
         `~ (x = &0) /\ ~ (y = &0) ==> ~ (x * y = &0)`));
      (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
      (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
      (MATCH_MP_TAC SQRT_POS_LT);
      (ASM_REWRITE_TAC[]);

   UP_ASM_TAC;
   (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
   (MESON_TAC[]);

(* --------------------------------------------------------------------------*)
(*         Derivative of  atn ((&1 - x / &2) * C) /                      *)
(*            (&2 * sqrt ((((&4 - x) * x) * C) / &4))                    *)  
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN 
    `(F1 has_real_derivative
     ((-- &1 / &2 * C) * 2G x - f1 x * &2 * G') / 2G x pow 2 *
     inv (&1 + F12 x pow 2))
     (atreal x within r)`
     ASSUME_TAC);

    (SUBGOAL_THEN `F1 = (\x:real. atn (F12 x))` ASSUME_TAC);
      (* Subgoal *)
    (EXPAND_TAC "F1" THEN EXPAND_TAC "F12");
    (REWRITE_TAC[]); 

  (ONCE_ASM_REWRITE_TAC[]);
   DEL_TAC;
  (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
  (ABBREV_TAC `f' = 
    ((-- &1 / &2 * C) * 2G (x:real) - f1 x * &2 * G') / 2G x pow 2`);

    (SUBGOAL_THEN 
      `inv (&1 + F12 x pow 2) = g' ((F12:real-> real) x)`
       ASSUME_TAC);
      (* Subgoal *)
    (EXPAND_TAC "F12" THEN EXPAND_TAC "g'");
    (REWRITE_TAC[]);
 
  (ONCE_ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN 
     `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
      ASSUME_TAC);   
      (* Subgoal *)
    (EXPAND_TAC "g'");
    (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);


    (SUBGOAL_THEN 
      `(F12 has_real_derivative f') (atreal x within r) /\ 
       (:real) (F12 x)` ASSUME_TAC);
      (* Subgoal *)
    (ASM_REWRITE_TAC[]);
    (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);

  (REPLICATE_TAC 2 UP_ASM_TAC);
  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
  (MESON_TAC[]);

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

  (ABBREV_TAC `X = (&4 - x) * x`);
  (SUBGOAL_THEN `~(X = &0)` ASSUME_TAC);
   STRIP_TAC;
    (SUBGOAL_THEN `D' = &0` ASSUME_TAC);
    (EXPAND_TAC "D'");
    (REWRITE_TAC[REAL_ARITH `(a * x)/ &4 = a * (x / &4)`]);
    (ONCE_ASM_REWRITE_TAC[]);
     REAL_ARITH_TAC;
  (MP_TAC (ASSUME `&0 < D'`));
  (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);

  (SUBGOAL_THEN `~(&4 - x = &0) /\ ~(x = &0)` ASSUME_TAC);
  (UP_ASM_TAC THEN EXPAND_TAC "X");
  (REWRITE_TAC[REAL_ENTIRE]);
  (MESON_TAC[]);

  (SUBGOAL_THEN 
    `inv (&1 + F12 (x:real) pow 2) = X / (X + C - X * C / &4)`
     ASSUME_TAC);
  (ONCE_REWRITE_TAC[GSYM REAL_INV_DIV]);
   AP_TERM_TAC;
  (REWRITE_TAC[REAL_ARITH `(a + b)/ c = a / c + b / c`]);
    
    (SUBGOAL_THEN `X / X = &1` ASSUME_TAC);
    (ASM_SIMP_TAC[REAL_DIV_REFL]);
 
  (ONCE_ASM_REWRITE_TAC[]); 
  (AP_TERM_TAC);
  (EXPAND_TAC "F12");
  (REWRITE_TAC[REAL_POW_DIV]);
  (REWRITE_TAC[REAL_POW_2]);
  (REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * a = &4 * a pow 2`]);
  (ONCE_ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `sqrt ((X * C) / &4) pow 2 = (X * C) / &4` ASSUME_TAC);
    (MATCH_MP_TAC SQRT_POW_2);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
    (ASM_REWRITE_TAC[]);
 
  (ONCE_ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ARITH `&4 * (X * C) / & 4 = X * C`]);
  (REWRITE_TAC[REAL_ARITH 
    `((&1 - x / &2) * C) * (&1 - x / &2) * C = 
     ((&1 - ((&4 - x) * x) / &4) * C) * C`]);
  (ONCE_ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN `~(C = &0)` ASSUME_TAC);
   STRIP_TAC;
    (SUBGOAL_THEN `D' = &0` ASSUME_TAC);
    (EXPAND_TAC "D'");
    (REWRITE_TAC[REAL_ARITH `(a * x)/ &4 = (a / &4) * x`]);
    (ONCE_ASM_REWRITE_TAC[]);
     REAL_ARITH_TAC;
  (MP_TAC (ASSUME `&0 < D'`));
  (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);

    (SUBGOAL_THEN 
      `(((&1 - X / &4) * C) * C) / (X * C) = ((&1 - X / &4) * C) / X`
      ASSUME_TAC);
    (ONCE_REWRITE_TAC[REAL_ARITH `((a * b) * c) / d = (a * b) * c / d`]);
    (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
    (ASM_REWRITE_TAC[]);

  (ONCE_ASM_REWRITE_TAC[]);
  (AP_THM_TAC THEN AP_TERM_TAC);
   REAL_ARITH_TAC;

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

(SUBGOAL_THEN `&2 * sqrt ((X * C) / &4) = sqrt (X * C)` ASSUME_TAC);
(MATCH_MP_TAC (REAL_ARITH 
    `(&2 * sqrt x = sqrt (&4) * sqrt x) /\ (sqrt (&4) * sqrt x = y)
      ==> &2 * sqrt x = y`));
(ASM_REWRITE_TAC[]);
 CONJ_TAC;

  (AP_THM_TAC THEN AP_TERM_TAC);
  (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`]);
  (SIMP_TAC[REAL_ARITH `&0 <= &2`; SQRT_MUL]);
  (SIMP_TAC[GSYM REAL_POW_2; GSYM SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
  
  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `X * C = &4 * (X * C) / &4`]);
  (ASM_REWRITE_TAC[]);
  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&4 * (a * b) / &4 = a * b`]);
  (MATCH_MP_TAC (GSYM SQRT_MUL));
  (REWRITE_TAC[REAL_ARITH `&0 <= &4`]);
  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
  (ASM_REWRITE_TAC[]);

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

  (SUBGOAL_THEN `2G (x:real) = sqrt (X * C)` ASSUME_TAC);  
  (EXPAND_TAC "2G");
  (ONCE_ASM_REWRITE_TAC[]);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `G' = ((&4 - &2 * x) * C) / &4 * inv (sqrt (X * C))` ASSUME_TAC);
  (EXPAND_TAC "G'");
  (REPEAT AP_TERM_TAC);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN `&0 < X * C` ASSUME_TAC);
  (EXPAND_TAC "X" THEN ASM_MESON_TAC[]);

  (SUBGOAL_THEN 
    `(-- &1 / &2 * C) * 2G (x:real) - f1 x * &2 * G' = 
      -- &2 * C * C / sqrt (X * C)` ASSUME_TAC);
  (ONCE_ASM_REWRITE_TAC[]);
  (EXPAND_TAC "f1");
  (ONCE_REWRITE_TAC[REAL_ARITH 
    `a * &2 * b / &4 * c = (a * &2 * b / &4) * c`]);
  (ONCE_REWRITE_TAC[REAL_ARITH 
    `((&1 - x / &2) * C) * &2 * ((&4 - &2 * x) * C) / &4 = 
     (&4 - (&4 - x) * x) * C * C / &2`]);
  (ONCE_ASM_REWRITE_TAC[]);    

  (SUBGOAL_THEN 
    `(-- &1 / &2 * C) * sqrt (X * C) = (-- &1 / &2 * C * X * C) / sqrt (X * C)`
     ASSUME_TAC);
  (REWRITE_TAC[REAL_ARITH 
    `(-- &1 / &2 * C * X * C) / Y = (-- &1 / &2 * C) * (X * C) / Y `]);
   AP_TERM_TAC;


    (SUBGOAL_THEN 
      `sqrt (X * C) * sqrt (X * C) = (X * C) ==> 
       sqrt (X * C) = (X * C) / sqrt (X * C)` ASSUME_TAC);
    (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
    (MATCH_MP_TAC (GSYM REAL_EQ_RDIV_EQ));
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);    

  (FIRST_X_ASSUM MATCH_MP_TAC); 
  (REWRITE_TAC[GSYM REAL_POW_2]);
  (MATCH_MP_TAC SQRT_POW_2);
  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
  (ASM_REWRITE_TAC[]);

 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[REAL_ARITH `-- a *  b * c / x = -- (a * b * c) / x`]);
 (REWRITE_TAC[REAL_ARITH `a / x - y = -- b / x <=> (a + b) / x = y`]);
 (REWRITE_TAC[REAL_ARITH 
   `-- &1 / &2 * C * X * C + &2 * C * C = (&4 - X) * C * C / &2`]);
 (ABBREV_TAC `m = (&4 - X) * C * C / &2`);
 (ABBREV_TAC `n = sqrt (X * C)`);

    (SUBGOAL_THEN `m = (m * inv n) * n  ==> m / n = m * inv n` ASSUME_TAC);
    (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
    (MATCH_MP_TAC (GSYM REAL_EQ_LDIV_EQ));
    (EXPAND_TAC "n");
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);    

  (FIRST_X_ASSUM MATCH_MP_TAC); 
  (REWRITE_TAC[REAL_ARITH `(m * inv n) * n = m * (inv n * n)`]);
  (MATCH_MP_TAC (MESON[REAL_MUL_RID] 
                  `inv n * n = &1 ==> m = m * inv n * n`));
  (MATCH_MP_TAC REAL_MUL_LINV);
  (MATCH_MP_TAC (REAL_ARITH `&0 < n ==> ~ (n = &0)`));
  (EXPAND_TAC "n");
  (MATCH_MP_TAC SQRT_POS_LT);
  (ASM_REWRITE_TAC[]);    

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

(SUBGOAL_THEN 
 `(F1 has_real_derivative -- &2 * C / (X + C - X * C / &4) / sqrt (X * C)) 
  (atreal x within r)`
  ASSUME_TAC);

  (SUBGOAL_THEN `2G (x:real) pow 2 = X * C` ASSUME_TAC);
  (MATCH_MP_TAC (REAL_ARITH 
    `2G (x:real) pow 2 = &4 * D' /\ &4 * D' = X * C ==> 
     2G (x:real) pow 2 = X * C`));
  (ASM_REWRITE_TAC[REAL_ARITH `(&4 * z = x * y) <=> ((x * y) / &4 = z)`]);  
  (EXPAND_TAC "D'");  
  (REWRITE_TAC[REAL_ARITH `&4 * (X * C) / &4 = X * C`]);
  (MATCH_MP_TAC SQRT_POW_2);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `((-- &1 / &2 * C) * 2G (x:real) - f1 x * &2 * G') / 2G x pow 2 *
     inv (&1 + F12 x pow 2) = 
     -- &2 * C / (X + C - X * C / &4) / sqrt (X * C)`
     ASSUME_TAC);
  (ASM_REWRITE_TAC[]);
  (ABBREV_TAC `m = X + C - X * C / &4`);
  (REWRITE_TAC[REAL_ARITH `-- &2 * C / m / n = (-- &2 * C) / m / n`]);  
  (REWRITE_TAC[REAL_ARITH 
    `(-- a * b * c / d) / e * f / g = (-- a * b * c * f) / e / g / d`]);
  (REPEAT (AP_THM_TAC THEN AP_TERM_TAC));
  (REWRITE_TAC[REAL_ARITH 
    `(-- a * b * c * d) / e = (-- a * b) * (d * c) / e`]);
  (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> (y * x = y)`));
  (MATCH_MP_TAC REAL_DIV_REFL);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
  (ASM_REWRITE_TAC[]);  

(ASM_MESON_TAC[]);

(UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN REPLICATE_TAC 4 DEL_TAC);
(REPLICATE_TAC 3 UP_ASM_TAC THEN REPLICATE_TAC 4 DEL_TAC);
(REPEAT DISCH_TAC);

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

(ABBREV_TAC `f2 = (\x. (&1 - c / &2) * (&4 - x) * x)`);
(ABBREV_TAC 
   `F22 = (\x. ((&1 - c / &2) * (&4 - x) * x) / 
          (&2 * sqrt ((((&4 - x) * x) * C) / &4)))`);

  (SUBGOAL_THEN 
    `(F22 has_real_derivative
     (((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G') / 2G x pow 2)
     (atreal x within r)`
     ASSUME_TAC);

    (SUBGOAL_THEN `F22 = (\x:real.  f2 x / 2G x)` ASSUME_TAC);
      (* Subgoal *) 
    (EXPAND_TAC "F22" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f2");
    (REWRITE_TAC[]);

  (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);

    (SUBGOAL_THEN 
      `(f2 has_real_derivative (&1 - c / &2) * (&4 - &2 * x)) 
       (atreal x within r) /\ 
       (2G has_real_derivative &2 * G') (atreal x within r) /\ ~(2G x = &0)`
       ASSUME_TAC);
      (*  Subgoal *)
    (ASM_REWRITE_TAC[]);    
     CONJ_TAC;  (* Break into 2 subgoals *)

      (EXPAND_TAC "f2" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
      (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
      (EXPAND_TAC "2G");
      (MATCH_MP_TAC (REAL_ARITH `&0 < &2 /\ &0 < x ==> &0 < &2 * x`));
      (REWRITE_TAC[REAL_ARITH `&0 < &2`]);
      (MATCH_MP_TAC SQRT_POS_LT);
      (MATCH_MP_TAC (REAL_ARITH `&0 < x  ==> &0 < x / &4`));
      (ASM_REWRITE_TAC[]);

   UP_ASM_TAC;
  (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
  (MESON_TAC[]);


(* --------------------------------------------------------------------------*)
(*         Derivative of  atn ((&1 - c / &2) * (&4 - x) * x) /               *)
(*            (&2 * sqrt ((((&4 - x) * x) * C) / &4))                        *)  
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN 
    `(F2 has_real_derivative
     (((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G') / 2G x pow 2 *
     inv (&1 + F22 x pow 2))
     (atreal x within r)`
     ASSUME_TAC);

    (SUBGOAL_THEN `F2 = (\x:real. atn (F22 x))` ASSUME_TAC);
      (* Subgoal *)
    (EXPAND_TAC "F2" THEN EXPAND_TAC "F22");
    (REWRITE_TAC[]); 

  (ONCE_ASM_REWRITE_TAC[]);
   DEL_TAC;
  (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
  (ABBREV_TAC `f' = 
    (((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G') / 2G x pow 2`);

    (SUBGOAL_THEN 
      `inv (&1 + F22 x pow 2) = g' ((F22:real-> real) x)`
       ASSUME_TAC);
      (* Subgoal *)
    (EXPAND_TAC "F22" THEN EXPAND_TAC "g'");
    (MESON_TAC[]);
 
  (ONCE_ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN 
     `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
      ASSUME_TAC);   
      (* Subgoal *)
    (EXPAND_TAC "g'");
    (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);


    (SUBGOAL_THEN 
      `(F22 has_real_derivative f') (atreal x within r) /\ 
       (:real) (F22 x)` ASSUME_TAC);
      (* Subgoal *)
    (ASM_REWRITE_TAC[]);
    (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);

  (REPLICATE_TAC 2 UP_ASM_TAC);
  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
  (MESON_TAC[]);

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

  (SUBGOAL_THEN 
    `inv (&1 + F22 (x:real) pow 2) = C / (X + C - X * C / &4)`
     ASSUME_TAC);
  (ONCE_REWRITE_TAC[GSYM REAL_INV_DIV]);
   AP_TERM_TAC;
  (REWRITE_TAC[REAL_ARITH `(a + b - d)/ c = b / c + (a - d) / c`]);

    (SUBGOAL_THEN `C / C = &1` ASSUME_TAC);
    (MATCH_MP_TAC REAL_DIV_REFL);
    (EXPAND_TAC "C");
    (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=> ~a /\ ~b`]);
    (ASM_REWRITE_TAC[REAL_ARITH `~ (&4 - x = &0) <=> ~(x = &4)`]);
 
  (ONCE_ASM_REWRITE_TAC[]); 
  (AP_TERM_TAC);
  (EXPAND_TAC "F22");
  (REWRITE_TAC[REAL_POW_DIV]);
  (REWRITE_TAC[REAL_POW_2]);
  (REWRITE_TAC[REAL_ARITH `(x * a) * x * a = x pow 2 * a pow 2`]);
  (ONCE_ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `sqrt ((X * C) / &4) pow 2 = (X * C) / &4` ASSUME_TAC);
    (MATCH_MP_TAC SQRT_POW_2);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
    (ASM_REWRITE_TAC[]);
 
  (ONCE_ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ARITH `&2 pow 2 * (X * C) / & 4 = X * C`]);

    (SUBGOAL_THEN 
      `((&1 - c / &2) pow 2 * X pow 2) / (X * C) = 
       ((&1 - C / &4) * X) * X / (C * X)` ASSUME_TAC);    
    (EXPAND_TAC "C");
    (REWRITE_TAC[REAL_ARITH 
                  `(&1 - c / &2) pow 2 = &1 - ((&4 - c) * c) / &4`]);
    (REWRITE_TAC[REAL_ARITH `a * b pow 2 = (a * b) * b`]);
    (ONCE_REWRITE_TAC[REAL_ARITH `((a * d) * b) / c = (a * d) * (b / c)`]);
    (REPEAT AP_TERM_TAC);
    (REWRITE_TAC[REAL_MUL_SYM]);

  (ONCE_ASM_REWRITE_TAC[]);   
  (REWRITE_TAC[REAL_ARITH `(a - a * b) / c = ((&1 - b) * a) / c`]);
  (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
  (ASM_REWRITE_TAC[]);
  (EXPAND_TAC "C");
  (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=> ~a /\ ~b`]);
  (ASM_REWRITE_TAC[REAL_ARITH `~ (&4 - x = &0) <=> ~(x = &4)`]);

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

(SUBGOAL_THEN `&2 * sqrt ((X * C) / &4) = sqrt (X * C)` ASSUME_TAC);
(MATCH_MP_TAC (REAL_ARITH 
    `(&2 * sqrt x = sqrt (&4) * sqrt x) /\ (sqrt (&4) * sqrt x = y)
      ==> &2 * sqrt x = y`));
(ASM_REWRITE_TAC[]);
 CONJ_TAC;

  (AP_THM_TAC THEN AP_TERM_TAC);
  (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`]);
  (SIMP_TAC[REAL_ARITH `&0 <= &2`; SQRT_MUL]);
  (SIMP_TAC[GSYM REAL_POW_2; GSYM SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
  
  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `X * C = &4 * (X * C) / &4`]);
  (ASM_REWRITE_TAC[]);
  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&4 * (a * b) / &4 = a * b`]);
  (MATCH_MP_TAC (GSYM SQRT_MUL));
  (REWRITE_TAC[REAL_ARITH `&0 <= &4`]);
  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
  (ASM_REWRITE_TAC[]);

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

  (SUBGOAL_THEN `2G (x:real) = sqrt (X * C)` ASSUME_TAC);  
  (EXPAND_TAC "2G");
  (ONCE_ASM_REWRITE_TAC[]);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `G' = ((&4 - &2 * x) * C) / &4 * inv (sqrt (X * C))` ASSUME_TAC);
  (EXPAND_TAC "G'");
  (REPEAT AP_TERM_TAC);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G' = 
     ((&1 - c / &2) * (&4 - &2 * x)) * (X * C) / &2 / sqrt (X * C)`
      ASSUME_TAC);

  (ONCE_ASM_REWRITE_TAC[]);
  (EXPAND_TAC "f2");
  (ONCE_REWRITE_TAC[REAL_ARITH 
    `(a * b) * &2 * (c * d) / &4 * e = (a * c) * (b * d * e) / &2`]);
  (ABBREV_TAC `m = (&1 - c / &2) * (&4 - &2 * x)`);
  (ONCE_REWRITE_TAC[REAL_ARITH `m * x - m * y = m * (x - y)`]);
   AP_TERM_TAC;
  (ONCE_ASM_REWRITE_TAC[]);    

  (SUBGOAL_THEN `sqrt (X * C) = (X * C) / sqrt (X * C)` ASSUME_TAC);
    (SUBGOAL_THEN 
      `sqrt (X * C) * sqrt (X * C) = (X * C) ==> 
       sqrt (X * C) = (X * C) / sqrt (X * C)` ASSUME_TAC);
    (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
    (MATCH_MP_TAC (GSYM REAL_EQ_RDIV_EQ));
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);    

  (FIRST_X_ASSUM MATCH_MP_TAC); 
  (REWRITE_TAC[GSYM REAL_POW_2]);
  (MATCH_MP_TAC SQRT_POW_2);
  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
  (ASM_REWRITE_TAC[]);

 (ABBREV_TAC `n = (X * C) / &2 / sqrt (X * C)`);
 (ABBREV_TAC `n' = inv (sqrt (X * C))`);
 (PURE_ONCE_ASM_REWRITE_TAC[]);
 (EXPAND_TAC "n" THEN EXPAND_TAC "n'");
 (REWRITE_TAC[REAL_ARITH `a / x - y = a / &2 / x <=> a / & 2 / x = y`]);
 (REWRITE_TAC[REAL_ARITH `(a *  b * c) / x = (a * b) / x  * c`]);
 (ABBREV_TAC `t = (X * C) / &2`);
 (ABBREV_TAC `r' = sqrt (X * C)`);

    (SUBGOAL_THEN `t = (t * inv r') * r'  ==> t / r' = t * inv r'`
       ASSUME_TAC);
    (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
    (MATCH_MP_TAC (GSYM REAL_EQ_LDIV_EQ));
    (EXPAND_TAC "r'");
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);

  (FIRST_X_ASSUM MATCH_MP_TAC); 
  (REWRITE_TAC[REAL_ARITH `(m * inv n) * n = m * (inv n * n)`]);
  (MATCH_MP_TAC (MESON[REAL_MUL_RID] 
                  `inv r' * r' = &1 ==> m = m * inv r' * r'`));
  (MATCH_MP_TAC REAL_MUL_LINV);
  (MATCH_MP_TAC (REAL_ARITH `&0 < n ==> ~ (n = &0)`));
  (EXPAND_TAC "r'");
  (MATCH_MP_TAC SQRT_POS_LT);
  (ASM_REWRITE_TAC[]);


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

(SUBGOAL_THEN 
  `(F2 has_real_derivative
   ((&2 - c) * (&2 - x)) * C / &2 / (X + C - X * C / &4) / sqrt (X * C))
   (atreal x within r)`
   ASSUME_TAC);

  (SUBGOAL_THEN `2G (x:real) pow 2 = X * C` ASSUME_TAC);
  (MATCH_MP_TAC (REAL_ARITH 
    `2G (x:real) pow 2 = &4 * D' /\ &4 * D' = X * C ==> 
     2G (x:real) pow 2 = X * C`));
  (ASM_REWRITE_TAC[REAL_ARITH `(&4 * z = x * y) <=> ((x * y) / &4 = z)`]);  
  (EXPAND_TAC "D'");  
  (REWRITE_TAC[REAL_ARITH `&4 * (X * C) / &4 = X * C`]);
  (MATCH_MP_TAC SQRT_POW_2);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `(((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G') / 2G x pow 2 *
       inv (&1 + F22 x pow 2) = 
     ((&2 - c) * (&2 - x)) * C / &2 / (X + C - X * C / &4) / sqrt (X * C)`
     ASSUME_TAC);
  (ASM_REWRITE_TAC[]);
  (ABBREV_TAC `m = X + C - X * C / &4`);
  (REWRITE_TAC[REAL_ARITH 
    `(a * b / c / d) / e * f / g = (a * f * (b / e)) / c / g / d`]);  
  (REWRITE_TAC[REAL_ARITH 
    `(a * b / c / d / e)= (a * b) / c / d / e`]);  

  (REPEAT(AP_THM_TAC THEN AP_TERM_TAC));
  (REWRITE_TAC[REAL_ARITH 
    `((&1 - c / &2) * (&4 - &2 * x)) = ((&2 - c) * (&2 - x))`]);
   AP_TERM_TAC;
  (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> (y * x = y)`));
  (MATCH_MP_TAC REAL_DIV_REFL);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
  (ASM_REWRITE_TAC[]);  

(ASM_MESON_TAC[]);
(UP_ASM_TAC THEN REPLICATE_TAC 9 DEL_TAC);
(REPEAT DISCH_TAC);

(* Begin Diff 3 *)

(ABBREV_TAC `f3 = (\x. (&8 + (x * c) / &2 - &2 * x - &2 * c))`);
(ABBREV_TAC 
   `F32 = (\x.(&8 + (x * c) / &2 - &2 * x - &2 * c) /
            sqrt ((((&4 - x) * x) * C) / &4))`);

  (SUBGOAL_THEN 
    `(F32 has_real_derivative
     ((c / &2 - &2) * G x - f3 x * G') / G x pow 2) (atreal x within r)`
     ASSUME_TAC);

    (SUBGOAL_THEN `F32 = (\x:real.  f3 x / G x)` ASSUME_TAC);
      (* Subgoal *) 
    (EXPAND_TAC "F32" THEN EXPAND_TAC "G" THEN EXPAND_TAC "f3");
    (REWRITE_TAC[]);

  (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);

    (SUBGOAL_THEN 
      `(f3 has_real_derivative (c / &2 - &2)) 
       (atreal x within r) /\ 
       (G has_real_derivative G') (atreal x within r) /\ ~(G x = &0)`
       ASSUME_TAC);
      (*  Subgoal *)
    (ASM_REWRITE_TAC[]);    
     CONJ_TAC;  (* Break into 2 subgoals *)

      (EXPAND_TAC "f3" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
      (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
      (EXPAND_TAC "G");
      (MATCH_MP_TAC SQRT_POS_LT);
      (ASM_REWRITE_TAC[]);

   UP_ASM_TAC;
  (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
  (MESON_TAC[]);


(* --------------------------------------------------------------------------*)
(*         Derivative of  atn (....)                                         *)  
(* --------------------------------------------------------------------------*)

  (SUBGOAL_THEN 
    `(F3 has_real_derivative
     ((c / &2 - &2) * G x - f3 x * G') / G x pow 2 * inv (&1 + F32 x pow 2))
     (atreal x within r)`
     ASSUME_TAC);

    (SUBGOAL_THEN `F3 = (\x:real. atn (F32 x))` ASSUME_TAC);
      (* Subgoal *)
    (EXPAND_TAC "F3" THEN EXPAND_TAC "F32");
    (REWRITE_TAC[]); 

  (ONCE_ASM_REWRITE_TAC[]);
   DEL_TAC;
  (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
  (ABBREV_TAC `f' = ((c / &2 - &2) * G (x:real) - f3 x * G') / G x pow 2`);

    (SUBGOAL_THEN 
      `inv (&1 + F32 x pow 2) = g' ((F32:real-> real) x)`
       ASSUME_TAC);
      (* Subgoal *)
    (EXPAND_TAC "F32" THEN EXPAND_TAC "g'");
    (MESON_TAC[]);
 
  (ONCE_ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN 
     `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
      ASSUME_TAC);   
      (* Subgoal *)
    (EXPAND_TAC "g'");
    (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);

    (SUBGOAL_THEN 
      `(F32 has_real_derivative f') (atreal x within r) /\ 
       (:real) (F32 x)` ASSUME_TAC);
      (* Subgoal *)
    (ASM_REWRITE_TAC[]);
    (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);

  (REPLICATE_TAC 2 UP_ASM_TAC);
  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
  (MESON_TAC[]);

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

  (SUBGOAL_THEN 
    `inv (&1 + F32 (x:real) pow 2) = (x * c) / (x * c + (&4 - x) * (&4 - c))`
     ASSUME_TAC);
  (ONCE_REWRITE_TAC[GSYM REAL_INV_DIV]);
   AP_TERM_TAC;
  (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);

    (SUBGOAL_THEN `(x * c) / (x * c) = &1` ASSUME_TAC);
    (MATCH_MP_TAC REAL_DIV_REFL);
    (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=> ~a /\ ~b`]);
    (ASM_REWRITE_TAC[]);
 
  (ONCE_ASM_REWRITE_TAC[]); 
  (AP_TERM_TAC);
  (EXPAND_TAC "F32");
  (REWRITE_TAC[REAL_POW_DIV]);
  (ONCE_ASM_REWRITE_TAC[]);

    (SUBGOAL_THEN `sqrt ((X * C) / &4) pow 2 = (X * C) / &4` ASSUME_TAC);
    (MATCH_MP_TAC SQRT_POW_2);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
    (ASM_REWRITE_TAC[]);
  (ONCE_ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ARITH `(x * a) * x * a = x pow 2 * a pow 2`]);
  (REWRITE_TAC[REAL_ARITH 
     `&8 + (x * c) / &2 - &2 * x - &2 * c = ((&4 - x) * (&4 - c)) / &2`]);
  (REWRITE_TAC[REAL_POW_DIV]);
  (REWRITE_TAC[REAL_ARITH `&2 pow 2 = &4`]);
  (ABBREV_TAC `m = ((&4 - x) * (&4 - c)) pow 2 / &4`);
  (ABBREV_TAC `n = ((X * C) / &4)`);
  (ABBREV_TAC `p = ((&4 - x) * (&4 - c)) / (x * c)`);

    (SUBGOAL_THEN `m = p * n ==> (m / n = p)` ASSUME_TAC); 
    (MATCH_MP_TAC (MESON[] `(b <=> a) ==> (a ==> b)`));
    (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
    (EXPAND_TAC "n");    
    (ASM_REWRITE_TAC[]);

  (FIRST_X_ASSUM MATCH_MP_TAC);
  (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN EXPAND_TAC "p");
  (REWRITE_TAC[REAL_ARITH `(a / x) * (b / y) = (a * b) / x / y`]);
  (AP_THM_TAC THEN AP_TERM_TAC);
  (REWRITE_TAC[REAL_ARITH `(a * b * c) / x = a * (b * c) / x`]);
  (REWRITE_TAC[REAL_POW_2]);
   AP_TERM_TAC;
  (EXPAND_TAC "X" THEN EXPAND_TAC "C");
  (REWRITE_TAC[REAL_ARITH `((a * b) * c * d) / e = (a * c) * (b * d) / e`]);
  (MATCH_MP_TAC (MESON[REAL_MUL_RID] `y = &1 ==> x = x * y`));
  (MATCH_MP_TAC REAL_DIV_REFL);
  (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=> ~a /\ ~b`]);
  (ASM_REWRITE_TAC[]);

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


  (SUBGOAL_THEN `G (x:real) = sqrt ((X * C) / &4)` ASSUME_TAC);  
  (EXPAND_TAC "G");
  (ONCE_ASM_REWRITE_TAC[]);
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `G' = ((&4 - &2 * x) * C) / &4 * inv (sqrt (X * C))` ASSUME_TAC);
  (EXPAND_TAC "G'");
  (REPEAT AP_TERM_TAC);
  (MATCH_MP_TAC (REAL_ARITH 
    `(&2 * sqrt x = sqrt (&4) * sqrt x) /\ (sqrt (&4) * sqrt x = y)
      ==> &2 * sqrt x = y`));
  (ASM_REWRITE_TAC[]);
   CONJ_TAC;

  (AP_THM_TAC THEN AP_TERM_TAC);
  (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`]);
  (SIMP_TAC[REAL_ARITH `&0 <= &2`; SQRT_MUL]);
  (SIMP_TAC[GSYM REAL_POW_2; GSYM SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
  
  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `X * C = &4 * (X * C) / &4`]);
  (ASM_REWRITE_TAC[]);
  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&4 * (a * b) / &4 = a * b`]);
  (MATCH_MP_TAC (GSYM SQRT_MUL));
  (REWRITE_TAC[REAL_ARITH `&0 <= &4`]);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
  (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `(c / &2 - &2) * G x - f3 x * G' = 
     (--C * ((&4 - x) * (&4 - c))) / &2 / sqrt (X * C)` ASSUME_TAC);

  (ONCE_ASM_REWRITE_TAC[]);
  (EXPAND_TAC "f3");

  (SUBGOAL_THEN `sqrt ((X * C) / &4) = sqrt (X * C) / &2` ASSUME_TAC);
    (SUBGOAL_THEN `&2 = sqrt (&4) ` ASSUME_TAC); 
    (MATCH_MP_TAC (REAL_ARITH 
      `(&2) = sqrt (&2) * sqrt (&2) /\ sqrt (&2) * sqrt (&2) = sqrt (&4) ==> 
       &2 = sqrt (&4)`));
     CONJ_TAC;
      (REWRITE_TAC[GSYM REAL_POW_2]);
      (MATCH_MP_TAC (GSYM SQRT_POW_2));
       REAL_ARITH_TAC;

      (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`]);
      (MESON_TAC[SQRT_MUL; REAL_ARITH `&0 <= &2`]);
  (ONCE_ASM_REWRITE_TAC[]);
  (EXPAND_TAC "D'");
  (MATCH_MP_TAC SQRT_DIV);
  (REWRITE_TAC[REAL_ARITH `&0 <= &4`]);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
  (ASM_REWRITE_TAC[]);

(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH 
  `(c / &2 - &2) * x / &2 = --(&4 - c) / &4 * x`]);
(REWRITE_TAC[REAL_ARITH 
  `(&8 + (x * c) / &2 - &2 * x - &2 * c) * s / &4 * r = 
   ((&4 - x) * (&4 - c)) * s / &8 * r`]);

  (SUBGOAL_THEN `--(&4 - c) / &4 * sqrt (X * C) =     
    (--(&4 - c) / &4 * (X * C)) / sqrt (X * C)` ASSUME_TAC);

  (REWRITE_TAC[REAL_ARITH 
    `(--(&4 - c) / &4 * X * C) / Y = (--(&4 - c) / &4) * (X * C) / Y `]);
   AP_TERM_TAC;

    (SUBGOAL_THEN 
      `sqrt (X * C) * sqrt (X * C) = (X * C) ==> 
       sqrt (X * C) = (X * C) / sqrt (X * C)` ASSUME_TAC);
    (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
    (MATCH_MP_TAC (GSYM REAL_EQ_RDIV_EQ));
    (MATCH_MP_TAC SQRT_POS_LT);
    (ASM_REWRITE_TAC[]);    

  (FIRST_X_ASSUM MATCH_MP_TAC); 
  (REWRITE_TAC[GSYM REAL_POW_2]);
  (MATCH_MP_TAC SQRT_POW_2);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
  (ASM_REWRITE_TAC[]);
 
 (PURE_ONCE_ASM_REWRITE_TAC[]);
 (REWRITE_TAC[REAL_ARITH `a / x - y = b / x <=> (a - b) / x = y`]);
 (EXPAND_TAC "X" THEN EXPAND_TAC "C");
 (REWRITE_TAC[REAL_ARITH 
   `((&4 - x) * (&4 - c)) *
    ((&4 - &2 * x) * (&4 - c) * c) / &8 * N = (((&4 - x) * (&4 - c)) *
    ((&4 - &2 * x) * (&4 - c) * c) / &8) * N `]);
(ABBREV_TAC 
  `m = ((&4 - x) * (&4 - c)) * ((&4 - &2 * x) * (&4 - c) * c) / &8`);
(ASM_REWRITE_TAC[]);
(ABBREV_TAC `n = sqrt (X * C)`);
 
  (SUBGOAL_THEN 
    `(--(&4 - c) / &4 * X * C - (--C * (&4 - x) * (&4 - c)) / &2) = m`
    ASSUME_TAC);
  (EXPAND_TAC "X" THEN EXPAND_TAC "C" THEN EXPAND_TAC "m");
   REAL_ARITH_TAC;    
  
(ONCE_ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN `m = (m * inv n) * n  ==> m / n = m * inv n` ASSUME_TAC);
  (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
  (MATCH_MP_TAC (GSYM REAL_EQ_LDIV_EQ));
  (EXPAND_TAC "n");
  (MATCH_MP_TAC SQRT_POS_LT);
  (ASM_REWRITE_TAC[]);    

  (FIRST_X_ASSUM MATCH_MP_TAC); 
  (REWRITE_TAC[REAL_ARITH `(m * inv n) * n = m * (inv n * n)`]);
  (MATCH_MP_TAC (MESON[REAL_MUL_RID] 
                  `inv r' * r' = &1 ==> m = m * inv r' * r'`));
  (MATCH_MP_TAC REAL_MUL_LINV);
  (MATCH_MP_TAC (REAL_ARITH `&0 < n ==> ~ (n = &0)`));
  (EXPAND_TAC "n");
  (MATCH_MP_TAC SQRT_POS_LT);
   ASM_REAL_ARITH_TAC;    
  (ASM_REWRITE_TAC[]);    

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


(ABBREV_TAC `F12 = 
  (\x. ((&1 - x / &2) * C) / (&2 * sqrt ((((&4 - x) * x) * C) / &4)))`);

    (SUBGOAL_THEN `sqrt ((X * C) / &4) pow 2 = (X * C) / &4` ASSUME_TAC);
    (MATCH_MP_TAC SQRT_POW_2);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
    (ASM_REWRITE_TAC[]);

  (SUBGOAL_THEN 
    `X + C - X * C / &4 = (&1 + F12 (x:real) pow 2 ) * X` ASSUME_TAC);

  (EXPAND_TAC "X" THEN EXPAND_TAC "C" THEN EXPAND_TAC "F12");
  (ONCE_ASM_REWRITE_TAC[]);
  (ONCE_REWRITE_TAC[REAL_POW_DIV]);
  (ONCE_REWRITE_TAC[REAL_POW_2]);
  (ONCE_REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * a = &4 * a pow 2`]);
  (ONCE_ASM_REWRITE_TAC[]);
  (ONCE_REWRITE_TAC[REAL_ARITH `&4 * x / &4 = x`]);
  (ONCE_REWRITE_TAC[REAL_ARITH 
    `((&1 - x / &2) * C) * (&1 - x / &2) * C = 
     (&1 - ((&4 - x) * x) / &4) * C * C`]);
  (ONCE_ASM_REWRITE_TAC[]);
  
    (SUBGOAL_THEN `&1 = (X * C) / (X * C)` ASSUME_TAC); 
    (REWRITE_TAC[EQ_SYM_EQ]);
    (MATCH_MP_TAC REAL_DIV_REFL);
    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
    (ASM_REWRITE_TAC[]);    

  (ONCE_REWRITE_TAC[REAL_ARITH `(&1 - x) * y = y - x * y`]);
  (ONCE_ASM_REWRITE_TAC[]);
  (ONCE_REWRITE_TAC[REAL_ARITH `a / x + b / x = (a + b) / x`]);
  (ONCE_REWRITE_TAC[REAL_ARITH 
    `X * C + C * C - X / &4 * C * C = (X + C - X * C / &4) * C`]);
  (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c * d = a * (d * b) / c`]);
  (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> (a = a * x)`));
  (MATCH_MP_TAC REAL_DIV_REFL);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
  (ASM_REWRITE_TAC[]);    

  (SUBGOAL_THEN `~ (X + C - X * C / &4 = &0)` ASSUME_TAC);
  (ONCE_ASM_REWRITE_TAC[]);
  (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~ a /\ ~ b`]);
  (ASM_REWRITE_TAC[]);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
  (MATCH_MP_TAC (REAL_ARITH `&0 <= x ==> &0 < &1 + x`));
  (REWRITE_TAC[REAL_LE_POW_2]);

  (UP_ASM_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN REPEAT DISCH_TAC);    

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


(SUBGOAL_THEN 
  `(F3 has_real_derivative
   (-- &2 * C * (&2 * x + &2 * c - x * c)) / &8 / (X + C - X * C / &4) /
    sqrt (X * C)) (atreal x within r)`
   ASSUME_TAC);

  (SUBGOAL_THEN `G (x:real) pow 2 = (X * C) / &4` ASSUME_TAC);
  (EXPAND_TAC "G");  
  (ASM_REWRITE_TAC[]);
  (MATCH_MP_TAC SQRT_POW_2);
  (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
  (ASM_REWRITE_TAC[]);    

  (SUBGOAL_THEN 
    `((c / &2 - &2) * G x - f3 x * G') / G x pow 2 * inv (&1 + F32 x pow 2) =
     (-- &2 * C * (&2 * x + &2 * c - x * c)) / &8 / (X + C - X * C / &4) /
     sqrt (X * C)` ASSUME_TAC);
  (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
  (REWRITE_TAC[REAL_ARITH 
    `(a / b / c / d) * f / g = (a * f) / b / d / g / c `]);  
  (REPEAT(AP_THM_TAC THEN AP_TERM_TAC));

  (ABBREV_TAC 
    `x1 = (x * c + (&4 - x) * (&4 - c))`);
  (ABBREV_TAC 
    `x2 = &2 * x + &2 * c - x * c`);

  (SUBGOAL_THEN 
    `X + C - X * C / &4 = x1 * x2 / &8` ASSUME_TAC);
  (EXPAND_TAC "X" THEN EXPAND_TAC "C" THEN EXPAND_TAC "x1" THEN EXPAND_TAC "x2");
  (REAL_ARITH_TAC);

(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH `(--x * a * b) * c * d = --x * (a * c) * (b * d)`]);
(ASM_REWRITE_TAC[]);

(SUBGOAL_THEN `~ (x1 = &0) /\ ~ (x2 = &0)` ASSUME_TAC);
(REPEAT STRIP_TAC);
  
  (SUBGOAL_THEN `X + C - X * C / &4 = &0` ASSUME_TAC);
  (MATCH_MP_TAC 
  (MESON[REAL_MUL_LZERO] `(x = x1 * x2 / &8) /\ (x1 = &0) ==> (x = &0)`));
  (ASM_REWRITE_TAC[]);  
  (MP_TAC (ASSUME `~(X + C - X * C / &4 = &0)`));
  (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);

  (SUBGOAL_THEN `X + C - X * C / &4 = &0` ASSUME_TAC);
  (MATCH_MP_TAC 
    (MESON[REAL_MUL_RZERO; REAL_ARITH `&0 / x = &0`] 
    `(x = x1 * x2 / &8) /\ (x2 = &0) ==> (x = &0)`));
  (ASM_REWRITE_TAC[]);  
  (MP_TAC (ASSUME `~(X + C - X * C / &4 = &0)`));
  (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);

(REWRITE_TAC[EQ_SYM_EQ]);
(REWRITE_TAC[REAL_ARITH `(-- &2 * C * x2) / &8 / (x1 * x2 / &8) =
                           (-- &2 * C) * (x2 / &8) / (x1 * x2 / &8)`]);
(SUBGOAL_THEN 
  `(-- &2 * C) * x2 / &8 / (x1 * x2 / &8) = (-- &2 * C) / x1 ` ASSUME_TAC);
(MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (REAL_ARITH `~(x = &0) ==> ~(x / &8 = &0)`));
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "D'");
(AP_THM_TAC THEN AP_TERM_TAC);
(REWRITE_TAC[REAL_ARITH `x / &2  = (x * &2) / &4 `]);
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `a / (b / &4) = a / (&1 * b / &4) `]);
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `((--C * X * C) * &2) / &4 = 
                                     (-- &2 * C) * (X * C) / &4 `]);
(PURE_REWRITE_TAC[EQ_SYM_EQ]);
(PURE_REWRITE_TAC[REAL_ARITH `(a * b / c) / d = a * (b/ c/ d)`]);
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a = b / &1`]);
(MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
(REWRITE_TAC[REAL_ARITH `~(&1 = &0)`]);
(MATCH_MP_TAC (REAL_ARITH `&0 < x  ==> ~ (x / &4 = &0)`));
(ASM_REWRITE_TAC[]);

(ASM_MESON_TAC[]);
(UP_ASM_TAC THEN UP_ASM_TAC THEN REPLICATE_TAC 8 DEL_TAC THEN REPEAT DISCH_TAC);


(ABBREV_TAC `F1' = -- &2 * C / (X + C - X * C / &4) / sqrt (X * C)`);
(ABBREV_TAC `F2' = 
  ((&2 - c) * (&2 - x)) * C / &2 / (X + C - X * C / &4) / sqrt (X * C)`);

(ABBREV_TAC `F3' = 
   (-- &2 * C * (&2 * x + &2 * c - x * c)) / &8 /
   (X + C - X * C / &4) / sqrt (X * C)`);


(SUBGOAL_THEN `&0 - (F1' + F2') + &2 * F3' = &0` ASSUME_TAC);
(REWRITE_TAC[REAL_ARITH `&0 - (a + b) + c = &0 <=> a + b - c = &0`]);
(EXPAND_TAC "F1'" THEN EXPAND_TAC "F2'" THEN EXPAND_TAC "F3'");
(ONCE_REWRITE_TAC[REAL_ARITH `--a / x + b / x - &2 * c / x = (--a + b - &2 * c) / x`]);


(ABBREV_TAC `m = sqrt (X * C)`);
(ABBREV_TAC `n = X + C - X * C / &4`);
(REWRITE_TAC[REAL_ARITH `-- &2 * x / a  + y * z / a - &2 * t / a = 
(-- &2 * x + y * z - &2 * t) / a `]);

(SUBGOAL_THEN `(-- &2 * C +
  ((&2 - c) * (&2 - x)) * C / &2 -
  &2 * (-- &2 * C * (&2 * x + &2 * c - x * c)) / &8) = &0 ` ASSUME_TAC);
(EXPAND_TAC "C");
 REAL_ARITH_TAC;
(ASM_REWRITE_TAC[]);

(SUBGOAL_THEN `&0 / n = &0 ` ASSUME_TAC);
(MATCH_MP_TAC (REAL_ARITH `~(x = &0) ==> &0 / x = &0`));
(ASM_REWRITE_TAC[]);

(ASM_REWRITE_TAC[]); 
 (MATCH_MP_TAC (REAL_ARITH `~(x = &0) ==> &0 / x = &0`)); 
 (EXPAND_TAC "m"); 
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`)); 
 (MATCH_MP_TAC SQRT_POS_LT); 
 (ASM_REWRITE_TAC[]);
 
 (ABBREV_TAC `FUN1 = (\x:real. --pi / &2 - F1 x - F2 x)`); 
 (ABBREV_TAC `FUN2 = (\x:real. F1 x + F2 x)`);
 
 (SUBGOAL_THEN `(FUN2 has_real_derivative F1' + F2') (atreal x within r)` ASSUME_TAC); 
 (EXPAND_TAC "FUN2"); 
 (ASM_SIMP_TAC[HAS_REAL_DERIVATIVE_ADD]);
 
 (SUBGOAL_THEN `(FUN1 has_real_derivative &0 - (F1' + F2')) (atreal x within r)` ASSUME_TAC);
    (SUBGOAL_THEN `FUN1 = (\x:real. --pi / &2 - FUN2 x)` ASSUME_TAC);
    (EXPAND_TAC "FUN1" THEN EXPAND_TAC "FUN2");
    (REWRITE_TAC[REAL_ARITH `a - (b + c) = a - b - c`]);
 
 (ASM_REWRITE_TAC[]);
 
 (SUBGOAL_THEN `((\x:real. --pi / &2) has_real_derivative &0 ) 
                 (atreal x within r)` ASSUME_TAC);
(REAL_DIFF_TAC); 
 (MESON_TAC[]);
 
 (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC); 
 (MP_TAC HAS_REAL_DERIVATIVE_SUB THEN MESON_TAC[]);
 
 (ABBREV_TAC `FUN3 = (\x:real. &2 * F3 x)`); 
 (SUBGOAL_THEN `(FUN3 has_real_derivative &2 * F3') (atreal x within r)` ASSUME_TAC); 
 (EXPAND_TAC "FUN3"); 
 (MP_TAC (ASSUME `(F3 has_real_derivative F3') (atreal x within r)`));  
 (MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN THEN MESON_TAC[]);

 
 (SUBGOAL_THEN `(FUNCTION has_real_derivative &0 - (F1' + F2') + &2 * F3') (atreal x within r)` ASSUME_TAC);

    (SUBGOAL_THEN `(\x. --pi / &2 - F1 x - F2 x + &2 * F3 x) = (\x:real. FUN1 x + FUN3 x)` ASSUME_TAC);
    (EXPAND_TAC "FUN1" THEN EXPAND_TAC "FUN3");
    (MESON_TAC[]);

    (ASM_REWRITE_TAC[]); 
 (ASM_MESON_TAC[HAS_REAL_DERIVATIVE_ADD]); 
 (ASM_MESON_TAC[]);

(* ========================================================================= *)
 
 (SUBGOAL_THEN `&0 < (&4 - c) * c` ASSUME_TAC); 
 (MATCH_MP_TAC REAL_LT_MUL);
 ASM_REAL_ARITH_TAC;
 
 (SUBGOAL_THEN `sqrt ((((&4 - c) * c) * (&4 - c) * c) / &4) = 
                 ((&4 - c) * c) / &2` ASSUME_TAC); 
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]); 
 (MATCH_MP_TAC SQRT_RULE_Euler_lemma);
 ASM_REAL_ARITH_TAC;
 
 (ASM_REWRITE_TAC[REAL_ARITH `&2 * x / &2 = x`]); 
 (REWRITE_TAC[REAL_ARITH 
 `&8 + (c * c) / &2 - &2 * c - &2 * c = (&4 - c) * ((&4 - c) / &2)`]); 
 (REWRITE_TAC[REAL_ARITH `((&4 - c) * c) / &2 = c * ((&4 - c) / &2)`]); 
 (REWRITE_TAC[REAL_ARITH `(a * b) / (c * d) = a * b / (c * d)`]);
 
 (SUBGOAL_THEN `(&4 - c) * (&4 - c) / &2 / (c * (&4 - c) / &2) = (&4 - c) / c` ASSUME_TAC);
 
 (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma); 
 (ASM_REWRITE_TAC[]);
 ASM_REAL_ARITH_TAC;
 
 (ONCE_ASM_REWRITE_TAC[]);
 
 (SUBGOAL_THEN `(&1 - c / &2) * (&4 - c) * c / ((&4 - c) * c) = (&1 - c / &2)` ASSUME_TAC); 
 (REWRITE_TAC[REAL_ARITH `a * b * c / d = a * (b * c) / d`]); 
 (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> a * x = a`)); 
 (MATCH_MP_TAC REAL_DIV_REFL); 
 (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=>  ~a /\ ~b`]);
 ASM_REAL_ARITH_TAC;
 
 (ASM_REWRITE_TAC[REAL_ARITH `a - b - b = a - &2 * b`]);
 
 (ABBREV_TAC `P = {x| &0 < x /\ x < &4}`);
 
 (SUBGOAL_THEN `is_realinterval P` ASSUME_TAC); 
 (EXPAND_TAC "P"); 
 (MP_TAC REAL_INTERVAL_Euler_lemma); 
 (REPEAT LET_TAC); 
 (UP_ASM_TAC THEN MESON_TAC[]);
 
 (SUBGOAL_THEN `&2 IN P` ASSUME_TAC); 
 (EXPAND_TAC "P"); 
 (REWRITE_TAC [IN_ELIM_THM]);
 REAL_ARITH_TAC;
 
 (SUBGOAL_THEN `!x. x IN P ==> ~(x = &0) /\ ~(&4 - x = &0)` ASSUME_TAC); 
 (GEN_TAC THEN EXPAND_TAC "P"); 
 (REWRITE_TAC [IN_ELIM_THM]);
 REAL_ARITH_TAC;
 
 (SUBGOAL_THEN `(c:real) IN P` ASSUME_TAC); 
 (EXPAND_TAC "P"); 
 (ASM_REWRITE_TAC [IN_ELIM_THM]);
 
 (REPLICATE_TAC 4 UP_ASM_TAC); 
 (MP_TAC DERIVATIVE_WRT_C1_Euler_lemma); 
 (MESON_TAC[DERIVATIVE_WRT_C1_Euler_lemma]);
 
 (ABBREV_TAC `R = {x:real| &0 < x /\ x < &4}`);
 
 (SUBGOAL_THEN `(c:real) IN R` ASSUME_TAC); 
 (EXPAND_TAC"R" THEN ASM_REWRITE_TAC[IN_ELIM_THM]); 
 (SUBGOAL_THEN `is_realinterval R` ASSUME_TAC); 
 (EXPAND_TAC"R" THEN REWRITE_TAC[is_realinterval]); 
 (REWRITE_TAC[IN_ELIM_THM]); 
 (REPEAT STRIP_TAC);
  (MATCH_MP_TAC (REAL_ARITH `&0 < a' /\ a' <= c ==> &0 < c`));
  (ASM_REWRITE_TAC[]);
  (MATCH_MP_TAC (REAL_ARITH `c' <= b' /\ b' < &4 ==> c' < &4`));
  (ASM_REWRITE_TAC[]);
 
 (SUBGOAL_THEN `!y. y IN R ==> &0 < ((&4 - y) * y) * (&4 - c) * c` ASSUME_TAC);
 
 (GEN_TAC THEN EXPAND_TAC "R" THEN REWRITE_TAC[IN_ELIM_THM]);
 STRIP_TAC; 
 (MATCH_MP_TAC REAL_LT_MUL);
  STRIP_TAC; 
 (MATCH_MP_TAC REAL_LT_MUL);
 ASM_REAL_ARITH_TAC; 
 (MATCH_MP_TAC REAL_LT_MUL); 
ASM_REAL_ARITH_TAC;
 
 (SUBGOAL_THEN `(b:real) IN R` ASSUME_TAC); 
 (EXPAND_TAC"R" THEN ASM_REWRITE_TAC[IN_ELIM_THM]);
 
 (REPLICATE_TAC 4 UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC); 
 (MESON_TAC[]);

 
 (EXPAND_TAC "d"); 
 (FIRST_X_ASSUM MATCH_MP_TAC); 
 (EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM])
]);;
  
  
end;;