(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: KIZHLTL                                                  *)
(*      Chaper    : Packing (Marchal cells)                                  *)
(*                                                                           *)
(* ========================================================================= *)
(* KIZHLTL1                                                                  *)
(* ========================================================================  *)

module Kizhltl = struct


open Sphere;;
open Euler_main_theorem;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Pack2;;
open Packing3;;
open Rogers;; 
open Vukhacky_tactics;;
open Marchal_cells;;
open Emnwuus;;
(* open Marchal_cells_2;; *)
open Marchal_cells_2_new;;
open Urrphbz1;;
open Lepjbdj;;
open Hdtfnfz;;
open Rvfxzbu;;
open Sltstlo;;
open Urrphbz2;;
open Urrphbz3;;
open Ynhyjit;;
open Njiutiu;;
open Tezffsk;;
open Qzksykg;;
open Ddzuphj;;
open Ajripqn;;
open Qzyzmjc;;
open Upfzbzm_support_lemmas;;
open Marchal_cells_3;;
open Grutoti;;

let KIZHLTL1 = prove_by_refinement (KIZHLTL1_concl,  

[(GEN_TAC);
 (ASM_CASES_TAC `saturated V /\ packing (V:real^3->bool)`);
 (UP_ASM_TAC THEN STRIP_TAC);


 (NEW_GOAL `!r. &1 <= r
         ==> sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol <= 
             vol (ball (vec 0, r))`);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `S = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 (REWRITE_WITH `sum S vol = vol (UNIONS S)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS);
 (REPEAT STRIP_TAC);
 (EXPAND_TAC "S");
 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 (REWRITE_TAC[GSYM HAS_MEASURE_MEASURE]);
 (UP_ASM_TAC THEN EXPAND_TAC "S" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
 (REWRITE_TAC[mcell_set; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC MEASURABLE_MCELL);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN]);

 (ASM_CASES_TAC `~NULLSET (s INTER t)`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `s:real^3->bool IN S` THEN UNDISCH_TAC `t:real^3->bool IN S`);
 (EXPAND_TAC "S" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
 (REWRITE_TAC[mcell_set; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (NEW_GOAL `s = t:real^3->bool`);
 (REWRITE_TAC[ASSUME `t = mcell i V ul`; ASSUME `s = mcell i' V ul'`]);
 (ABBREV_TAC `j = if i <= 4 then i else 4`);
 (ABBREV_TAC `j' = if i' <= 4 then i' else 4`);
 (REWRITE_WITH `mcell i V ul = mcell j V ul`);
 (EXPAND_TAC "j" THEN COND_CASES_TAC);
 (REFL_TAC);
 (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`; 
   ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);
 (REWRITE_WITH `mcell i' V ul' = mcell j' V ul'`);
 (EXPAND_TAC "j'" THEN COND_CASES_TAC);
 (REFL_TAC);
 (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`; 
   ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);
 (REWRITE_WITH `j' = j /\ mcell j' V ul' = mcell j V ul`);
 (MATCH_MP_TAC Ajripqn.AJRIPQN);

 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[IN]);
 (ASM_MESON_TAC[IN]);
 (EXPAND_TAC "j'" THEN COND_CASES_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `i <= 4 <=> i=0\/i=1\/i=2\/i=3\/i=4`]
   THEN SET_TAC[]);
 (SET_TAC[]);
 (EXPAND_TAC "j" THEN COND_CASES_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `i <= 4 <=> i=0\/i=1\/i=2\/i=3\/i=4`]
   THEN SET_TAC[]);
 (SET_TAC[]);
 (UP_ASM_TAC);
 (REWRITE_WITH `mcell j V ul = mcell i V ul`);
 (EXPAND_TAC "j" THEN COND_CASES_TAC);
 (REFL_TAC);
 (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`; 
   ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);
 (REWRITE_WITH `mcell j' V ul' = mcell i' V ul'`);
 (EXPAND_TAC "j'" THEN COND_CASES_TAC);
 (REFL_TAC);
 (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`; 
   ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

 (MATCH_MP_TAC MEASURE_SUBSET);
 (REWRITE_TAC[MEASURABLE_BALL]);
 (REPEAT STRIP_TAC);
 (EXPAND_TAC "S" THEN MATCH_MP_TAC MEASURABLE_UNIONS);
 (REPEAT STRIP_TAC);
 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN;IN_ELIM_THM; mcell_set]);
 (REPEAT STRIP_TAC);
 (ASM_SIMP_TAC[MEASURABLE_MCELL]);
 (EXPAND_TAC "S" THEN SET_TAC[]);

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

 (NEW_GOAL `?c. !r. &1 <= r
         ==> vol (ball (vec 0, r)) + c * r pow 2 <= 
            sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 (EXISTS_TAC `-- (&24 / &3) * pi`);
 (REPEAT STRIP_TAC);

 (ASM_CASES_TAC `r < &6`);
 (NEW_GOAL `&0 <= sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 (MATCH_MP_TAC SUM_POS_LE);
 (ASM_SIMP_TAC[Packing3.KIUMVTC]);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC MEASURE_POS_LE);
 (ASM_SIMP_TAC[Pack1.measurable_voronoi]);

 (NEW_GOAL `vol (ball ((vec 0):real^3,r)) + (--(&24 / &3) * pi) * r pow 2 <= &0`);
 (REWRITE_TAC[REAL_ARITH `a + (--b * c) * d <= &0 <=> a <= b * c * d`]);
 (ASM_SIMP_TAC [VOLUME_BALL; REAL_ARITH `&1 <= r ==> &0 <= r`]);
 (REWRITE_TAC[REAL_ARITH `&4 / &3 * pi * r pow 3 <= &24 / &3 * pi * r pow 2
   <=> &0 <= &4 / &3 * pi * r pow 2 * (&6 - r)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_DIV THEN REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[PI_POS_LE]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[REAL_LE_POW_2]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);


 (NEW_GOAL `vol (ball (vec 0,r - &2)) <=  
   sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 (REWRITE_WITH 
   `sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u)) = 
    sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_closed V u))`);
 (MATCH_MP_TAC SUM_EQ);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[GSYM Pack2.MEASURE_VORONOI_CLOSED_OPEN]);

 (ABBREV_TAC `S:real^3->bool = V INTER ball (vec 0, r)`);
 (ABBREV_TAC `g = (\t:real^3. voronoi_closed V t)`);

 (REWRITE_WITH `sum S (\u:real^3. vol (voronoi_closed V u)) = sum S (\t. vol (g t))`);
 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
 (REWRITE_WITH `sum S (\t:real^3. vol (g t)) = measure (UNIONS (IMAGE g S))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "g");
 (REPEAT STRIP_TAC);
 (EXPAND_TAC "S");
 (ASM_SIMP_TAC[Packing3.KIUMVTC]);
 (MATCH_MP_TAC Pack2.MEASURABLE_VORONOI_CLOSED);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Pack2.NEGLIGIBLE_INTER_VORONOI_CLOSED);
 (ASM_SET_TAC[]);
 (EXPAND_TAC "g" THEN REWRITE_TAC[IMAGE]);
 (MATCH_MP_TAC MEASURE_SUBSET);
 (REWRITE_TAC[MEASURABLE_BALL]);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC MEASURABLE_UNIONS);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 (EXPAND_TAC "S");
 (ASM_SIMP_TAC[Packing3.KIUMVTC]);

 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Pack2.MEASURABLE_VORONOI_CLOSED);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUBSET; IN_BALL; IN_UNIONS]);
 (REPEAT STRIP_TAC);
 (MP_TAC (ASSUME `saturated (V:real^3->bool)`));
 (REWRITE_TAC[saturated] THEN STRIP_TAC);
 (NEW_GOAL `?y. y IN V /\ dist (x:real^3,y) < &2`);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `?v:real^3. v IN V /\ x IN voronoi_closed V v`);
 (MATCH_MP_TAC Packing3.TIWWFYQ);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);

 (EXISTS_TAC `voronoi_closed V (v:real^3)`);
 (ASM_REWRITE_TAC[]);

 (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 (EXISTS_TAC `v:real^3`);
 (STRIP_TAC);
 (EXPAND_TAC "S" THEN REWRITE_TAC[IN_INTER]);
 (ASM_REWRITE_TAC[IN_BALL]);

 (NEW_GOAL `dist (vec 0,v) <= dist (vec 0,x) + dist (x, v:real^3)`);
 (REWRITE_TAC[DIST_TRIANGLE]);
 (NEW_GOAL `dist (x, v:real^3) < &2`);
 (NEW_GOAL `dist (x, v) <= dist (x, y:real^3)`);
 (UNDISCH_TAC `x:real^3 IN voronoi_closed V v`);
 (REWRITE_TAC[IN; voronoi_closed; IN_ELIM_THM]);
 (STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (REFL_TAC);

 (NEW_GOAL `vol (ball (vec 0,r)) + (--(&24 / &3) * pi) * r pow 2 <= 
             vol (ball (vec 0,r - &2))`);
 (ASM_SIMP_TAC[VOLUME_BALL; REAL_ARITH `~(r < &6) ==> &0 <= r`;
   REAL_ARITH `~(r < &6) ==> &0 <= (r - &2)` ]);
 (REWRITE_TAC[REAL_ARITH 
 `&4 / &3 * pi * r pow 3 + (--(&24 / &3) * pi) * r pow 2 <=
  &4 / &3 * pi * (r - &2) pow 3 <=> 
  &0 <= &4 / &3 * pi * (&12 * r - &8)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_DIV THEN REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (REWRITE_TAC[PI_POS_LE]);
 (NEW_GOAL `&12 * r >= &72`);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN STRIP_TAC);

 (EXISTS_TAC `c:real`);
 (REPEAT STRIP_TAC);

 (NEW_GOAL `sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol <=
              vol (ball (vec 0,r))`);
 (ASM_SIMP_TAC[]);
 (NEW_GOAL `vol (ball (vec 0,r)) + c * r pow 2 <=
            sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 (ASM_SIMP_TAC[]);
 (ABBREV_TAC `a1 = sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol`);
 (ABBREV_TAC `a2 = vol (ball ((vec 0):real^3,r))`);
 (ABBREV_TAC `a3 = sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 (ASM_REAL_ARITH_TAC);

 (EXISTS_TAC `&0`);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[])]);;

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

let KIZHLTL2 = prove_by_refinement (KIZHLTL2_concl,

[(REPEAT STRIP_TAC);
 (ASM_CASES_TAC `saturated V /\ packing V`);
 (NEW_GOAL 
  `?C. !r. &1 <= r ==> 
   &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &8))) <=
   C * 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);
 (EXISTS_TAC `(&2 * mm1 / pi) * (&4 * pi) * (--C)`);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `&(CARD (V INTER ball ((vec 0):real^3,r) DIFF 
                     V INTER ball (vec 0,r - &8))) <= C * r pow 2`);
 (ASM_SIMP_TAC[]);
 (NEW_GOAL `total_solid V = (\X. total_solid V X)`);
 (REWRITE_TAC[GSYM ETA_AX]);
 (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
 (REWRITE_TAC[total_solid]);
 (ABBREV_TAC `B = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 (NEW_GOAL `FINITE (B:(real^3->bool) ->bool)`);
 (EXPAND_TAC "B" THEN MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
 (ASM_REWRITE_TAC[]);
 (ABBREV_TAC `A1:real^3->bool = V INTER ball (vec 0,r)`);
 (ABBREV_TAC `A2:real^3->bool = V INTER ball (vec 0,r - &8)`);
 (NEW_GOAL `FINITE (A1:real^3->bool)`);
 (EXPAND_TAC "A1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `FINITE (A2:real^3->bool)`);
 (EXPAND_TAC "A2" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `sum B (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X)) 
          <= sum B (\X. sum (VX V X) (\x. sol x X))`);
 (MATCH_MP_TAC SUM_LE);
 (ASM_REWRITE_TAC[BETA_THM]);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC SUM_SUBSET_SIMPLE);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[VX] THEN COND_CASES_TAC);
 (REWRITE_TAC[FINITE_EMPTY]);
 (LET_TAC);
 (COND_CASES_TAC);
 (REWRITE_TAC[FINITE_EMPTY]);
 (REWRITE_TAC[FINITE_SET_OF_LIST]);
 (SET_TAC[]);
 (REWRITE_TAC[BETA_THM]);

 (UNDISCH_TAC `x:real^3->bool IN B`);
 (EXPAND_TAC "B" THEN REWRITE_TAC[IN; IN_ELIM_THM; mcell_set_2]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `eventually_radial x' (mcell i V ul)`);
 (MATCH_MP_TAC Urrphbz2.URRPHBZ2);
 (ASM_REWRITE_TAC[]);
 (SUBGOAL_THEN `x' IN (VX V x)` MP_TAC);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[VX]);
 (COND_CASES_TAC);
 (SET_TAC[]);
 (LET_TAC);
 (COND_CASES_TAC);
 (SET_TAC[]);
 (STRIP_TAC);

 (UNDISCH_TAC `cell_params V x = k,ul'`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[cell_params]);
 (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ x = mcell k V ul)`);
 (DISCH_TAC);
 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SELECT_AX);
 (EXISTS_TAC `(i:num,ul:(real^3)list)`);
 (EXPAND_TAC "P");
 (REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN EXPAND_TAC "P" THEN REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
 (NEW_GOAL `set_of_list (truncate_simplex (k - 1) ul') SUBSET V:real^3->bool`);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `k - 1`);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3`);
 (STRIP_TAC);
 (ASM_SET_TAC[]);
 (ASM_ARITH_TAC);
 (ASM_SET_TAC[]);


 (UP_ASM_TAC THEN REWRITE_TAC[eventually_radial]);
 (REPEAT STRIP_TAC);
 (REWRITE_WITH `sol x' (mcell i V ul) = 
  &3 * vol ((mcell i V ul) INTER normball x' r') / r' pow 3`);
 (MATCH_MP_TAC sol);
 (ASM_REWRITE_TAC[GSYM Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM; NORMBALL_BALL]);
 (MATCH_MP_TAC MEASURABLE_INTER);
 (ASM_SIMP_TAC[MEASURABLE_BALL; MEASURABLE_MCELL]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[REAL_ARITH `&0 <= &3`] THEN MATCH_MP_TAC REAL_LE_DIV);
 (STRIP_TAC);
 (MATCH_MP_TAC MEASURE_POS_LE);
 (MATCH_MP_TAC MEASURABLE_INTER);
 (ASM_SIMP_TAC[MEASURABLE_BALL; NORMBALL_BALL; MEASURABLE_MCELL]);
 (MATCH_MP_TAC REAL_POW_LE THEN ASM_REAL_ARITH_TAC);

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

 (NEW_GOAL `sum B  (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X)) = 
             sum A2 (\u. sum  {X | X IN B /\ VX V X u} (\X. sol u X))`);
 (MATCH_MP_TAC SUM_SUM_RESTRICT);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `sum A2 (\u. sum {X | X IN B /\ VX V X u} (\X. sol u X)) = 
             sum A2 (\u. sum {X | mcell_set V X /\ u IN VX V X} 
                    (\X. sol u X))`);
 (MATCH_MP_TAC SUM_EQ);
 (EXPAND_TAC "A2" THEN REWRITE_TAC[IN_INTER; IN_DIFF] THEN 
   REWRITE_TAC[IN_BALL; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (REWRITE_WITH `{X | B X /\ VX V X x} = 
                 {X | mcell_set V X /\ VX V X x}`);
 (REWRITE_TAC[SET_RULE `a = b <=> a SUBSET b /\ b SUBSET a`]);
 (STRIP_TAC);
 (EXPAND_TAC "B");
 (SET_TAC[]);
 (REWRITE_WITH `!x:real^3->bool. B x <=> x IN B`);
 (REWRITE_TAC[IN]);
 (EXPAND_TAC "B" THEN REWRITE_TAC[SUBSET; IN_INTER; IN_DIFF] THEN  
   REWRITE_TAC[IN_BALL; IN; IN_ELIM_THM]);
 (REWRITE_TAC[MESON[] `A /\ X /\ Y ==> (B /\ A) /\ X /\ Y <=> A /\ X /\ Y ==> B`]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `x IN VX V x'`);
 (ASM_REWRITE_TAC[IN]);
 (NEW_GOAL `~NULLSET x'`);
 (UNDISCH_TAC `x IN VX V x'` THEN REWRITE_TAC[VX] THEN COND_CASES_TAC);
 (SET_TAC[]);
 (MESON_TAC[]);

 (NEW_GOAL `dist (vec 0, x'':real^3) <= dist (vec 0, x) + dist (x, x'')`);
 (REWRITE_TAC[DIST_TRIANGLE]);
 (NEW_GOAL `?p. x' SUBSET ball (p:real^3,&4)`);
 (MATCH_MP_TAC MCELL_SUBSET_BALL_4);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[SUBSET; IN_BALL] THEN STRIP_TAC);
 (NEW_GOAL `dist (x, x'':real^3) <= dist (x, p) + dist (p, x'')`);
 (REWRITE_TAC[DIST_TRIANGLE]);
 (NEW_GOAL `dist (x, p:real^3) < &4`);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (FIRST_ASSUM MATCH_MP_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_ELIM_THM] THEN STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_SET_TAC[]);
 (NEW_GOAL `dist (p:real^3,x'') < &4`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[IN]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

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

 (UP_ASM_TAC);
 (REWRITE_WITH `sum A2 (\u. sum {X | mcell_set V X /\ u IN VX V X} (\X. sol u X)) = sum A2 (\u. &4 * pi)`);
 (MATCH_MP_TAC SUM_EQ);
 (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC);
 (MATCH_MP_TAC Qzyzmjc.QZYZMJC);
 (ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_SIMP_TAC[SUM_CONST]);
 (STRIP_TAC);

 (ABBREV_TAC `s1 = sum B (\X. sum (VX V X) (\x. sol x X))`);
 (NEW_GOAL `&(CARD (A2:real^3->bool)) * &4 * pi <= s1`);
 (ABBREV_TAC `s2 = sum B (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X))`);
 (ABBREV_TAC `s3 = sum A2 (\u. sum {X | X IN B /\ VX V X u} (\X. sol u X))`);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `(&2 * mm1 / pi) * &(CARD (A2:real^3->bool)) * &4 * pi <= (&2 * mm1 / pi) * s1`);
 (REWRITE_TAC[REAL_ARITH `a * b <= a * c <=> &0 <= (c - b) * a`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_TAC[PI_POS_LE]);
 (NEW_GOAL `#1.012080 < mm1`);
 (REWRITE_TAC[Flyspeck_constants.bounds]);
 (UP_ASM_TAC THEN REAL_ARITH_TAC);
 
 (NEW_GOAL `&(CARD (A1:real^3->bool)) * &8 * mm1 + 
             ((&2 * mm1 / pi) * (&4 * pi) * --C) * r pow 2 <= 
             (&2 * mm1 / pi) * &(CARD (A2:real^3->bool)) * &4 * pi`);
 (REWRITE_TAC[REAL_ARITH `((&2 * mm1 / pi) * (&4 * pi) * --C) * r pow 2 = 
  (--C * r pow 2) * (&8 * mm1) * (pi / pi)`]);
 (REWRITE_TAC[REAL_ARITH `(&2 * mm1 / pi) * &(CARD A2) * &4 * pi = 
  &(CARD A2) * (&8 * mm1) * (pi / pi)`]);
 (REWRITE_WITH `pi / pi = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (MP_TAC PI_POS THEN REAL_ARITH_TAC);
 (REWRITE_TAC[REAL_MUL_RID; REAL_ARITH `a * b + c * b <= d * b <=>
  &0 <= (d - a - c) * b `]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH `&0 <= a - b - (--c * x) <=> b - a <= c * x`]);

 (NEW_GOAL `A2 SUBSET A1:real^3->bool`);
 (EXPAND_TAC "A1" THEN EXPAND_TAC "A2");
 (MATCH_MP_TAC (SET_RULE `A SUBSET B ==> V INTER A SUBSET V INTER B`));
 (MATCH_MP_TAC SUBSET_BALL);
 (REAL_ARITH_TAC);
 (REWRITE_WITH `&(CARD (A1:real^3->bool)) - &(CARD (A2:real^3->bool)) = 
   &(CARD A1 - CARD A2)`);
 (MATCH_MP_TAC REAL_OF_NUM_SUB);
 (MATCH_MP_TAC CARD_SUBSET);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `CARD (A1:real^3->bool) - CARD (A2:real^3->bool) = 
   CARD (A1 DIFF A2)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC CARD_DIFF);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC REAL_LE_MUL);
 (NEW_GOAL `#1.012080 < mm1`);
 (REWRITE_TAC[Flyspeck_constants.bounds]);
 (UP_ASM_TAC THEN REAL_ARITH_TAC);


 (ASM_REAL_ARITH_TAC);
 (EXISTS_TAC `&0`);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[])]);;

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

let KIZHLTL4_concl = 
  `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r
               ==> (&8 * mm2 / pi) *
                   sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
                   (\X. sum (edgeX V X)
                        (\({u, v}). if {u, v} IN edgeX V X
                                    then dihX V X (u,v) * lmfun (hl [u; v])
                                    else &0)) +
                   c * r pow 2 <=
                   &8 *
                   mm2 *
                   sum (V INTER ball (vec 0,r))
                   (\u. sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
                        (\v. lmfun (hl [u; v])))`;;

let KIZHLTL4 = prove_by_refinement (KIZHLTL4_concl,

[(REPEAT STRIP_TAC);
 (ASM_CASES_TAC `saturated V /\ packing V`);
 (ABBREV_TAC `c = &8 * mm2 * (&0)`);
 (EXISTS_TAC `c:real`);  (* choose d later *)

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

 (REPEAT STRIP_TAC);
 (ABBREV_TAC `S1 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 (ABBREV_TAC `V1:real^3->bool = V INTER ball (vec 0, r)`);
 (ABBREV_TAC `T1 = {{u,v:real^3} | u IN V1 /\ v IN V1}`);

 (NEW_GOAL `FINITE (S1:(real^3->bool)->bool)`);
 (EXPAND_TAC "S1");
 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);

 (NEW_GOAL `FINITE (T1:(real^3->bool)->bool)`);
 (EXPAND_TAC "T1");
 (REWRITE_TAC[GSYM set_of_list]);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `IMAGE (set_of_list) {[u; v:real^3] | u IN V1 /\ v IN V1}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_IMAGE);
 (REWRITE_TAC[SET_RULE `{[u;v] | u IN s /\ v IN s} = 
                         {y | ?u0 u1. u0 IN s /\ u1 IN s /\ y = [u0; u1]}`]);
 (MATCH_MP_TAC FINITE_LIST_KY_LEMMA_2);
 (EXPAND_TAC "V1" THEN MATCH_MP_TAC Packing3.KIUMVTC);
 (ASM_REWRITE_TAC[]);
 (SET_TAC[]);

 (ABBREV_TAC 
   `S2 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~NULLSET X}`);
 (NEW_GOAL `FINITE (S2:(real^3->bool)->bool)`);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `S1:(real^3->bool)->bool`);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN SET_TAC[]);

 (ABBREV_TAC `g = (\X. (\({u, v}). 
                            if {u, v} IN edgeX V X
                            then dihX V X (u,v) * lmfun (hl [u; v])
                            else &0))`);
 (REWRITE_WITH 
`sum S1  (\X. sum (edgeX V X)
                 (\({u, v}). if {u, v} IN edgeX V X
                             then dihX V X (u,v) * lmfun (hl [u; v])
                             else &0)) = 
 sum S1 (\X. sum (edgeX V X) (\({u, v}). g X {u,v}))`);
 (MATCH_MP_TAC SUM_EQ);

 (EXPAND_TAC "S1" THEN REWRITE_TAC[IN_ELIM_THM; IN; mcell_set_2]);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC SUM_EQ);
 (REWRITE_WITH `!x'. x' IN edgeX V x <=> 
                      ?u v. VX V x u /\ VX V x v /\ ~(u = v) /\ x' = {u, v}`);
 (REWRITE_TAC[IN; IN_ELIM_THM; edgeX]);
 (MESON_TAC[]);
 (REPEAT STRIP_TAC);

 (ABBREV_TAC `f_temp = (\u v. if edgeX V x {u, v}
             then dihX V x (u,v) * lmfun (hl [u; v])
             else &0)`);
 (NEW_GOAL `!u v. (f_temp:real^3->real^3->real) u v = f_temp v u`);
 (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);
 (REPEAT GEN_TAC THEN COND_CASES_TAC);
 (COND_CASES_TAC);
 (REWRITE_WITH `dihX V x (u',v') = dihX V x (v',u')`);
 (MATCH_MP_TAC DIHX_SYM);
 (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);
 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (COND_CASES_TAC);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (REFL_TAC);

 (REWRITE_WITH `(\({u, v}). if edgeX V x {u, v}
             then dihX V x (u,v) * lmfun (hl [u; v])
             else &0) = (\({u, v}). f_temp u v)`);
 (EXPAND_TAC "f_temp");
 (REWRITE_TAC[]);

 (REWRITE_TAC[BETA_SET_2_THM; ASSUME `x' = {u,v:real^3}`]);
 (REWRITE_WITH `(\({u, v}). f_temp u v) {u, v} = 
                             (f_temp:real^3->real^3->real) u v`);
 (MATCH_MP_TAC BETA_PAIR_THM);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `(g:(real^3->bool)->(real^3->bool)->real) x = 
                 (\({u, v}). f_temp u v)`);
 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "g" THEN REWRITE_TAC[IN]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC BETA_PAIR_THM);
 (ASM_REWRITE_TAC[]);

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

 (REWRITE_WITH `sum S1 (\X. sum (edgeX V X) (\({u, v}). g X {u, v})) = 
                 sum S1 (\X. sum (edgeX V X)  (g X))`);
 (MATCH_MP_TAC SUM_EQ);
 (REWRITE_TAC[] THEN REPEAT STRIP_TAC);
 (MATCH_MP_TAC SUM_EQ);
 (REWRITE_TAC[edgeX; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[BETA_SET_2_THM]);

 (REWRITE_WITH `sum S1 (\X. sum (edgeX V X) (g X)) = 
                 sum S2 (\X. sum (edgeX V X) (g X))`);
 (MATCH_MP_TAC SUM_SUPERSET);
 (STRIP_TAC);
 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN SET_TAC[]);
 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC SUM_EQ_0);
 (REPEAT STRIP_TAC);

 (ABBREV_TAC `f_temp = (\u v. if edgeX V x {u, v}
             then dihX V x (u,v) * lmfun (hl [u; v])
             else &0)`);
 (NEW_GOAL `!u v. (f_temp:real^3->real^3->real) u v = f_temp v u`);
 (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);
 (REPEAT GEN_TAC THEN COND_CASES_TAC);
 (COND_CASES_TAC);
 (REWRITE_WITH `dihX V x (u,v) = dihX V x (v,u)`);

 (MATCH_MP_TAC DIHX_SYM);
 (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (COND_CASES_TAC);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (REFL_TAC);

 (REWRITE_WITH `(g:(real^3->bool)->(real^3->bool)->real) x = 
                 (\({u, v}). f_temp u v)`);
 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "g" THEN REWRITE_TAC[IN]);
 (UNDISCH_TAC `x' IN edgeX V x` THEN REWRITE_TAC[IN;IN_ELIM_THM; edgeX]);
 (STRIP_TAC);
 (ASM_SIMP_TAC[BETA_PAIR_THM]);
 (EXPAND_TAC "f_temp");
 (COND_CASES_TAC);
 (REWRITE_TAC[dihX]);
 (COND_CASES_TAC);
 (REAL_ARITH_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (REFL_TAC);

 (REWRITE_WITH 
 `sum S2 (\X. sum (edgeX V X) (g X)) =
  sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X))`);
 (MATCH_MP_TAC SUM_EQ);
 (EXPAND_TAC "S2" 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 "T1" THEN REWRITE_TAC[SUBSET; edgeX; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXPAND_TAC "V1" THEN REWRITE_TAC[IN_ELIM_THM]);
 (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);
 (REWRITE_TAC[ASSUME `x' = {u, v:real^3}`; IN_INTER;
               MESON[IN] `V (x:real^3) <=> x IN 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; IN_ELIM_THM]);
 (STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);

 (REWRITE_WITH 
  `sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X)) = 
   sum T1 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x))`);
 (REWRITE_WITH 
  `sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X)) = 
   sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (\x.g X x))`);
 (REWRITE_TAC[ETA_AX]);
 (ASM_SIMP_TAC[SUM_SUM_RESTRICT]);

(* May 09 - OK here *)

 (ABBREV_TAC 
  `T2 = {{u0:real^3, u1} | u0 IN V1 /\ u1 IN V1 /\ ~(u0 = u1) /\
                           hl[u0;u1] <= h0}`);
 (NEW_GOAL `sum T1 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x)) = 
             sum T2 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x))`);
 (MATCH_MP_TAC SUM_SUPERSET);
 (EXPAND_TAC "T1" THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN 
   REPEAT STRIP_TAC);
 (SET_TAC[]);
 (MATCH_MP_TAC SUM_EQ_0);
 (EXPAND_TAC "g" THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);

 (ABBREV_TAC `f_temp = (\u v. if {u, v} IN edgeX V x'
             then dihX V x' (u,v) * lmfun (hl [u; v])
             else &0)`);
 (REWRITE_WITH `(\({u, v}). if {u, v} IN edgeX V x'
             then dihX V x' (u,v) * lmfun (hl [u; v])
             else &0) = (\({u, v}). f_temp u v)`);
 (EXPAND_TAC "f_temp");
 (REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `(\({u, v}). f_temp u v) {u, v} = 
                             (f_temp:real^3->real^3->real) u v`);
 (MATCH_MP_TAC BETA_PAIR_THM);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "f_temp");
 (REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC);
 (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} ={b,a}`]);
 (REWRITE_WITH `dihX V x' (u',v') = dihX V x' (v',u')`);
 (MATCH_MP_TAC DIHX_SYM);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `x' IN {X | S2 X /\ edgeX V X x}`);
 (EXPAND_TAC "S2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (MESON_TAC[]);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`]);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`]);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (REFL_TAC);

 (EXPAND_TAC "f_temp");
 (COND_CASES_TAC);

 (ASM_CASES_TAC `hl [u; v:real^3] <= h0`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `~(?u0 u1.
            (V1 u0 /\ V1 u1 /\ ~(u0 = u1) /\ hl [u0; u1] <= h0) /\
            x = {u0, u1:real^3})` THEN REWRITE_TAC[]);
 (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `{u, v} IN edgeX V x'` THEN REWRITE_TAC[IN; IN_ELIM_THM; edgeX]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (REWRITE_WITH `lmfun (hl [u; v:real^3]) = &0`);
 (ASM_REWRITE_TAC[lmfun]);
 (REAL_ARITH_TAC);
 (REFL_TAC);

 (ASM_REWRITE_TAC[]);
(* ==================================================================== *)
(* REALLY OK Here *)

 (MATCH_MP_TAC (REAL_ARITH `(?b. a <= b /\ b + d <= e) ==> a + d <= e`));
 (EXISTS_TAC `(&8 * mm2 / pi) *
     sum T2 (\x. sum {X | mcell_set V X /\ x IN edgeX V X} (\X. g X x))`);
 (STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH `a * b <= a * c <=> &0 <= a * (c - b)`]);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 (REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_DIV THEN SIMP_TAC[ZERO_LE_MM2_LEMMA; PI_POS_LE]);
 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
 (MATCH_MP_TAC SUM_LE THEN REPEAT STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `T1:(real^3->bool)->bool`);
 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
 (REWRITE_TAC[BETA_THM]);
 (MATCH_MP_TAC SUM_SUBSET_SIMPLE);

 (STRIP_TAC);
 (REWRITE_TAC[IN] THEN MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
 (UP_ASM_TAC THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] 
   THEN STRIP_TAC);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);

 (EXPAND_TAC "S2" THEN REWRITE_TAC[IN] THEN SET_TAC[]);
 (REWRITE_TAC[BETA_THM]);
 (REWRITE_WITH `g x' x = gammaY V x' lmfun x`);
 (EXPAND_TAC "g" THEN REWRITE_TAC[gammaY]);
 (MATCH_MP_TAC gamma_y_pos_le);

 (UP_ASM_TAC THEN ASM_REWRITE_TAC[IN_DIFF; IN; IN_ELIM_THM]);
 (MESON_TAC[]);
 (REWRITE_WITH 
  `sum T2 (\x. sum {X | mcell_set V X /\ x IN edgeX V X} (\X. g X x)) = 
   sum T2 (\x. &2 * pi * lmfun (radV x))`);
 (MATCH_MP_TAC SUM_EQ);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[BETA_THM]);
 (EXPAND_TAC "g");

 (REWRITE_TAC[HL; BETA_THM; set_of_list]);
 (UP_ASM_TAC THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 (STRIP_TAC);

 (REWRITE_WITH `sum {X | mcell_set V X /\ edgeX V X x}
 (\X. (\({u, v}). if edgeX V X {u, v}
                  then dihX V X (u,v) * lmfun (radV {u, v}) else &0) x) = 
                sum {X | mcell_set V X /\ edgeX V X x}
 (\X. (if edgeX V X {u0, u1}
                  then dihX V X (u0,u1) * lmfun (radV {u0, u1}) else &0))`);
 (MATCH_MP_TAC SUM_EQ);
 (ASM_REWRITE_TAC[IN; IN_ELIM_THM; BETA_THM] THEN REPEAT STRIP_TAC);
 (ABBREV_TAC 
  `f_temp = (\u v. if edgeX V x' {u, v}
                   then dihX V x' (u,v) * lmfun (radV {u, v}) else &0)`);
 (NEW_GOAL `!u:real^3 v:real^3. 
            (f_temp:real^3->real^3->real) u v = f_temp v u`);
 (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);
 (REPEAT GEN_TAC THEN COND_CASES_TAC);
 (COND_CASES_TAC);
 (REWRITE_WITH `dihX V x' (u,v) = dihX V x' (v,u)`);

 (MATCH_MP_TAC DIHX_SYM);
 (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (COND_CASES_TAC);
 (UP_ASM_TAC THEN MESON_TAC[]);
 (REFL_TAC);

 (REWRITE_WITH 
 `(\({u, v}). if edgeX V x' {u, v}
              then dihX V x' (u,v) * lmfun (radV {u, v})
              else &0)
    = (\({u, v}). f_temp u v)`);
 (EXPAND_TAC "f_temp" THEN REWRITE_TAC[IN]);
 (REWRITE_WITH 
  `(if edgeX V x' {u0, u1}
   then dihX V x' (u0,u1) * lmfun (radV {u0, u1}) else &0) = 
   f_temp u0 u1`);
 (EXPAND_TAC "f_temp" THEN REWRITE_TAC[IN]);
 (MATCH_MP_TAC BETA_PAIR_THM);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `FINITE {X | mcell_set V X /\ edgeX V X x}`);
 (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC [SUM_CASES]);

 (REWRITE_TAC[SET_RULE 
 `{X | X IN {X | mcell_set V X /\ edgeX V X {u0, u1}} /\ edgeX V X {u0, u1}} =
  {X | mcell_set V X /\ edgeX V X {u0, u1}} /\ 
  {X | X IN {X | mcell_set V X /\ edgeX V X {u0, u1}} /\ 
      ~edgeX V X {u0, u1}} = {}`; SUM_CLAUSES; REAL_ARITH `a + &0 = a`]);
 (REWRITE_TAC[SUM_RMUL]);
 (REWRITE_WITH 
  `sum {X | mcell_set V X /\ edgeX V X {u0, u1}} (\X. dihX V X (u0,u1)) = 
   &2 * pi`);
 (REWRITE_WITH 
  `{X | mcell_set V X /\ edgeX V X {u0, u1}} = 
   {X | mcell_set V X /\ {u0, u1} IN edgeX V X}`);
 (REWRITE_TAC[IN]);
 (MATCH_MP_TAC GRUTOTI);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (ASM_SET_TAC[]);
 (ASM_SET_TAC[]);
 (NEW_GOAL `h0 < sqrt (&2)`);
 (REWRITE_TAC[H0_LT_SQRT2]);
 (ASM_REAL_ARITH_TAC);
 (REAL_ARITH_TAC);
 (REWRITE_TAC[SUM_LMUL; REAL_ARITH `(&8 * mm2 / pi) * &2 * pi * a = 
                                     (&8 * mm2) * (pi / pi) * (&2 * a)`]);
 (REWRITE_WITH `pi / pi = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (REWRITE_TAC[PI_NZ]);
 (REWRITE_TAC[REAL_ARITH `&1 * a = a`]);
 (EXPAND_TAC "c");
 (REWRITE_TAC[REAL_ARITH 
  `(&8 * mm2) * a + (&8 * mm2 * d) * b <= &8 * mm2 * c <=> 
   &0 <= (&8 * mm2) * (c - a - d * b)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (SIMP_TAC[REAL_LE_MUL; REAL_ARITH `&0 <= &8`; ZERO_LE_MM2_LEMMA]);
 (REWRITE_TAC[REAL_ARITH `&0 <= a - b - c <=> b + c <= a`]);

 (EXPAND_TAC "T2");
 (REWRITE_TAC[Marchal_cells_3.HL_2; 
   REAL_ARITH `inv (&2) * x <= y <=> x <= &2 * y`]);
 (REWRITE_WITH `&2 *
 sum
 {{u0:real^3, u1} | u0 IN V1 /\ u1 IN V1 /\ 
                   ~(u0 = u1) /\ dist (u0,u1) <= &2 * h0}
 (\x. lmfun (radV x)) = 
 sum 
 {u0:real^3,u1 | u0 IN V1 /\ u1 IN V1 /\ 
                ~(u0 = u1) /\ dist (u0,u1) <= &2 * h0}
 (\(u0,u1). (\x. lmfun (radV x)) {u0, u1})`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC SUM_PAIR_2_SET);
 (EXPAND_TAC "V1");
 (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 (REWRITE_TAC[GSYM Marchal_cells_3.HL_2; HL;set_of_list]);

 (ABBREV_TAC 
  `t = (\u:real^3. {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0})`);
 (ABBREV_TAC `f_temp = (\u v. lmfun (radV {u:real^3, v}))`);

 (REWRITE_WITH 
`sum V1
 (\u. sum {v | v IN V /\ ~(u = v) /\ dist (u,v:real^3) <= &2 * h0}
 (\v. lmfun (radV {u, v}))) = 
 sum V1 
 (\u:real^3. sum
 ((t:real^3->real^3->bool) u) ((f_temp:real^3->real^3->real) u))`);

 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "t");
 (REWRITE_TAC[]);
 
 (REWRITE_WITH 
 `sum V1 (\i. sum (t i) (f_temp i)) =
  sum {u0:real^3,u1:real^3 | u0 IN V1 /\ u1 IN t u0} (\(u0,u1). f_temp u0 u1)`);
 (MATCH_MP_TAC SUM_SUM_PRODUCT);
 (REPEAT STRIP_TAC);
 (EXPAND_TAC "V1");
 (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 (EXPAND_TAC "t");
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `(V:real^3->bool) INTER ball (vec 0, r + &2 * h0)`);
 (STRIP_TAC);
 (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 (REWRITE_TAC[SUBSET; IN; IN_INTER; IN_BALL; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `dist (vec 0, x) <= dist (vec 0, u0) + dist (u0, x:real^3)`);
 (NORM_ARITH_TAC);
 (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
 (REWRITE_TAC[GSYM IN_BALL]);
 (UNDISCH_TAC `u0:real^3 IN V1` THEN EXPAND_TAC "V1" THEN SET_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (EXPAND_TAC "t" THEN EXPAND_TAC "f_temp");
 (REWRITE_TAC[IN; IN_ELIM_THM]);
 (REWRITE_TAC[REAL_ARITH `a + &0 * r pow 2 = a`]);
 (MATCH_MP_TAC SUM_SUBSET_SIMPLE);
 (REPEAT STRIP_TAC);

 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC 
  `{u0:real^3,u1:real^3 |u0 IN V1 /\u1 IN V INTER ball (vec 0, r + &2 * h0)}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_PRODUCT);
 (STRIP_TAC);
 (EXPAND_TAC "V1");
 (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`]);
 (REWRITE_TAC[IN_BALL; IN_INTER; IN]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `dist (vec 0, u1) <= dist (vec 0, u0) + dist (u0, u1:real^3)`);
 (NORM_ARITH_TAC);
 (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
 (REWRITE_TAC[GSYM IN_BALL]);
 (UNDISCH_TAC `(V1:real^3->bool) u0` THEN EXPAND_TAC "V1");
 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`]);
 (SET_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (EXPAND_TAC "V1" THEN 
   REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`; IN_INTER] THEN    
   SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_DIFF; IN_ELIM_THM; IN]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[lmfun_pos_le]);

 (EXISTS_TAC `&0`);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[])]);;

(* ------ Finish the proof of KIZHLTL 1, KIZHLTL 2, KIZHLTL 4  -------- *)


 end;;