(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: UPFZBZM                                                  *)
(*      SUM_GAMMAX_LMFUN_ESTIMATE - a supported lemma.                       *)
(*      Chaper    : Packing (Clusters)                                       *)
(*                                                                           *)
(* ========================================================================= *)
open Sum_beta_bump;;

let TSKAJXY_statement = new_definition
   `TSKAJXY_statement <=>
      (!V X.
          saturated V /\
          packing V /\
          mcell_set V X /\
          critical_edgeX V X = {}
          ==> gammaX V X lmfun >= &0)`;;
let SUM_GAMMAX_LMFUN_ESTIMATE_concl = 
  `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\ 
               cell_cluster_estimate V /\ TSKAJXY_statement ==> 
    c * r pow 2 <=  sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X} 
    (\X. gammaX V X lmfun)`;;

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

let SUM_GAMMAX_LMFUN_ESTIMATE = prove_by_refinement (
    SUM_GAMMAX_LMFUN_ESTIMATE_concl,

[(GEN_TAC);

(* ================== Choose the constants ================================= *)

 (NEW_GOAL `?cc1. (&1 <= cc1) /\ (!V X.
             packing V /\ saturated V /\ mcell_set V X
             ==> gammaX V X lmfun <= cc1)`);
 (MP_TAC BOUND_GAMMA_X_lmfun THEN STRIP_TAC);
 (EXISTS_TAC `max (c:real) (&1)`);
 (STRIP_TAC);
 (REAL_ARITH_TAC);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `gammaX V X lmfun <= c`);
 (ASM_MESON_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN STRIP_TAC);

 (NEW_GOAL `?cc2. (&1 <= cc2) /\ 
            (!V u0.
             saturated V /\ packing V /\ u0 IN V
             ==> & (CARD {X | mcell_set V X /\ VX V X u0}) <= cc2)`);

 (MP_TAC CARD_MCELL_CONTAINS_POINT_klemma);
 (STRIP_TAC);
 (EXISTS_TAC `max (&c:real) (&1)`);
 (STRIP_TAC);
 (REAL_ARITH_TAC);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= (&c:real)`);
 (REWRITE_TAC[REAL_OF_NUM_LE]);
 (ASM_MESON_TAC[]);
 (ABBREV_TAC `s = &(CARD {X | mcell_set V X /\ VX V X u0})`);
 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN STRIP_TAC);

 (NEW_GOAL
 `?cc3. &1 <= cc3 /\
       (!V X e.
            saturated V /\ packing V /\ mcell_set V X /\ critical_edgeX V X e
            ==> beta_bump V e X <= cc3)`);
 (MP_TAC BOUND_BETA_BUMP THEN STRIP_TAC);
 (EXISTS_TAC `max (c:real) (&1)`);
 (STRIP_TAC);
 (REAL_ARITH_TAC);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `beta_bump V e X <= c`);
 (ASM_MESON_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN STRIP_TAC);

 (NEW_GOAL
 `?cc4. &1 <= cc4 /\
       (!V u0. 
           saturated V /\ packing V /\ u0 IN V 
            ==> &(CARD {X | mcell_set V X /\ VX V X u0}) <= cc4)`);
 (MP_TAC CARD_MCELL_CONTAINS_POINT_klemma THEN STRIP_TAC);
 (EXISTS_TAC `max (&c) (&1)`);
 (STRIP_TAC);
 (REAL_ARITH_TAC);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= &c`);
 (REWRITE_TAC[REAL_OF_NUM_LE]);
 (ASM_MESON_TAC[]);
 (ABBREV_TAC `s = &(CARD {X | mcell_set V X /\ VX V X u0})`);
 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN STRIP_TAC);

 (ASM_CASES_TAC `saturated V /\ packing V`);

 (NEW_GOAL 
  `?dd1. !r. &1 <= r ==> 
   &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &8))) <=
    dd1 * r pow 2`);

 (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &8)
    = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &8)`);
 (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
 (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]);
 (TAKE_TAC);

 (ABBREV_TAC `dd2 = max dd1 (&1)`);
 (ABBREV_TAC `dd = &1 / &2 * dd2 * (&4) pow 3 * cc2 * cc1`);

 (NEW_GOAL 
  `?dd3. !r. &1 <= r ==> 
  &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &16))) <=
   dd3 * r pow 2`);

 (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &16)
    = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &16)`);
 (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
 (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]);
 (TAKE_TAC);

 (ABBREV_TAC `dd4 = max dd3 (&1)`);
 (ABBREV_TAC `ss1 = (&4) pow 3 * cc4 * cc3`);
 (ABBREV_TAC `ss = &1 / &2 * dd4 * ss1`);

 (ABBREV_TAC `c:real = -- (dd + ss)`);
 (EXISTS_TAC `c:real`);


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

 (REPEAT STRIP_TAC);
 (NEW_GOAL `!X. mcell_set V X /\ critical_edgeX V X  = {} ==> 
                 gammaX V X lmfun >= &0`);
 (UP_ASM_TAC THEN REWRITE_TAC[TSKAJXY_statement]);
 (STRIP_TAC);
 (ASM_SIMP_TAC[]);

 (ABBREV_TAC `B = {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}`);
 (ABBREV_TAC `B0 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
                         critical_edgeX V X = {}}`);
 (ABBREV_TAC `B1 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
                         ~(critical_edgeX V X = {})}`);
 (NEW_GOAL `FINITE (B1:(real^3->bool)->bool)`);
 (EXPAND_TAC "B1");
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 (STRIP_TAC);
 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 (SET_TAC[]);

 (REWRITE_WITH `B = B0 UNION B1:(real^3->bool)->bool`);
 (EXPAND_TAC "B" THEN EXPAND_TAC "B1" THEN EXPAND_TAC "B0");
 (SET_TAC[]);
 (REWRITE_WITH `sum (B0 UNION B1) (\X. gammaX V X lmfun) = 
   sum B0 (\X. gammaX V X lmfun) + sum B1 (\X. gammaX V X lmfun)`);
 (MATCH_MP_TAC SUM_UNION);
 (REPEAT STRIP_TAC);
 (EXPAND_TAC "B0");
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 (STRIP_TAC);
 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 (SET_TAC[]);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "B1" THEN EXPAND_TAC "B0");
 (SET_TAC[]);
 (MATCH_MP_TAC (REAL_ARITH `&0 <= b /\ a <= c ==> a <= b + c`));
 (STRIP_TAC);
 (MATCH_MP_TAC SUM_POS_LE);
 (STRIP_TAC);
 (EXPAND_TAC "B0");
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 (STRIP_TAC);
 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 (SET_TAC[]);
 (REWRITE_TAC[BETA_THM; REAL_ARITH `&0 <= a <=> a >= &0`]);
 (EXPAND_TAC "B0" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_SIMP_TAC[]);

 (REWRITE_WITH 
  `sum B1 (\X. gammaX V X lmfun) = 
   sum B1 (\X. (gammaX V X lmfun) * 
                sum (critical_edgeX V X) (\e. critical_weight V X))`);
 (MATCH_MP_TAC SUM_EQ);
 (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[critical_weight]);
 (REWRITE_WITH 
  `sum (critical_edgeX V x) (\e. &1 / &(CARD (critical_edgeX V x))) = 
   &(CARD (critical_edgeX V x)) * (&1 / &(CARD (critical_edgeX V x)))`);
 (MATCH_MP_TAC SUM_CONST);
 (REWRITE_TAC[FINITE_critical_edgeX]);
 (REWRITE_TAC[REAL_ARITH `a * &1 / a = a / a`]);
 (REWRITE_WITH `&(CARD (critical_edgeX V x)) / &(CARD (critical_edgeX V x)) = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (REWRITE_TAC[REAL_OF_NUM_EQ]);
 (REWRITE_WITH `CARD (critical_edgeX V x) = 0 <=> critical_edgeX V x = {}`);
 (MATCH_MP_TAC CARD_EQ_0);
 (REWRITE_TAC[FINITE_critical_edgeX]);
 (ASM_REWRITE_TAC[]);
 (REAL_ARITH_TAC);

(* ------------------------------------------------------------------------- *)
(* Hint:      - See proofs of KIZHLTL1; KIZHLTL2 to adapt                    *)
(* ------------------------------------------------------------------------- *)

 (REWRITE_TAC[GSYM SUM_LMUL]);

 (ABBREV_TAC `T1:real^3->bool = V INTER ball (vec 0, r)`);
 (ABBREV_TAC `T2 = {{u0, u1:real^3} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\   
                                       hl [u0; u1] <= hplus}`);
 (NEW_GOAL `FINITE (T2:(real^3->bool)->bool)`);
 (EXPAND_TAC "T2" THEN MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{{u0, u1:real^3} | u0 IN T1 /\ u1 IN T1}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SET_PRODUCT_KY_LEMMA);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC Pack2.KIUMVTC);
 (ASM_REWRITE_TAC[]);
 (SET_TAC[]);

 (REWRITE_WITH 
 `sum B1 (\X. sum (critical_edgeX V X) 
                   (\x. gammaX V X lmfun * critical_weight V X)) =
  sum B1 (\X. sum {y:real^3->bool| y IN T2 /\ critical_edgeX V X y} 
                   (\x. gammaX V X lmfun * critical_weight V X))`);
 (MATCH_MP_TAC SUM_EQ);
 (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (AP_THM_TAC THEN AP_TERM_TAC);
 (REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);
 (STRIP_TAC);
 (SET_TAC[]);
 (REWRITE_TAC[SET_RULE `A SUBSET {y | T2 y /\ A y} <=> A SUBSET T2`]);
 (EXPAND_TAC "T2" THEN REWRITE_TAC[SUBSET; critical_edgeX; IN; IN_ELIM_THM; edgeX]);
 (REPEAT STRIP_TAC);
 (EXPAND_TAC "T1" THEN REWRITE_TAC[IN_ELIM_THM]);
 (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3`);
 (REWRITE_TAC[ASSUME `~(u' = v':real^3)`]);

 (REWRITE_TAC[ASSUME `x' = {u, v:real^3}`; MESON[IN] `V (x:real^3) <=> x IN V`;
               GSYM (ASSUME `{u, v} = {u', v':real^3}`); IN_INTER]);

 (NEW_GOAL `VX V x = V INTER x`);
 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `VX V x = {}`);
 (REWRITE_TAC[VX]);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `VX V x u'` THEN ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
 (SET_TAC[]);

 (STRIP_TAC);
 (ASM_SET_TAC[]);
 (STRIP_TAC);
 (ASM_SET_TAC[]);
 (REWRITE_WITH `hl [u';
 v':real^3] = hl [u; v:real^3]`);
 (ASM_REWRITE_TAC[HL; set_of_list]);
 (ASM_REWRITE_TAC[]);

 (ABBREV_TAC `f = (\X. (\x:real^3->bool. 
                            gammaX V X lmfun * critical_weight V X))`);
 (REWRITE_WITH 
 `sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y}
                  (\x:real^3->bool. gammaX V X lmfun * critical_weight V X)) = 
  sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y}
                  (\x:real^3->bool. f X x))`);
 (EXPAND_TAC "f" THEN REFL_TAC);
 (REWRITE_WITH 
  `sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y} (\x. f X x)) = 
   sum T2 (\x. sum {X | X IN B1 /\ critical_edgeX V X x} (\X. f X x))`);
 (ASM_SIMP_TAC[SUM_SUM_RESTRICT]);

 (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (REWRITE_TAC[MESON[] `(A/\B/\C)/\D <=> A/\B/\C/\D`]);
 (REWRITE_WITH 
`sum T2 (\x. sum
               {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
                   ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
        (\X. f X x)) = 
 sum T2  (\x. sum {X | mcell_set V X /\
                     ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
      (\X. f X x)) - 
sum T2  (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
                      ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
      (\X. f X x))`);
 (REWRITE_TAC[REAL_ARITH `a = b - c <=> b = a + c`]);
 (REWRITE_WITH 
` sum T2
 (\x. sum
      {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
           ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
      (\X. f X x)) +
 sum T2
 (\x. sum
      {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
           ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
      (\X. f X x)) = 
 sum T2 
 (\x. (\x. sum
      {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
           ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
      (\X. f X x)) x + 
(\x. sum
      {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
           ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
      (\X. f X x)) x)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC SUM_ADD);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SUM_EQ);
 (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC);

 (REWRITE_WITH 
`sum
 {X | X SUBSET ball (vec 0,r) /\
      mcell_set V X /\
      ~(critical_edgeX V X = {}) /\
      critical_edgeX V X x}
 (\X. f X x) +
 sum
 {X | ~(X SUBSET ball (vec 0,r)) /\
      mcell_set V X /\
      ~(critical_edgeX V X = {}) /\
      critical_edgeX V X x}
 (\X. f X x) = 
 sum ({X | X SUBSET ball (vec 0,r) /\
      mcell_set V X /\
      ~(critical_edgeX V X = {}) /\
      critical_edgeX V X x} UNION 
      {X | ~(X SUBSET ball (vec 0,r)) /\
      mcell_set V X /\
      ~(critical_edgeX V X = {}) /\
      critical_edgeX V X x}) 
 (\X. f X x)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC SUM_UNION);
 (REPEAT STRIP_TAC);

 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `B1:(real^3->bool)->bool`);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "B1" THEN SET_TAC[]);

 (UP_ASM_TAC THEN EXPAND_TAC "T2");
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
 (STRIP_TAC);
 (ASM_SIMP_TAC[Marchal_cells_3.FINITE_MCELL_SET_LEMMA]);
 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `x SUBSET VX V x'`);
 (UNDISCH_TAC `critical_edgeX V x' x` THEN REWRITE_TAC[critical_edgeX;edgeX]);
 (REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[ASSUME `x = {u, v:real^3}`; ASSUME `{u, v:real^3} = {u', v'}`]);
 (SET_TAC[ASSUME `VX V x' u'`; ASSUME `VX V x' v'`]);
 (NEW_GOAL `VX V x' = V INTER x'`);
 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM; IN]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `VX V x' = {}`);
 (ASM_REWRITE_TAC[VX]);
 (UNDISCH_TAC `x SUBSET VX V x'` THEN REWRITE_TAC[ASSUME `VX V x' = {}`]);
 (REWRITE_TAC[ASSUME `x = {u0, u1:real^3}`] THEN SET_TAC[]);
 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`; IN_BALL]);
 (NEW_GOAL `dist (vec 0, x'') <= dist (vec 0, u0:real^3) + dist (u0, x'')`);
 (NORM_ARITH_TAC);
 (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
 (REWRITE_TAC[GSYM IN_BALL]);
 (UNDISCH_TAC `(T1:real^3->bool) u0` THEN EXPAND_TAC "T1");
 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`] THEN SET_TAC[]);
 (NEW_GOAL `dist (u0, x'':real^3) < &8`);
 (REWRITE_TAC[GSYM IN_BALL]);
 (NEW_GOAL `x' SUBSET ball (u0:real^3,&8)`);
 (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM; IN]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC MCELL_SUBSET_BALL8);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[GSYM (ASSUME `x' = mcell i V ul`)]);
 (UNDISCH_TAC `x SUBSET VX V x'` THEN UNDISCH_TAC `VX V x' = V INTER x'`);
 (ASM_REWRITE_TAC[]);
 (SET_TAC[]);
 (SUBGOAL_THEN `(x'':real^3) IN x'` MP_TAC);
 (UNDISCH_TAC `(x':real^3->bool) x''` THEN SET_TAC[]);
 (UP_ASM_TAC THEN SET_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (SET_TAC[]);

 (REWRITE_WITH ` ({X | X SUBSET ball (vec 0,r) /\
       mcell_set V X /\
       ~(critical_edgeX V X = {}) /\
       critical_edgeX V X x} UNION
  {X | ~(X SUBSET ball (vec 0,r)) /\
       mcell_set V X /\
       ~(critical_edgeX V X = {}) /\
       critical_edgeX V X x}) = 
 {X | mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}`);
 (SET_TAC[]);
 (REWRITE_WITH 
  `(\x. sum
      {X | mcell_set V X /\
           ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) = 
    (\x. sum
      {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`);
 (REWRITE_TAC[FUN_EQ_THM]);
 (STRIP_TAC);
 (REWRITE_WITH 
`{X | mcell_set V X /\
      ~(!x. critical_edgeX V X x <=> {} x) /\ critical_edgeX V X x} = 
 {X | mcell_set V X /\ critical_edgeX V X x}`);
 (REWRITE_TAC[SET_RULE `A = B <=> A SUBSET B /\ B SUBSET A`]);
 (STRIP_TAC);
 (SET_TAC[]);
 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (REWRITE_TAC[MESON[IN] `(A:(real^3->bool)->bool) x <=> x IN A`]);
 (SET_TAC[]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH 
  ` (\x. sum
      {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
           ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) = 
     (\x. sum
      {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
           critical_edgeX V X x} (\X. f X x))`);
 (REWRITE_TAC[FUN_EQ_THM]);
 (STRIP_TAC);
 (REWRITE_WITH 
`{X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
      ~(!x. critical_edgeX V X x <=> {} x) /\ critical_edgeX V X x} = 
 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}`);
 (REWRITE_TAC[SET_RULE `A = B <=> A SUBSET B /\ B SUBSET A`]);
 (STRIP_TAC);
 (SET_TAC[]);
 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
 (GEN_TAC THEN DISCH_TAC);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (REWRITE_TAC[MESON[IN] `(A:(real^3->bool)->bool) x <=> x IN A`]);
 (SET_TAC[]);

(* OK here *)

 (MATCH_MP_TAC (REAL_ARITH `(?x. c <= x /\ a + x <= b) ==> a <= b - c`));
 (EXISTS_TAC `dd * r pow 2`); 
 (STRIP_TAC);

 (ABBREV_TAC 
   `T3:real^3->bool = V INTER ball (vec 0, r) DIFF ball (vec 0, r - &8)`);
 (ABBREV_TAC `T4 = {{u0:real^3, u1} | u0 IN T3 /\ u1 IN T3 /\ 
                                      ~(u0 = u1) /\ hl [u0; u1] <= hplus}`);
 (REWRITE_WITH `sum T2
 (\x. sum
      {X | ~(X SUBSET ball (vec 0,r)) /\
           mcell_set V X /\
           critical_edgeX V X x}
      (\X. f X x)) =  sum T4
 (\x. sum
      {X | ~(X SUBSET ball (vec 0,r)) /\
           mcell_set V X /\
           critical_edgeX V X x}
      (\X. f X x))`);
 
 (EXPAND_TAC "T2");
 (MATCH_MP_TAC SUM_SUPERSET);
 (STRIP_TAC);
 (EXPAND_TAC "T4" THEN EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN SET_TAC[]);

 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (REWRITE_WITH 
  `{X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} =
   {}`);
 (REWRITE_TAC[SET_RULE `x = {} <=> ~(?s. s IN x)`]);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN STRIP_TAC);

 (NEW_GOAL `(x:real^3->bool) SUBSET s`);
 (MATCH_MP_TAC CRITICAL_EDGEX_SUBSET_MCELL);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);

 (NEW_GOAL `?p:real^3. p IN s DIFF ball (vec 0,r)`);
 (UNDISCH_TAC `~(s SUBSET ball ((vec 0):real^3,r))` THEN SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_DIFF; IN_BALL; REAL_ARITH 
   `~(a < r) <=> r <= a`] THEN STRIP_TAC);
 (NEW_GOAL `s SUBSET ball (p:real^3,&8)`);
 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `u0:real^3 IN ball (p,&8) /\ u1 IN ball (p,&8)`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN STRIP_TAC);
 (UNDISCH_TAC `~(T4:(real^3->bool)->bool) x`);
 (REWRITE_TAC[MESON[IN] `(T4:(real^3->bool)->bool) x <=> x IN T4`]);
 (EXPAND_TAC "T4" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[IN_INTER; IN_DIFF; IN_BALL]);
 (REWRITE_TAC[IN; IN_ELIM_THM]);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `(T1:(real^3->bool)) u0` THEN 
   UNDISCH_TAC `(T1:(real^3->bool)) u1`);
 (REWRITE_WITH `!x. T1 x <=> x:real^3 IN T1`);
 (ASM_REWRITE_TAC[IN]);
 (EXPAND_TAC "T1" THEN REWRITE_TAC[IN_INTER; IN_BALL]);
 (REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `dist (vec 0,p) <= dist (p, u0) + dist (vec 0, u0:real^3)`);
 (NORM_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `dist (vec 0,p) <= dist (p, u1) + dist (vec 0, u1:real^3)`);
 (NORM_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[SUM_CLAUSES]);

 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
 (EXISTS_TAC `sum T4 (\x:real^3->bool. cc2 * cc1)`);
 (STRIP_TAC);
 (MATCH_MP_TAC SUM_LE);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{{u0:real^3, u1} | u0 IN T3 /\ u1 IN T3}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN T3 /\ u1 IN T3}`);
 (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
 (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_IMAGE);
 (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:real^3->bool`);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN 
   REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `u0:real^3, u1:real^3` THEN ASM_REWRITE_TAC[]);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[IN] THEN EXPAND_TAC "T4" THEN EXPAND_TAC "T3" THEN
   REWRITE_TAC[ABS_SIMP; IN_DIFF; IN_INTER; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);

 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
 (EXISTS_TAC 
 `sum {X| ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}  
  (\x. cc1)`);
 (STRIP_TAC);
 (MATCH_MP_TAC SUM_LE);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | mcell_set V X /\ edgeX V X x}`);
 (STRIP_TAC);
 (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 (REWRITE_TAC[critical_edgeX] THEN SET_TAC[]);
 (REWRITE_TAC[BETA_THM; ABS_SIMP; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (EXPAND_TAC "f");
 (NEW_GOAL `critical_weight V x' <= &1`);
 (REWRITE_TAC[critical_weight]);
 (REWRITE_WITH `&1 / &(CARD (critical_edgeX V x')) <= &1 <=> 
                 &1  <= &(CARD (critical_edgeX V x'))`);
 (MATCH_MP_TAC Packing3.REAL_DIV_LE_1);
 (REWRITE_TAC[REAL_OF_NUM_LT; ARITH_RULE `0 < a <=> ~(a = 0)`]);
 (REWRITE_WITH `CARD (critical_edgeX V x') = 0 <=> critical_edgeX V x' = {}`);
 (MATCH_MP_TAC CARD_EQ_0);
 (REWRITE_TAC[critical_edgeX; edgeX] THEN MATCH_MP_TAC FINITE_SUBSET);

 (EXISTS_TAC `{{u0:real^3, u1} | u0 IN VX V x' /\ u1 IN VX V x'}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN VX V x' /\ u1 IN VX V x'}`);
 (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
 (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_IMAGE);
 (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
 (MATCH_MP_TAC FINITE_VX);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN 
   REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `u0':real^3, u1':real^3` THEN ASM_REWRITE_TAC[]);
 (EXISTS_TAC `u0':real^3` THEN EXISTS_TAC `u1':real^3` THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN SET_TAC[]);
 (REWRITE_TAC[REAL_OF_NUM_LE; ARITH_RULE `1 <= a <=> ~(a = 0)`]);
 (REWRITE_WITH `CARD (critical_edgeX V x') = 0 <=> critical_edgeX V x' = {}`);
 (MATCH_MP_TAC CARD_EQ_0);
 (REWRITE_TAC[critical_edgeX; edgeX] THEN MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{{u0:real^3, u1} | u0 IN VX V x' /\ u1 IN VX V x'}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN VX V x' /\ u1 IN VX V x'}`);
 (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
 (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_IMAGE);
 (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
 (MATCH_MP_TAC FINITE_VX);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN 
   REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `u0':real^3, u1':real^3` THEN ASM_REWRITE_TAC[]);
 (EXISTS_TAC `u0':real^3` THEN EXISTS_TAC `u1':real^3` THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN SET_TAC[]);
 (NEW_GOAL `&0 <= critical_weight V x'`);
 (REWRITE_TAC[critical_weight] THEN MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_TAC[REAL_ARITH `&0 <= &1`; REAL_OF_NUM_LE]);
 (ARITH_TAC);
 (NEW_GOAL `gammaX V x' lmfun <= cc1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `gammaX V x' lmfun * critical_weight V x' <= cc1 * critical_weight V x'`);

 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
 (MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC);

 (NEW_GOAL `cc1 * critical_weight V x' <= cc1`);
 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 (REWRITE_WITH `!x b. b - b * x = b * (&1 - x)`);
 (REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_WITH 
 `sum
  {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}
  (\x. cc1) = 
 &(CARD
   {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}) 
   * cc1`);
 (MATCH_MP_TAC SUM_CONST);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | mcell_set V X /\ edgeX V X x}`);
 (STRIP_TAC);
 (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 (REWRITE_TAC[critical_edgeX] THEN SET_TAC[]);

 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 (REWRITE_TAC[REAL_ARITH `a * x - b * x = x * (a - b)`]);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL 
  ` &(CARD
     {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x})
    <=  &(CARD {X | mcell_set V X /\ VX V X u0})`);
 (REWRITE_TAC[REAL_OF_NUM_LE] THEN MATCH_MP_TAC CARD_SUBSET);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM]);
 (SET_TAC[]);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (u0,&8) /\ mcell_set V X}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
 (ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[SUBSET]);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `VX V x' = V INTER x'`);
 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 (UNDISCH_TAC `mcell_set V x'` THEN 
   REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (UNDISCH_TAC `VX V x' u0` THEN ASM_REWRITE_TAC[VX]);
 (REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= cc2`);
 (ASM_MESON_TAC[]);

 (ABBREV_TAC `s1_temp = &(CARD
       {X | ~(X SUBSET ball (vec 0,r)) /\
            mcell_set V X /\
            critical_edgeX V X x})`);
 (ABBREV_TAC `s2_temp = &(CARD {X | mcell_set V X /\ VX V X u0})`);
 (ASM_REAL_ARITH_TAC);

 (ABBREV_TAC `g = (\x:real^3->bool. cc2 * cc1)`);

 (REWRITE_WITH 
  `sum T4 (g:(real^3->bool)->real) = 
   &1 / &2 * 
   sum {m,n | m IN T3 /\ n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
   (\(m:real^3,n). g {m, n})`);
 (ONCE_REWRITE_TAC[REAL_ARITH `a = &1 / &2 * b <=> b = &2 * a`]);
 (EXPAND_TAC "T4");
 (REWRITE_TAC[HL_2; REAL_ARITH `inv (&2) * a <= b <=> a <= &2 * b`]);
 (MATCH_MP_TAC SUM_PAIR_2_SET);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:real^3->bool`);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[REAL_ARITH `&1 / &2 * s <= t <=> s <= &2 * t`]);

 (ABBREV_TAC 
  `h = (\m:real^3. {n | n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus})`);
 (REWRITE_WITH 
  `{m,n | m IN T3 /\ n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} =   
   {m:real^3,n | m IN T3 /\ n IN h m}`);
 (EXPAND_TAC "h");
 (SET_TAC[PAIR_EQ]);
 (ABBREV_TAC `k = (\m n. (g:(real^3->bool)->real) {m,n})`);
 (REWRITE_WITH `(\(m,n). (g:(real^3->bool)->real) {m, n}) = (\(m,n). k m n)`);
 (REWRITE_TAC[FUN_EQ_THM]);
 (STRIP_TAC);
 (NEW_GOAL `(x:real^3#real^3) = FST x, SND x`);
 (REWRITE_TAC[PAIR]);
 (ONCE_REWRITE_TAC[ASSUME `(x:real^3#real^3) = FST x, SND x`]);
 (EXPAND_TAC "k" THEN REWRITE_TAC[]);
 (REWRITE_WITH 
  `sum {m:real^3,n:real^3 | m IN T3 /\ n IN h m} (\(m,n). k m n)  = 
   sum T3 (\m. sum (h m) (k m))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC SUM_SUM_PRODUCT);
 (STRIP_TAC);

 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:real^3->bool`);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (REPEAT STRIP_TAC);
 (EXPAND_TAC "h");

 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T3:real^3->bool`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:real^3->bool`);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (SET_TAC[]);

 (EXPAND_TAC "k" THEN EXPAND_TAC "g");
 (NEW_GOAL `sum T3 (\m. sum ((h:real^3->real^3->bool) m) (\n. cc2 * cc1)) <= 
             sum T3 (\m. (&4) pow 3 * cc2 * cc1)`);
 (MATCH_MP_TAC SUM_LE);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:real^3->bool`);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (EXPAND_TAC "h" THEN REPEAT STRIP_TAC THEN REWRITE_TAC[]);
 (REWRITE_WITH 
 `sum {n:real^3 | n IN T3 /\ ~(x = n) /\ 
                  dist (x,n) <= &2 * hplus} (\n. cc2 * cc1) =
  &(CARD {n | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus}) * 
  (cc2 * cc1)`);
 (MATCH_MP_TAC SUM_CONST);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T3:real^3->bool`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:real^3->bool`);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (SET_TAC[]);

 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `(a <= b <=> &0 <= b - a)`)]);


 (NEW_GOAL 
   `&(CARD {n | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus}) <= 
    &(CARD (V INTER ball (x:real^3, &3)))`);
 (REWRITE_TAC[REAL_OF_NUM_LE]);
 (MATCH_MP_TAC CARD_SUBSET);
 (STRIP_TAC);
 (EXPAND_TAC "T3" THEN REWRITE_TAC[IN_DIFF; IN_BALL]);
 (REWRITE_TAC[IN_INTER; IN_BALL; IN_ELIM_THM; SUBSET; IN]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `&2 * hplus < &3`);
 (REWRITE_TAC[hplus] THEN REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `&(CARD (V INTER ball (x:real^3,&3))) <= &4 pow 3`);
 (REWRITE_TAC[REAL_ARITH `&4 = &3 + &1`]);
 (MATCH_MP_TAC BOUNDS_VGEN_klemma);
 (ASM_REWRITE_TAC[REAL_ARITH `&0 <= &3`]);
 (ABBREV_TAC 
 `s1 = &(CARD {n:real^3 | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus})`);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `sum T3 (\m:real^3. &4 pow 3 * cc2 * cc1) <= &2 * dd * r pow 2`);
 (REWRITE_WITH 
  `sum T3 (\m:real^3. &4 pow 3 * cc2 * cc1) = 
   &(CARD T3) * &4 pow 3 * cc2 * cc1`);
 (MATCH_MP_TAC SUM_CONST);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:real^3->bool`);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (EXPAND_TAC "dd");

 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 (REWRITE_TAC[REAL_ARITH 
 `&2 * (&1 / &2 * dd2 * &4 pow 3 * cc2 * cc1) * r pow 2 -
 &(CARD (T3:real^3->bool)) * &4 pow 3 * cc2 * cc1 = 
  (&4 pow 3 * cc2 * cc1) * (dd2 * r pow 2 - &(CARD T3))`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH `&0 <= &4 pow 3 * x <=> &0 <= x`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC);
 (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `(a <= b <=> &0 <= b - a)`)]);
 (EXPAND_TAC "T3");

 (ONCE_REWRITE_TAC[SET_RULE `A INTER B DIFF C = A INTER B DIFF A INTER C`]);
 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
 (EXISTS_TAC `dd1 * r pow 2`);
 (STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b ) * x`]);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[REAL_LE_POW_2]);
 (ASM_REAL_ARITH_TAC);

(* ======================================================================== *)
(* CHECK DEN DAY LA OK ROI - (._o) (0_o) *)
(* ==================================================================== *)

 (REWRITE_WITH 
 `sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x)) = 
  sum T2 (\e. cluster_gammaX V e (cell_cluster V e)) - 
  sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))`);
 (REWRITE_TAC[REAL_ARITH `a = b - c <=> b = a + c`]);
 (ABBREV_TAC 
 `f1 = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`);
 (ABBREV_TAC 
 `f2 = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))`);
 (REWRITE_WITH 
 `sum T2 (\e. cluster_gammaX V e (cell_cluster V e)) = 
  sum T2 (\e:real^3->bool. f1 e + f2 e)`);
 (MATCH_MP_TAC SUM_EQ);
 (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN REWRITE_TAC[cluster_gammaX; cell_cluster]);
 (REWRITE_TAC[FUN_EQ_THM] THEN REPEAT STRIP_TAC);
 (EXPAND_TAC "f");
 (REWRITE_TAC[SET_RULE `{X | x IN critical_edgeX V X /\ mcell_set V X} = 
                         {X | mcell_set V X /\ critical_edgeX V X x}`]);
 (MATCH_MP_TAC SUM_ADD);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (u0,&8) /\ mcell_set V X}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
 (ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[SUBSET]);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `VX V x' = V INTER x'`);
 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 (UNDISCH_TAC `mcell_set V x'` THEN 
   REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (UNDISCH_TAC `critical_edgeX V x' x` THEN 
   REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM] THEN STRIP_TAC);
 (NEW_GOAL `VX V x' u0`);
 (NEW_GOAL `u0 = u' \/ u0 = v':real^3`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_TAC[ASSUME `u0 = u':real^3`]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `u0 = v':real^3`]);
 (ASM_REWRITE_TAC[]);

 (UNDISCH_TAC `VX V x' u0` THEN ASM_REWRITE_TAC[VX]);
 (REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
 (SET_TAC[]);

 (NEW_GOAL `VX V x' u0`);
 (UNDISCH_TAC `mcell_set V x'` THEN 
   REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (UNDISCH_TAC `critical_edgeX V x' x` THEN 
   REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM] THEN STRIP_TAC);
 (NEW_GOAL `u0 = u' \/ u0 = v':real^3`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_TAC[ASSUME `u0 = u':real^3`]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `u0 = v':real^3`]);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SUM_ADD);
 (ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC (REAL_ARITH `&0 <= a /\ b + x <= &0 ==> x <= a - b`));
 (STRIP_TAC);
 (MATCH_MP_TAC SUM_POS_LE);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);

 (UNDISCH_TAC `cell_cluster_estimate V`);
 (REWRITE_TAC[cell_cluster_estimate]);
 (REWRITE_TAC[REAL_ARITH `&0 <= a <=> a >= &0`] THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);

 (ABBREV_TAC 
  `f1 = (\x. sum {X | X SUBSET ball (vec 0, r + &8) /\ 
                      ~(X SUBSET ball (vec 0, r - &8)) /\
                      mcell_set V X /\
                      critical_edgeX V X x} (beta_bump V x))`);
 (ABBREV_TAC 
  `f2 = (\x. sum {X | X SUBSET ball (vec 0, r - &8) /\ mcell_set V X /\
                      critical_edgeX V X x} (beta_bump V x))`);
 (REWRITE_WITH 
  `sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))
   = sum (T2:(real^3->bool)->bool) f1 + sum T2 f2`);
 (REWRITE_WITH 
  `sum (T2:(real^3->bool)->bool) f1 + sum T2 f2 = sum T2 (\x. f1 x + f2 x)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC SUM_ADD);
 (ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC SUM_EQ);
 (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (EXPAND_TAC "f1" THEN EXPAND_TAC "f2");
 (ABBREV_TAC 
 `s1 = {X | X SUBSET ball (vec 0,r + &8) /\ ~(X SUBSET ball (vec 0,r - &8)) /\
            mcell_set V X /\ critical_edgeX V X x}`);
 (ABBREV_TAC `s2 = {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X /\
                         critical_edgeX V X x}`);
 (REWRITE_WITH `{X | mcell_set V X /\ critical_edgeX V X x} = s1 UNION s2`);
 (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN 
   REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; IN_ELIM_THM; IN]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `x' SUBSET ball ((vec 0):real^3,r - &8)`);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[SUBSET; IN_DIFF; IN_BALL]);
 (REPEAT STRIP_TAC);

 (NEW_GOAL `x' SUBSET ball (u0:real^3, &8)`);
 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);

 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `x:real^3->bool SUBSET x'`);
 (MATCH_MP_TAC CRITICAL_EDGEX_SUBSET_MCELL);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (SET_TAC[]);
 (NEW_GOAL `dist (u0:real^3, x'') < &8`);
 (REWRITE_TAC[GSYM IN_BALL] THEN ASM_SET_TAC[]);
 (NEW_GOAL `dist (vec 0, x'') <= dist (u0, x'') + dist (vec 0, u0:real^3)`);
 (NORM_ARITH_TAC);
 (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
 (REWRITE_TAC[GSYM IN_BALL]);
 (UNDISCH_TAC `(T1:real^3->bool) u0`);
 (EXPAND_TAC "T1" THEN REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
 (SET_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[]);

 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SUM_UNION);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
 (STRIP_TAC);
 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA_2]);
 (ASM_SET_TAC[]);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X}`);
 (STRIP_TAC);
 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA_2]);
 (ASM_SET_TAC[]);

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

 (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN SET_TAC[]);

 (REWRITE_WITH `sum (T2:(real^3->bool)->bool) f2 = &0`);
 (EXPAND_TAC "f2");
 (REWRITE_TAC[SET_RULE 
  `!V r x. {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X /\
                         critical_edgeX V X x} = 
           {X | X IN {X| X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
                         critical_edgeX V X x}`]);
 (REWRITE_WITH 
 `sum T2
  (\x. sum
      {X | X IN {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
           critical_edgeX V X x}
      (beta_bump V x)) = 
 sum T2
  (\x. sum
      {X | X IN {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
           critical_edgeX V X x}
      (\X. beta_bump V x X))`);
 (REWRITE_WITH `!x V. (\X. beta_bump V x X) = beta_bump V x`);
 (REWRITE_TAC[FUN_EQ_THM] THEN ASM_REWRITE_TAC[]);

 (ABBREV_TAC `t = {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X}`);
 (ABBREV_TAC `g = beta_bump V`);
 (ABBREV_TAC `s = T2:(real^3->bool)->bool`);
 (REWRITE_WITH 
   `sum s (\x. sum {X | X IN t /\ critical_edgeX V X x} (\X. g x X)) = 
    sum t (\X. sum {x | x IN s /\ critical_edgeX V X x} (\x. g x X))`);
 (MATCH_MP_TAC SUM_SUM_RESTRICT);
 (STRIP_TAC);
 (EXPAND_TAC "s" THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "t");
 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "s" THEN EXPAND_TAC "t" THEN EXPAND_TAC "g");
 (MATCH_MP_TAC SUM_EQ_0);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC);

 (REWRITE_WITH `{x' | T2 x' /\ critical_edgeX V x x'} = 
                 {x' | x' IN critical_edgeX V x}`);
 (MATCH_MP_TAC (SET_RULE `A SUBSET B /\ B SUBSET A ==> A = B`));
 (STRIP_TAC);
 (SET_TAC[]);
 (ASM_REWRITE_TAC[IN]);
 (REWRITE_TAC[GSYM (ASSUME `{{u0:real^3, u1} | u0 IN T1 /\ u1 IN T1 /\ 
                             ~(u0 = u1) /\ hl [u0; u1] <= hplus} = s`)]);

 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; critical_edgeX; edgeX]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3` THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "T1");
 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`; IN_INTER; IN_BALL]);
 (NEW_GOAL `VX V x = V INTER x`);
 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[IN]);
 (STRIP_TAC THEN UNDISCH_TAC `VX V x u'`);
 (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);
 (REWRITE_WITH `u':real^3 IN V /\ v' IN V`);
 (ASM_SET_TAC[]);
 (REPEAT STRIP_TAC);

 (NEW_GOAL `u':real^3 IN ball (vec 0, r - &8)`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN REAL_ARITH_TAC);
 (NEW_GOAL `v':real^3 IN ball (vec 0, r - &8)`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN REAL_ARITH_TAC);
 (REWRITE_WITH `hl [u'; v':real^3] = hl [u; v:real^3]`);
 (REWRITE_TAC[HL; set_of_list]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);
 (ASM_REWRITE_TAC[]);
 (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SUM_BETA_BUMP_LEMMA);
 (ASM_REWRITE_TAC[]);

 (REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
 (EXPAND_TAC "T2");
 (REWRITE_TAC[HL_2; REAL_ARITH `inv (&2) * a <= b <=> a <= &2 * b`]);
 (REWRITE_WITH 
 `sum {{u0:real^3, u1} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\ 
                         dist (u0,u1) <= &2 * hplus} f1 = 
 &1 / &2 * 
 sum {m,n | m IN T1 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
     (\(m,n). f1 {m, n})`);
 (REWRITE_TAC[REAL_ARITH `a = &1 / &2 * b <=> b = &2 * a`]);
 (MATCH_MP_TAC SUM_PAIR_2_SET);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
 (ASM_REWRITE_TAC[]);

 (ABBREV_TAC 
  `T3 = V INTER ball ((vec 0):real^3,r) DIFF ball (vec 0, r - &16)`);
 (REWRITE_WITH 
  `sum {m:real^3,n | m IN T1 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
     (\(m,n). f1 {m, n}) = 
   sum {m,n | m IN T3 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
 (\(m,n). f1 {m, n})`);
 (MATCH_MP_TAC SUM_SUPERSET);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN 
   REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3` THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "T1" THEN UNDISCH_TAC 
   `(V INTER ball ((vec 0):real^3,r) DIFF ball (vec 0,r - &16)) m` THEN     
   REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
 (SET_TAC[]);
 (EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "f1");
 (REWRITE_WITH 
 `{X | X SUBSET ball (vec 0,r + &8) /\
       ~(X SUBSET ball (vec 0,r - &8)) /\
       mcell_set V X /\
       critical_edgeX V X {m, n}} = {}`);
 (REWRITE_TAC[SET_RULE `y = {} <=> ~(?x. x IN y)`]);
 (REPEAT STRIP_TAC);
 (UNDISCH_TAC `~(?m n.
            ((V INTER ball (vec 0,r) DIFF ball (vec 0,r - &16)) m /\
             (V INTER ball (vec 0,r)) n /\
             ~(m = n) /\
             dist (m:real^3,n) <= &2 * hplus) /\
            x = m,n) ` THEN REWRITE_TAC[]);
 (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
 (EXPAND_TAC "T3" THEN REWRITE_TAC[IN_DIFF; IN; IN_BALL]);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?p:real^3. p IN x' /\ ~(p IN ball (vec 0,r - &8))`);
 (UNDISCH_TAC `~(x' SUBSET ball ((vec 0):real^3,r - &8))`);
 (SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL]);
 (NEW_GOAL `x' SUBSET ball (p:real^3, &8)`);
 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `m:real^3 IN x'`);
 (UNDISCH_TAC `critical_edgeX V x' {m, n}` THEN 
   REWRITE_TAC[critical_edgeX; edgeX; IN_ELIM_THM; IN]);
 (REPEAT STRIP_TAC);

 (NEW_GOAL `VX V x' = V INTER x'`);
 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[IN]);
 (STRIP_TAC THEN UNDISCH_TAC `VX V x' u'`);
 (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);

 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
 (ASM_SET_TAC[]);
 (NEW_GOAL `dist (p, m:real^3) < &8`);
 (REWRITE_TAC[GSYM IN_BALL]);
 (ASM_SET_TAC[]);
 (NEW_GOAL `dist (vec 0, p) <= dist (vec 0, m:real^3) + dist (p, m)`);
 (NORM_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[SUM_CLAUSES]);

 (ABBREV_TAC 
  `g = (\m:real^3. {n | n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus})`);
 (REWRITE_WITH 
  `{m,n | m IN T3 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} = 
   {m,n:real^3 | m IN T3 /\ n IN g m}`);
 (EXPAND_TAC "g" THEN ASM_REWRITE_TAC[] THEN SET_TAC[]);
 (ABBREV_TAC `h = (\m. (\n. (f1:(real^3->bool)->real) {m, n}))`);
 (REWRITE_WITH `(\(m,n). (f1:(real^3->bool)->real) {m, n}) = 
                 (\(m,n). h m n)`);
 (REWRITE_TAC[FUN_EQ_THM]);
 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `x:real^3#real^3 = FST x, SND x`);
 (REWRITE_TAC[PAIR]);
 (ONCE_ASM_REWRITE_TAC[]);
 (EXPAND_TAC "h" THEN REWRITE_TAC[]);

 (REWRITE_WITH `sum {m,n | m IN T3 /\ n IN g m} (\(m,n). h m n) = 
                 sum T3 (\m. sum (g m) ((h:real^3->real^3->real) m))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC SUM_SUM_PRODUCT);
 (STRIP_TAC);

 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "T3" THEN SET_TAC[]);

 (REPEAT STRIP_TAC);
 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "T1" THEN SET_TAC[]);

 (NEW_GOAL 
  `sum T3 (\m. sum ((g:real^3->real^3->bool) m) (h m)) <= 
   sum T3 (\n:real^3. ss1)`);
 (MATCH_MP_TAC SUM_LE);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "T3" THEN SET_TAC[]);
 (REPEAT STRIP_TAC THEN REWRITE_TAC[]);

 (NEW_GOAL `sum ((g:real^3->real^3->bool) x) (h x) <= sum (g x) (\x. cc4 * cc3)`);
 (MATCH_MP_TAC SUM_LE);
 (STRIP_TAC);
 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "T1" THEN SET_TAC[]);

 (REPEAT STRIP_TAC THEN EXPAND_TAC "h" THEN REWRITE_TAC[]);
 (EXPAND_TAC "f1");
 (ABBREV_TAC `S1 = {X | X SUBSET ball (vec 0,r + &8) /\
      ~(X SUBSET ball (vec 0,r - &8)) /\
      mcell_set V X /\
      critical_edgeX V X {x, x'}}`);
 (NEW_GOAL `sum (S1:(real^3->bool)->bool) (beta_bump V {x, x'}) <= 
             sum S1 (\x. cc3)`);
 (MATCH_MP_TAC SUM_LE);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
 (STRIP_TAC);
 (REPEAT STRIP_TAC THEN REWRITE_TAC[]);
 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "S1" THEN SET_TAC[]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (UP_ASM_TAC THEN EXPAND_TAC "S1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (STRIP_TAC THEN ASM_REWRITE_TAC[]);

 (NEW_GOAL `sum S1 (\x:real^3->bool. cc3) = &(CARD S1) * cc3`);
 (MATCH_MP_TAC SUM_CONST);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
 (STRIP_TAC);
 (REPEAT STRIP_TAC THEN REWRITE_TAC[]);
 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "S1" THEN SET_TAC[]);
 (NEW_GOAL `&(CARD (S1:(real^3->bool)->bool)) <= cc4`);
 (NEW_GOAL `&(CARD (S1:(real^3->bool)->bool)) <= 
             &(CARD {X | mcell_set V X /\ VX V X x})`);
 (REWRITE_TAC[REAL_OF_NUM_LE]);
 (MATCH_MP_TAC CARD_SUBSET);
 (STRIP_TAC);
 (EXPAND_TAC "S1" THEN 
   REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; critical_edgeX; edgeX] THEN 
   REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `x:real^3 = u' \/ x = v'`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | X SUBSET ball (x:real^3, &8) /\ mcell_set V X}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
 (NEW_GOAL `VX V x'' = V INTER x''`);
 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 (UNDISCH_TAC `mcell_set V x''` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[IN]);
 (STRIP_TAC THEN UNDISCH_TAC `VX V x'' x`);
 (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);
 (NEW_GOAL `x'' SUBSET ball (x:real^3, &8)`);
 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X x}) <= cc4`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `x IN (T3:real^3->bool)` THEN EXPAND_TAC "T3");
 (SET_TAC[]);
 (ABBREV_TAC `s_temp = &(CARD {X | mcell_set V X /\ VX V X x})`);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `sum (S1:(real^3->bool)->bool) (\x. cc3) <= cc4 * cc3`);
 (ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
 (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (ABBREV_TAC `s_temp = sum (S1:(real^3->bool)->bool) (\x. cc3)`);
 (ASM_REAL_ARITH_TAC);



 (NEW_GOAL `sum ((g:real^3->real^3->bool) x) (\x. cc4 * cc3) <= ss1`);
 (REWRITE_WITH 
  `sum ((g:real^3->real^3->bool) x) (\x. cc4 * cc3) =
   &(CARD (g x)) * cc4 * cc3`);
 (MATCH_MP_TAC SUM_CONST);
 (EXPAND_TAC "g");
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:real^3->bool`);
 (STRIP_TAC);
 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
 (ASM_REWRITE_TAC[]);
 (SET_TAC[]);

 (NEW_GOAL `&(CARD ((g:real^3->real^3->bool) x)) <= 
             &(CARD (V INTER ball (x:real^3, &3)))`);
 (REWRITE_TAC[REAL_OF_NUM_LE]);
 (MATCH_MP_TAC CARD_SUBSET);
 (STRIP_TAC);
 (EXPAND_TAC "g" THEN EXPAND_TAC "T1" THEN 
   REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; IN_INTER; IN_BALL]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `&2 * hplus < &3`);
 (REWRITE_TAC[hplus] THEN REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);

 (EXPAND_TAC "ss1");
 (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
 (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `a <= b <=> &0 <= b - a`)]);
 (NEW_GOAL `&(CARD (V INTER ball (x:real^3,&3))) <= &4 pow 3`);
 (REWRITE_TAC[REAL_ARITH `&4 = &3 + &1`]);
 (MATCH_MP_TAC BOUNDS_VGEN_klemma);
 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC);

 (ASM_REAL_ARITH_TAC);

 (EXPAND_TAC "g");
 (REWRITE_TAC[REAL_ARITH `&1 / &2 * x + a <= &0 <=> x <= &2 * (-- a)`]);
 (REWRITE_TAC[REAL_ARITH `c * r pow 2 + d * r pow 2 = (c + d) * r pow 2`]);
 (REWRITE_WITH `(c:real) + dd = -- ss`);
 (EXPAND_TAC "c");
 (REAL_ARITH_TAC);
 (REWRITE_TAC[REAL_ARITH `&2 * --(--ss * r pow 2) = &2 * ss * r pow 2`]);
 (NEW_GOAL `sum T3 (\n:real^3. ss1) <= &2 * ss * r pow 2`);
 (REWRITE_WITH `sum T3 (\n:real^3. ss1) = &(CARD (T3)) * ss1`);
 (MATCH_MP_TAC SUM_CONST);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `(V:real^3->bool) INTER ball (vec 0,r)`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "T3" THEN SET_TAC[]);
 (EXPAND_TAC "ss");
 (REWRITE_TAC[REAL_ARITH 
   `&2 * (&1 / &2 * dd4 * ss1) * r pow 2 = (dd4 * r pow 2) * ss1`]);
 (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
 (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `a <= b <=> &0 <= b - a`)]);
 (EXPAND_TAC "T3");
 (ONCE_REWRITE_TAC[SET_RULE `A INTER B DIFF C = A INTER B DIFF A INTER C`]);

 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
 (EXISTS_TAC `dd3 * r pow 2`);
 (STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b ) * x`]);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[REAL_LE_POW_2]);
 (EXPAND_TAC "ss1");
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC);

 (REWRITE_WITH 
 `sum T3 (\m:real^3. sum {n | n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} 
         (h m)) =
  sum T3 (\m. sum (g m) (h m))`);
 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (EXISTS_TAC `&0`);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `~(saturated V /\ packing V)` THEN ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[])]);;