(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: QZKSYKG                                                  *)
(*      Chaper    : Packing                                                  *)
(*                                                                           *)
(* ========================================================================= *)


module Qzksykg = struct

open Rogers;;
open Vukhacky_tactics;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Sphere;; 
open Marchal_cells;;
open Emnwuus;;
open Marchal_cells_2_new;;
open Lepjbdj;;
open Hdtfnfz;;
open Ynhyjit;;

let CONVEX_HULL_4_IMP_3_1 = 
prove_by_refinement (
 `!a:real^3 b c d x. 
    x IN convex hull {a,b,c,d} ==> 
       (?x1 t1 t2.
           x1 IN convex hull {a,b,c} /\ 
           &0 <= t1 /\ &0 <= t2 /\ t1 + t2 = &1 /\ 
           x = t1 % x1 + t2 % d)`,

[(REWRITE_TAC[CONVEX_HULL_4; CONVEX_HULL_3;IN;IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `z < &1`);

 (EXISTS_TAC `(u/ (u + v + w)) % a + (v/ (u+v+w)) % b + (w/(u+v+w)) % (c:real^3)`);
 (EXISTS_TAC `(u + v + w):real` THEN EXISTS_TAC `z:real`);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `u/(u+v+w)`);
 (EXISTS_TAC `v/(u+v+w)`);
 (EXISTS_TAC `w/(u+v+w)`);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_DIV);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_DIV);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_DIV);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[REAL_ARITH `u / (u + v + w) + v / (u + v + w) + w / (u + v + w)=
  (u + v + w) / (u + v + w)`]);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (ASM_REAL_ARITH_TAC);
 (REFL_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[VECTOR_ARITH `s % (s1 /s % a + s2 / s % b + s3/ s % c) =
   (s * s1 / s) % a + (s * s2 / s) % b + (s * s3 / s) % c`]);
 (REWRITE_TAC[REAL_ARITH `s * s1 / s = s1 * (s / s)`]);
 (REWRITE_WITH `(u + v + w) / (u + v + w) = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[REAL_MUL_RID] THEN VECTOR_ARITH_TAC);

 (NEW_GOAL `z = &1 /\ u = &0 /\ v = &0 /\ w = &0`);
 (ASM_REAL_ARITH_TAC);
 (EXISTS_TAC `a:real^3`);
 (EXISTS_TAC `&0` THEN EXISTS_TAC `&1`);
 (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1 /\ &0 + &1 = &1`]);
 (STRIP_TAC);
 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
 (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1 /\ &1 + &0 + &0 = &1`]);
 (VECTOR_ARITH_TAC);
 (VECTOR_ARITH_TAC)]);;

let BARV_2_EXPLICIT = 
prove_by_refinement (
 `!V vl. barV V 2 vl ==> ?u0 u1 u2. vl = [u0;u1;u2]`,

[(REWRITE_TAC[BARV] THEN REPEAT STRIP_TAC);
 (NEW_GOAL `?x0 xl. (vl:(real^3)list) = CONS x0 xl /\ LENGTH xl = 2`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `x0:real^3`);
 (NEW_GOAL `?x1 yl. (xl:(real^3)list) = CONS x1 yl /\ LENGTH yl = 1`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `x1:real^3`);
 (NEW_GOAL `?x2 zl. (yl:(real^3)list) = CONS x2 zl /\ LENGTH zl = 0`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `x2:real^3`);
 (NEW_GOAL `(zl:(real^3)list) = []`);
 (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 (ASM_REWRITE_TAC[])]);;
let ROGERS_EXPLICIT_2 = 
prove_by_refinement (
 `!V ul.
  saturated V /\ packing V /\ barV V 2 ul ==> 
  rogers V ul = convex hull 
 {HD ul, omega_list_n V ul 1, omega_list_n V ul 2}`,


[(REPEAT STRIP_TAC THEN REWRITE_TAC[ROGERS]);
 (NEW_GOAL `?u0 u1 u2. (ul:(real^3)list) = [u0:real^3;u1;u2]`);
 (MATCH_MP_TAC BARV_2_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `{j | j < LENGTH (ul:(real^3)list)} = {0, 1,2}`);
 (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) = 3`]);
 (SET_TAC[ARITH_RULE `0 < 3 /\ 1 < 3 /\ 2 < 3 /\ 
                      (!j. j < 3 ==> (j=0\/j=1\/j=2))`]);
 (REWRITE_TAC[IMAGE]);
 (AP_TERM_TAC);
 (REWRITE_TAC[SET_RULE `!x. x IN {0,1,2} <=> (x = 0 \/x = 1 \/x = 2)`]);
 (REWRITE_WITH
 `!y. (?x. (x = 0 \/ x = 1 \/ x = 2) /\ y = omega_list_n V ul x) 
 <=> (y = omega_list_n V ul 0) \/ (y = omega_list_n V ul 1) \/
     (y = omega_list_n V ul 2)`);
 (SET_TAC[BETA_THM]);
 (REWRITE_WITH 
   `{y | y = omega_list_n V ul 0 \/ y = omega_list_n V ul 1 \/
          y = omega_list_n V ul 2} 
     =  {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2}`);
 (SET_TAC[]);
 (REWRITE_WITH `omega_list_n V ul 0 = HD ul`);
 (REWRITE_TAC[OMEGA_LIST_N])]);;
let TWO_REARRANGEMENT_LEMMA = 
prove_by_refinement (
 `!V ul p u0 u1 u2 u3. 
    packing V /\ saturated V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3] ==>
    (?p. p permutes 0..1 /\ [u1;u0;u2;u3] = left_action_list p ul)`,

[(REPEAT STRIP_TAC);
 (ABBREV_TAC `p = (\i. if i = 0 then 1 else if i = 1 then 0 else i)`);
 (EXISTS_TAC `p:num->num`);

 (NEW_GOAL `p 0 = 1`);
 (EXPAND_TAC "p");
 (COND_CASES_TAC);
 (REFL_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `p 1 = 0`);
 (EXPAND_TAC "p");
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (REFL_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!i. 1 < i ==> p i = i`);
 (EXPAND_TAC "p");
 (REPEAT STRIP_TAC);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `inverse p 0 = 1`);
 (REWRITE_TAC[inverse]);
 (MATCH_MP_TAC SELECT_UNIQUE);
 (GEN_TAC THEN EQ_TAC);
 (REWRITE_TAC[BETA_THM]);
 (ASM_CASES_TAC `y = 0`);
 (ASM_REWRITE_TAC[]);
 (ARITH_TAC);
 (ASM_CASES_TAC `1 < y`);
 (ASM_SIMP_TAC[]);
 (STRIP_TAC);
 (ASM_ARITH_TAC);
 (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);

 (NEW_GOAL `inverse p 1 = 0`);
 (REWRITE_TAC[inverse]);
 (MATCH_MP_TAC SELECT_UNIQUE);
 (GEN_TAC THEN EQ_TAC);
 (REWRITE_TAC[BETA_THM]);
 (ASM_CASES_TAC `y = 1`);
 (ASM_REWRITE_TAC[]);
 (ARITH_TAC);
 (ASM_CASES_TAC `1 < y`);
 (ASM_SIMP_TAC[]);
 (STRIP_TAC);
 (ASM_ARITH_TAC);
 (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);

 (NEW_GOAL `!i. 1 < i ==> inverse p i = i`);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[inverse]);
 (MATCH_MP_TAC SELECT_UNIQUE);
 (GEN_TAC THEN EQ_TAC);
 (REWRITE_TAC[BETA_THM]);
 (ASM_CASES_TAC `y = 0`);
 (ASM_SIMP_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `y = 1`);
 (ASM_SIMP_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `1 < y`);
 (ASM_ARITH_TAC);
 (STRIP_TAC);
 (NEW_GOAL `(p:num->num) y = y`);
 (UNDISCH_TAC `1 < y` THEN ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[]);
 (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);
 (ASM_MESON_TAC[]);
 (STRIP_TAC);
 (MATCH_MP_TAC Hypermap.lemma_permutes_via_surjetive);
 (REWRITE_WITH `0..1 = {0,1}`);
 (REWRITE_TAC[GSYM NUMSEG_LE; ARITH_RULE `x <= 1 <=> x = 0 \/ x = 1`]);
 (SET_TAC[]);
 (REWRITE_TAC[Geomdetail.FINITE6; SET_RULE `a IN {x,y} <=> a = x \/ a = y`]);
 (ASM_MESON_TAC[]);

 (ASM_REWRITE_TAC[left_action_list;LENGTH; ARITH_RULE   
  `SUC (SUC (SUC (SUC 0))) = 4`]);
 (ASM_REWRITE_TAC[TABLE_4]);
 (ASM_SIMP_TAC[TABLE_4; EL;HD;TL; ARITH_RULE `1 < 2 /\ 1 < 3`]);
 (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`])]);;

let SET_SUBSET_AFFINE_HULL = 
prove (
 `!S:real^3->bool. S SUBSET affine hull S`,

 STRIP_TAC THEN 
 MATCH_MP_TAC (SET_RULE `(?C. A SUBSET C /\ C SUBSET B) ==> A SUBSET B`) THEN
 EXISTS_TAC `convex hull S:real^3->bool` THEN 
 REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET] THEN 
 REWRITE_TAC[IN_SET_IMP_IN_CONVEX_HULL_SET]);;
(* ========================================================================= *)

let QZKSYKG1_concl = 
 `!V ul vl k p.
         saturated V /\
         packing V /\
         barV V 3 ul /\
         k IN {0,1,2,3,4} /\
         ~ (mcell k V ul = {}) /\
         p permutes 0..(k - 1) /\
         vl = left_action_list p ul
        ==> barV V 3 vl`;;

let QZKSYKG2_concl = 
 `!V ul k.
         saturated V /\
         packing V /\
         barV V 3 ul /\
         k IN {0,1,2,3,4} 
     ==> (mcell k V ul SUBSET 
      UNIONS{rogers V (left_action_list p ul) | p permutes 0..(k-1)})`;;

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

let QZKSYKG1 = prove_by_refinement (QZKSYKG1_concl,
[(REPEAT STRIP_TAC);
 (ASM_CASES_TAC `k = 0 \/ k = 1`);
 (UNDISCH_TAC `p permutes 0..(k-1)`);
 (REWRITE_WITH `k - 1 = 0`);
 (ASM_ARITH_TAC);
 (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);
 (NEW_GOAL `k IN {2,3,4}`);
 (ASM_SET_TAC[]);

(* Cases k = 4 *)

 (ASM_CASES_TAC `k = 4`);
 (UNDISCH_TAC `~(mcell k V ul = {})`);
 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
 (COND_CASES_TAC);
 (STRIP_TAC);
 (REWRITE_TAC[MESON[IN] `barV V 3 s <=> s IN barV V 3`]);
 (MATCH_MP_TAC Rogers.YIFVQDV_1);
 (ASM_REWRITE_TAC[IN]);
 (REWRITE_WITH `3 = k - 1`);
 (ASM_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (MESON_TAC[]);

(* Cases k = 3, k = 2 *)

 (REWRITE_WITH 
  `barV V 3 vl /\
      (!j. k - 1 <= j /\ j <= 3
           ==> omega_list_n V vl j = omega_list_n V ul j)`);
 (MATCH_MP_TAC YNHYJIT);
 (EXISTS_TAC `p:num->num`);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `~(mcell k V ul = {})`);

 (ASM_CASES_TAC `k = 3`);
 (SIMP_TAC [ASSUME `k = 3`; MCELL_EXPLICIT; mcell3]);
 (COND_CASES_TAC);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`]);
 (ASM_REWRITE_TAC[]);
 (MESON_TAC[]);

 (NEW_GOAL `k = 2`);
 (ASM_SET_TAC[]);
 (SIMP_TAC [ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
 (COND_CASES_TAC);
 (LET_TAC);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]);
 (ASM_REWRITE_TAC[]);
 (MESON_TAC[])]);;
(* ========================================================================= *)


let QZKSYKG2 = prove_by_refinement ( QZKSYKG2_concl,

[(REPEAT STRIP_TAC);
 (ASM_CASES_TAC `k = 0 \/ k = 1`);
 (REWRITE_WITH `k - 1 = 0`);
 (ASM_ARITH_TAC);
 (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);
 (REWRITE_TAC[Packing3.SING_GSPEC_APP; UNIONS_1;
   Packing3.LEFT_ACTION_LIST_I]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell0]);
 (SET_TAC[]);
 (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell1]);
 (COND_CASES_TAC);
 (SET_TAC[]);
 (SET_TAC[]);

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

 (ASM_CASES_TAC `k = 4`);
 (REWRITE_WITH `k - 1 = 3`);
 (ASM_ARITH_TAC);
 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`; mcell4]);
 (COND_CASES_TAC);
 (REWRITE_WITH `convex hull set_of_list ul =
             UNIONS {rogers V (left_action_list p ul) | p permutes 0..3}`);
 (MATCH_MP_TAC Rogers.WQPRRDY);
 (ASM_REWRITE_TAC[IN]);
 (SET_TAC[]);
 (SET_TAC[]);

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

 (ASM_CASES_TAC `k = 3`);
 (REWRITE_WITH `k - 1 = 2`);
 (ASM_ARITH_TAC);
 (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell3]);
 (COND_CASES_TAC);

 (ABBREV_TAC `m = mxi V ul`);
 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list; 
   SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);

 (REWRITE_TAC[SUBSET]);
 (GEN_TAC THEN DISCH_TAC);
 (NEW_GOAL `(?x1 t1 t2.
                  x1 IN convex hull {u0, u1, u2:real^3} /\
                  &0 <= t1 /\
                  &0 <= t2 /\
                  t1 + t2 = &1 /\
                  x = t1 % x1 + t2 % m)`);
 (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_3_1]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_TAC[ASSUME `x:real^3 = t1 % x1 + t2 % m`]);

 (UNDISCH_TAC `x1 IN convex hull {u0, u1, u2:real^3}`);
 (REWRITE_WITH `convex hull {u0,u1,u2:real^3} = 
   UNIONS {rogers V (left_action_list p (truncate_simplex 2 ul)) | p permutes 0..2}`);
 (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list (truncate_simplex 2 ul)`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
 (MATCH_MP_TAC Rogers.WQPRRDY);
 (ASM_REWRITE_TAC[IN]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[IN_UNIONS]);
 (REPEAT STRIP_TAC);

 (NEW_GOAL `?p:num->num. p permutes 0..2 /\ t = rogers V (left_action_list p (truncate_simplex 2 ul))`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ABBREV_TAC `zl:(real^3)list = left_action_list p (truncate_simplex 2 ul)`);
 (EXISTS_TAC `rogers V (left_action_list p ul)`);
 (STRIP_TAC);
 (ASM_SET_TAC[]);
 (ABBREV_TAC `vl:(real^3)list = left_action_list p ul`);
 (NEW_GOAL 
   `rogers V vl =
     convex hull
     {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);
 (MATCH_MP_TAC ROGERS_EXPLICIT);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[MESON[IN] `barV V 3 vl <=> vl IN barV V 3`]);
 (REWRITE_WITH `vl IN barV V 3 /\
               omega_list_n V vl 2 = omega_list_n V ul 2 /\
               omega_list_n V vl 3 = omega_list_n V ul 3 /\
               mxi V vl = mxi V ul`);
 (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
 (EXISTS_TAC `p:num->num` THEN ASM_REWRITE_TAC[]);

 (NEW_GOAL `zl = truncate_simplex 2 (vl:(real^3)list)`);
 (EXPAND_TAC "zl" THEN EXPAND_TAC "vl");
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; 
   ARITH_RULE `SUC (SUC (SUC 0)) = 3`; TABLE_4; ARITH_RULE `SUC 3 = 4`;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; left_action_list]);

 (REWRITE_WITH `EL (inverse p 0) [u0; u1; u2:real^3] = 
                 EL (inverse p 0) [u0; u1; u2; u3] /\ 
                 EL (inverse p 1) [u0; u1; u2:real^3] = 
                 EL (inverse p 1) [u0; u1; u2; u3] /\
                 EL (inverse p 2) [u0; u1; u2:real^3] = 
                 EL (inverse p 2) [u0; u1; u2; u3]`);
 (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 [u0; u1; u2; u3]`);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);

 (NEW_GOAL `!i. i IN 0..2 ==> inverse p i IN 0..2`);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `y = inverse (p:num->num) i`);
 (ASM_CASES_TAC `y IN 0..2`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (MP_TAC (ASSUME `p permutes 0..2`) THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (STRIP_TAC);
 (NEW_GOAL `(p:num->num) y = y`);
 (ASM_SIMP_TAC[]);
 (UP_ASM_TAC THEN EXPAND_TAC "y");
 (REWRITE_WITH `(p:num->num) (inverse p i) = i`);
 (MESON_TAC[PERMUTES_INVERSES; ASSUME `p permutes 0..2`]);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
 (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
 (NEW_GOAL `inverse p 0 IN 0..2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);


 (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
 (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
 (NEW_GOAL `inverse p 1 IN 0..2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);

 (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
 (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
 (NEW_GOAL `inverse p 2 IN 0..2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);

 (NEW_GOAL `rogers V zl =
      convex hull {HD zl, omega_list_n V zl 1, omega_list_n V zl 2}`);
 (MATCH_MP_TAC ROGERS_EXPLICIT_2);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `2 <= 3`]);

 (REWRITE_TAC[MESON[IN] `barV V 3 vl <=> vl IN barV V 3`]);
 (REWRITE_WITH `vl IN barV V 3 /\
               omega_list_n V vl 2 = omega_list_n V ul 2 /\
               omega_list_n V vl 3 = omega_list_n V ul 3 /\
               mxi V vl = mxi V ul`);
 (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
 (EXISTS_TAC `p:num->num` THEN ASM_REWRITE_TAC[]);


(* ------------------------------ *)
 (NEW_GOAL 
  `x1 IN convex hull {HD zl, omega_list_n V zl 1, omega_list_n V zl 2}`);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_3;IN;IN_ELIM_THM]);
 (STRIP_TAC);
 (ABBREV_TAC `q1 = omega_list_n V zl 1`);
 (ABBREV_TAC `q2 = omega_list_n V zl 2`);
 (ABBREV_TAC `s3 = omega_list_n V ul 3`);
 (ABBREV_TAC `q0 = HD (zl:(real^3)list)`);

 (NEW_GOAL `vl IN barV V 3 /\
             omega_list_n V vl 2 = omega_list_n V ul 2 /\
             omega_list_n V vl 3 = omega_list_n V ul 3 /\
             mxi V vl = mxi V ul`);
 (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
 (EXISTS_TAC `p:num->num`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC);
 (NEW_GOAL `?v0 v1 v2 v3. vl = [v0;v1;v2;v3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);

 (NEW_GOAL `HD vl = q0:real^3`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (EXPAND_TAC "q0" THEN 
   REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);

 (NEW_GOAL `omega_list_n V vl 1 = q1`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (EXPAND_TAC "q1" THEN 
   REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
 (REWRITE_TAC[ARITH_RULE `2 = 1 + 1`]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);

 (NEW_GOAL `omega_list_n V vl 2 = q2`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (EXPAND_TAC "q2" THEN 
   REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
 (REWRITE_WITH `truncate_simplex 2 (vl:(real^3)list) = 
                 truncate_simplex (2 + 0) vl`);
 (REWRITE_TAC[ARITH_RULE `2 + 0 = 2`]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);

 (UNDISCH_TAC `omega_list_n V vl 2 = omega_list_n V ul 2` THEN   
   ASM_REWRITE_TAC[]);
 (DISCH_TAC);
 (NEW_GOAL `between m (q2, s3:real^3)`);
 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
                  dist (u0,s) = sqrt (&2) /\
                  mxi V ul = s`);
 (MATCH_MP_TAC MXI_EXPLICIT);
 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN 
   EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; 
   CONVEX_HULL_2; CONVEX_HULL_4]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `t1 * u` THEN EXISTS_TAC `t1 * v`);
 (EXISTS_TAC `t1 * w + t2 * u'` THEN EXISTS_TAC `t2 * v'`);
 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD]);
 (STRIP_TAC);
 (REWRITE_WITH 
   `t1 * u + t1 * v + (t1 * w + t2 * u') + t2 * v' = 
    t1 * (u + v + w) + t2 * (u' + v')`);
 (REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[REAL_MUL_RID]);
 (VECTOR_ARITH_TAC);
 (SET_TAC[]);

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

 (NEW_GOAL `k = 2`);
 (ASM_SET_TAC[]);
 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
 (COND_CASES_TAC);
 (LET_TAC);

 (ABBREV_TAC `m = mxi V ul`);
 (ABBREV_TAC `s2 = omega_list_n V ul 2`);
 (ABBREV_TAC `s3 = omega_list_n V ul 3`);
 (ASM_REWRITE_TAC[HD;TL; ARITH_RULE `2 - 1 = 1`]);
 (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ A SUBSET C) ==> A SUBSET B`));
 (EXISTS_TAC `convex hull {u0, u1, s2, s3:real^3}`);
 (REPEAT STRIP_TAC); (* Two subgoals *)

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

 (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ A SUBSET C) ==> A SUBSET B`));
 (EXISTS_TAC `rogers V ul UNION rogers V [u1;u0;u2;u3:real^3]`);
 (STRIP_TAC);
 (REWRITE_TAC[SUBSET; IN_UNIONS; IN_UNION]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[IN;IN_ELIM_THM]);
 (EXISTS_TAC `rogers V ul`);
 (STRIP_TAC);
 (EXISTS_TAC `I:num->num`);
 (ASM_REWRITE_TAC[PERMUTES_I; Packing3.LEFT_ACTION_LIST_I]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN]);

 (REWRITE_TAC[IN;IN_ELIM_THM]);
 (EXISTS_TAC `rogers V [u1;u0;u2;u3]`);
 (STRIP_TAC);
 (NEW_GOAL `?p. p permutes 0..1 /\ [u1;u0;u2;u3:real^3] = left_action_list p ul`);
 (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `p:num->num`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN]);
 (NEW_GOAL `?p. p permutes 0..1 /\ [u1;u0;u2;u3:real^3] = left_action_list p ul`);
 (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);


 (ABBREV_TAC `vl = [u1;u0;u2;u3:real^3]`);
 (NEW_GOAL `barV V 3 vl /\
             (!j. 1 <= j /\ j <= 3
                  ==> omega_list_n V vl j = omega_list_n V ul j)`);
 (ONCE_REWRITE_TAC[ARITH_RULE `1 = 2 - 1`]);
 (MATCH_MP_TAC YNHYJIT);
 (EXISTS_TAC `p:num->num` THEN REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]);
 (ASM_REWRITE_TAC[SET_RULE `2 IN {2,3,4}`]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ABBREV_TAC `s1 = omega_list_n V ul 1`);
 (NEW_GOAL `rogers V ul = convex hull {HD ul, s1, s2, s3}`);
 (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN EXPAND_TAC "s3");
 (MATCH_MP_TAC ROGERS_EXPLICIT);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `rogers V vl = convex hull {HD vl, omega_list_n V vl 1,
             omega_list_n V vl 2, omega_list_n V vl 3}`);
 (MATCH_MP_TAC ROGERS_EXPLICIT);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `omega_list_n V vl 1 = s1`);
 (EXPAND_TAC "s1" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (NEW_GOAL `omega_list_n V vl 2 = s2`);
 (EXPAND_TAC "s2" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (NEW_GOAL `omega_list_n V vl 3 = s3`);
 (EXPAND_TAC "s3" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);

 (ASM_REWRITE_TAC[HD]);
 (REWRITE_TAC[GSYM (ASSUME `vl = left_action_list p (ul:(real^3)list)`);
  GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);

 (NEW_GOAL `s1 = circumcenter {u1, u0:real^3}`);
 (EXPAND_TAC "s1" THEN MATCH_MP_TAC Marchal_cells_2_new.OMEGA_LIST_1_EXPLICIT_NEW);
 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[IN]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `hl [u1;u0:real^3] = 
   hl (truncate_simplex 1 (ul:(real^3)list))`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL]);
 (REWRITE_TAC[set_of_list; SET_RULE `{a,b} = {b,a}`]);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);

 (REWRITE_TAC[SUBSET; CONVEX_HULL_4; IN; IN_ELIM_THM; IN_UNION]);
 (REPEAT STRIP_TAC);

 (ASM_CASES_TAC `u <= v:real`);
 (DISJ2_TAC);
 (EXISTS_TAC `v - u:real` THEN EXISTS_TAC `&2 * u`);
 (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
 (ASM_SIMP_TAC[REAL_ARITH `v - u + &2 * u + w + z = u + v + w + z`; REAL_LE_MUL; REAL_ARITH `&0 <= &2`; REAL_ARITH `&0 <= a - b <=> b <= a`]);
 (VECTOR_ARITH_TAC);
 (NEW_GOAL `v <= u:real`);
 (ASM_REAL_ARITH_TAC);
 (DISJ1_TAC);
 (EXISTS_TAC `u - v:real` THEN EXISTS_TAC `&2 * v`);
 (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
 (ASM_SIMP_TAC[REAL_ARITH `u - v + &2 * v + w + z = u + v + w + z`;  
   REAL_LE_MUL; REAL_ARITH `&0 <= &2`; REAL_ARITH `&0 <= a - b <=> b <= a`]);
 (VECTOR_ARITH_TAC);

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

 (REWRITE_TAC[SUBSET; IN_INTER]);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `s1 = omega_list_n V ul 1`);

 (NEW_GOAL `s1 = circumcenter {u0, u1:real^3}`);
 (EXPAND_TAC "s1" THEN MATCH_MP_TAC Marchal_cells_2_new.OMEGA_LIST_1_EXPLICIT_NEW);
 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[IN]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `hl [u0;u1:real^3] = 
   hl (truncate_simplex 1 (ul:(real^3)list))`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL;set_of_list]);
 (ASM_REWRITE_TAC[]);

 (ABBREV_TAC `vl:(real^3)list = truncate_simplex 1 ul`);

 (NEW_GOAL `s1:real^3 IN voronoi_list V vl`);
 (EXPAND_TAC "vl" THEN EXPAND_TAC "s1");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (NEW_GOAL `s2:real^3 IN voronoi_list V vl`);
 (EXPAND_TAC "vl" THEN EXPAND_TAC "s2");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (NEW_GOAL `s3:real^3 IN voronoi_list V vl`);
 (EXPAND_TAC "vl" THEN EXPAND_TAC "s3");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);

 (NEW_GOAL `m IN voronoi_list V vl`);
 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
 (REWRITE_WITH `m = s2:real^3`);
 (EXPAND_TAC "m" THEN REWRITE_TAC[mxi]);
 (COND_CASES_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
                  dist (u0,s) = sqrt (&2) /\
                  mxi V ul = s)`);
 (MATCH_MP_TAC MXI_EXPLICIT);
 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V vl <=> 
   convex hull {s2, s3} SUBSET (convex hull (voronoi_list V vl))`);
 (REWRITE_WITH `convex hull (voronoi_list V vl) = voronoi_list V vl`);
 (REWRITE_TAC[CONVEX_HULL_EQ]);
 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (NEW_GOAL `~(u0 = u1:real^3)`);
 (STRIP_TAC);
 (NEW_GOAL `LENGTH (ul:(real^3)list) = 3 + 1 /\ 
             CARD (set_of_list ul) = 3 + 1`);
 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list; 
   SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`]);
 (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (ASM_ARITH_TAC);

 (UNDISCH_TAC `x IN aff_ge {u0, u1} {m, s3:real^3}`);
 (REWRITE_WITH `aff_ge {u0, u1} {m, s3:real^3} =
             {y | ?t1 t2 t3 t4.
                      &0 <= t3 /\
                      &0 <= t4 /\
                      t1 + t2 + t3 + t4 = &1 /\
                      y = t1 % u0 + t2 % u1 + t3 % m + t4 % s3}`);
 (MATCH_MP_TAC AFF_GE_2_2);

 (NEW_GOAL `~(m IN {u0, u1:real^3})`);
 (STRIP_TAC);

 (ASM_CASES_TAC `m = u0:real^3`);
 (UNDISCH_TAC `m IN voronoi_list V vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
 (STRIP_TAC);
 (NEW_GOAL `m:real^3 IN voronoi_closed V u1`);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
 (STRIP_TAC);
 (NEW_GOAL `dist (u0, u1:real^3) = &0`);
 (NEW_GOAL `&0 <= dist (u0, u1:real^3)`);
 (REWRITE_TAC[DIST_POS_LE]);
 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `m = u1:real^3`);
 (UNDISCH_TAC `m IN voronoi_list V vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
 (STRIP_TAC);
 (NEW_GOAL `m:real^3 IN voronoi_closed V u0`);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
 (STRIP_TAC);
 (NEW_GOAL `dist (u1, u0:real^3) = &0`);
 (NEW_GOAL `&0 <= dist (u1, u0:real^3)`);
 (REWRITE_TAC[DIST_POS_LE]);
 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
 (ASM_MESON_TAC[]);
 (ASM_SET_TAC[]);


 (NEW_GOAL `~(s3 IN {u0, u1:real^3})`);
 (STRIP_TAC);

 (ASM_CASES_TAC `s3 = u0:real^3`);
 (UNDISCH_TAC `s3 IN voronoi_list V vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
 (STRIP_TAC);
 (NEW_GOAL `s3:real^3 IN voronoi_closed V u1`);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
 (STRIP_TAC);
 (NEW_GOAL `dist (u0, u1:real^3) = &0`);
 (NEW_GOAL `&0 <= dist (u0, u1:real^3)`);
 (REWRITE_TAC[DIST_POS_LE]);
 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `s3 = u1:real^3`);
 (UNDISCH_TAC `s3 IN voronoi_list V vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
 (STRIP_TAC);
 (NEW_GOAL `s3:real^3 IN voronoi_closed V u0`);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
 (STRIP_TAC);
 (NEW_GOAL `dist (u1, u0:real^3) = &0`);
 (NEW_GOAL `&0 <= dist (u1, u0:real^3)`);
 (REWRITE_TAC[DIST_POS_LE]);
 (ASM_REAL_ARITH_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
 (ASM_MESON_TAC[]);
 (ASM_SET_TAC[]);

 (REWRITE_TAC[DISJOINT]);
 (ASM_SET_TAC[]);

(*  ======================================================================== *)
(* OK here *)

 (REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `&0 <= t1 /\ &0 <= t2`);

 (ASM_CASES_TAC `&0 < t3 + t4`);
 (ABBREV_TAC `t5 = t3 + t4:real`);
 (ABBREV_TAC `z = t3 / t5 % m + t4 / t5 % (s3:real^3)`);
 (NEW_GOAL `between z (m, s3:real^3)`);
 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
 (EXISTS_TAC `t3 / t5` THEN EXISTS_TAC `t4 / t5`);
 (ASM_SIMP_TAC[REAL_LE_DIV; REAL_ARITH `&0 < a ==> &0 <= a`]);
 (ASM_REWRITE_TAC[REAL_ARITH `a/b+c/b = (a+c)/b`]);
 (MATCH_MP_TAC REAL_DIV_REFL THEN ASM_REAL_ARITH_TAC);

 (NEW_GOAL `z IN voronoi_list V vl`);
 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 (EXISTS_TAC `convex hull {m, s3:real^3}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V vl <=> 
   convex hull {m, s3} SUBSET (convex hull (voronoi_list V vl))`);
 (REWRITE_WITH `convex hull (voronoi_list V vl) = voronoi_list V vl`);
 (REWRITE_TAC[CONVEX_HULL_EQ]);
 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

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

 (ASM_CASES_TAC `t1 < &0`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`);
 (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
 (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
 (NEW_GOAL `x = t1 % u0 + t2 % u1 + t5 % (z:real^3)`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "z" THEN EXPAND_TAC "t5");
 (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
 (REWRITE_TAC[REAL_ARITH `a * b / a = b * (a / a)`]);
 (ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ARITH `&0 < y ==> ~(y = &0)`;
  REAL_MUL_RID]);
 (REWRITE_TAC[dist]);
 (REWRITE_WITH `x - u1:real^3 = t1 % (u0 - u1) + t5 % (z - u1)`);
 (REWRITE_WITH `x - u1:real^3 = x - (t1 + t2 + t5) % u1`);
 (REWRITE_WITH `t1 + t2 + t5 = &1`);
 (ASM_REAL_ARITH_TAC);
 (VECTOR_ARITH_TAC);
 (REWRITE_TAC[ASSUME `x = t1 % u0 + t2 % u1 + t5 % z:real^3`]);
 (VECTOR_ARITH_TAC);

 (REWRITE_TAC[DOT_LADD; DOT_LMUL; GSYM NORM_POW_2]);
 (NEW_GOAL `(z - u1) dot (u0 - u1:real^3) <= 
             norm (z - u1:real^3) * norm (u0 - u1) * a`);

 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
 (NEW_GOAL `m = s2:real^3`);
 (EXPAND_TAC "m" THEN REWRITE_TAC[mxi] THEN COND_CASES_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `u0 - u1 = &2 % (u0 - s1:real^3)`);
 (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
  midpoint; VECTOR_ARITH `u0 - inv (&2) % (u0 + u1) = inv (&2) % (u0 - u1)`]);
 (VECTOR_ARITH_TAC);

 (NEW_GOAL `(z - s1) dot (u0 - s1:real^3) = &0`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V vl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);

 (NEW_GOAL `norm (s2 - u1) <= norm (z - u1:real^3)`);
 (REWRITE_WITH `norm (s2 - u1) <= norm (z - u1:real^3) <=> 
                 norm (s2 - u1) pow 2 <= norm (z - u1:real^3) pow 2`);
 (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
 (REWRITE_WITH `s2 - u1 = (s2 - s1) + (s1 - u1:real^3) /\ 
                  z - u1 = (z - s1) + (s1 - u1:real^3)`);
 (VECTOR_ARITH_TAC);
 (REWRITE_WITH `norm (s2 - s1 + s1 - u1) pow 2 = 
   norm (s2 - s1) pow 2 + norm (s1 - u1:real^3) pow 2`);
 (NEW_GOAL `(s2 - s1) dot (s1 - u1:real^3) = &0`);
 (REWRITE_WITH `s1 - u1 = u0 - s1:real^3`);
 (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V vl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);
 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);

 (REWRITE_WITH `norm (z - s1 + s1 - u1:real^3) pow 2 = 
                 norm (z - s1) pow 2 + norm (s1 - u1) pow 2`);
 (NEW_GOAL `(z - s1) dot (s1 - u1:real^3) = &0`);
 (REWRITE_WITH `s1 - u1 = u0 - s1:real^3`);
 (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
 (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
 (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] THEN
   REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]);
 (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);
 (REWRITE_TAC[GSYM dist; DIST_SYM]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `!a b c d:real^3. 
   dist (a, b:real^3) pow 2 <= dist (c,d) pow 2 <=> dist (a,b) <= dist (c,d)`);
 (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (SIMP_TAC[Collect_geom.POW2_COND; DIST_POS_LE]);
 (MATCH_MP_TAC CLOSEST_POINT_LE);
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);

 (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
 (EXPAND_TAC "zl" THEN REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
 (EXPAND_TAC "zl" THEN EXPAND_TAC "s3");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 (ASM_MESON_TAC[]);
 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=> 
   convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
 (REWRITE_TAC[CONVEX_HULL_EQ]);
 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (REWRITE_WITH `(z - u1) dot (u0 - u1:real^3) = &2 *  norm (u0 - s1) pow 2`);
 (REWRITE_WITH `(z - u1) dot (u0 - u1) = (z - s1) dot (u0 - u1) + 
                 (s1 - u1) dot (u0 - u1:real^3)`);
 (VECTOR_ARITH_TAC);
 (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; DOT_RMUL]);
 (REWRITE_WITH `(s1 - u1) = (u0 - s1:real^3)`);
 (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);


 (NEW_GOAL `&2 * norm (u0 - s1:real^3) pow 2 <= 
             norm (s2 - u1) * norm (u0 - u1) * a`);
 (NEW_GOAL `norm (s2 - u1:real^3) >= sqrt (&2)`);
 (NEW_GOAL `norm (s2 - u1:real^3) >= 
             hl (truncate_simplex 2 (ul:(real^3)list))`);
 (REWRITE_TAC[GSYM dist]);
 (NEW_GOAL `?p. p permutes 0..1 /\
                    [u1; u0; u2; u3:real^3] = left_action_list p ul`);
 (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ABBREV_TAC `ul' = [u1;u0;u2;u3:real^3]`);
 (NEW_GOAL `barV V 3 ul' /\
             (!j. 1 <= j /\ j <= 3
                  ==> omega_list_n V ul' j = omega_list_n V ul j)`);
 (ONCE_REWRITE_TAC[ARITH_RULE `1 = 2 - 1`]);
 (MATCH_MP_TAC YNHYJIT);
 (EXISTS_TAC `p:num->num` THEN REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; 
   SET_RULE `2 IN {2,3,4}`]);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `s2 = omega_list_n V ul' 2 /\ u1 = HD ul'`);
 (STRIP_TAC);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] );
 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); HD] );
 (REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
 (ABBREV_TAC `xl:(real^3)list = truncate_simplex 2 ul'`);
 (REWRITE_WITH `hl (truncate_simplex 2 (ul:(real^3)list)) = 
                 hl (xl:(real^3)list)`);
 (EXPAND_TAC "xl");
 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; 
   GSYM (ASSUME `[u1;u0;u2;u3:real^3] = ul'`); TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (REWRITE_TAC[HL; set_of_list; SET_RULE `{u0, u1, u2} = {u1,u0,u2}`]);
 (REWRITE_WITH `omega_list_n V ul' 2 = omega_list V xl`);
 (REWRITE_WITH `omega_list V xl = omega_list_n V xl 2`);
 (REWRITE_TAC[OMEGA_LIST]);
 (EXPAND_TAC "xl" THEN REWRITE_TAC[GSYM 
  (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (REWRITE_TAC[LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`]);
 (EXPAND_TAC "xl");
 (REWRITE_WITH 
  `truncate_simplex 2 (ul':(real^3)list) = truncate_simplex (2 + 0) ul'`);
 (REWRITE_TAC[ARITH_RULE `2 + 0 = 2`]);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
 (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); LENGTH]);
 (ARITH_TAC);
 (REWRITE_WITH `HD ul' = HD (xl:(real^3)list)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN EXPAND_TAC "xl");
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); LENGTH]);
 (ARITH_TAC);
 (MATCH_MP_TAC Rogers.WAUFCHE1);
 (EXISTS_TAC `2`);
 (REWRITE_TAC[IN] THEN EXPAND_TAC "xl");
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

 (EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `u0:real^3 = HD vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
 (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; NORM_MUL]);
 (REWRITE_WITH `abs (&2) = &2`);
 (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
 (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
 (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
 (REWRITE_WITH `&1 <= norm (s2 - u1) / sqrt (&2) <=> 
                 &1 * sqrt (&2) <= norm (s2 - u1:real^3)`);
 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
 (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `norm (s2 - u1) * norm (u0 - u1:real^3) * a <= 
             norm (z - u1) * norm (u0 - u1) * a`);
 (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=> 
                           &0 <= (x * y) * (b - a)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[NORM_POS_LE]);
 (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (REWRITE_TAC[DIST_POS_LE]);
 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

(* ------------------------------------------------------------------------- *)
(* OK here too *)

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

 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
                  dist (u0,s) = sqrt (&2) /\
                  mxi V ul = s`);
 (MATCH_MP_TAC MXI_EXPLICIT);
 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
 (ASM_REWRITE_TAC[]);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (UP_ASM_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN STRIP_TAC);

 (NEW_GOAL `u0 - u1 = &2 % (u0 - s1:real^3)`);
 (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
  midpoint; VECTOR_ARITH `u0 - inv (&2) % (u0 + u1) = inv (&2) % (u0 - u1)`]);
 (VECTOR_ARITH_TAC);

 (NEW_GOAL `(z - s1) dot (u0 - s1:real^3) = &0`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V vl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);

 (NEW_GOAL `between m (s2, z:real^3)`);
 (MATCH_MP_TAC BETWEEN_TRANS_2);
 (EXISTS_TAC `s3:real^3`);
 (STRIP_TAC);
 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);

 (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
 (EXPAND_TAC "s2" THEN EXPAND_TAC "zl");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 
 (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
 (EXPAND_TAC "s3" THEN EXPAND_TAC "zl");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);

 (NEW_GOAL `m:real^3 IN voronoi_list V zl`);
 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=> 
   convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
 (REWRITE_TAC[CONVEX_HULL_EQ]);
 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (NEW_GOAL `z:real^3 IN voronoi_list V zl`);
 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 (EXISTS_TAC `convex hull {m, s3:real^3}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V zl <=> 
   convex hull {m, s3} SUBSET (convex hull (voronoi_list V zl))`);
 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
 (REWRITE_TAC[CONVEX_HULL_EQ]);
 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (NEW_GOAL `norm (m - u1) <= norm (z - u1:real^3)`);
 (REWRITE_WITH `norm (m - u1) <= norm (z - u1:real^3) <=> 
                 norm (m - u1) pow 2 <= norm (z - u1:real^3) pow 2`);
 (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
 (REWRITE_WITH `m - u1 = (m - s2) + (s2 - u1:real^3) /\ 
                 z - u1 = (z - s2) + (s2 - u1:real^3)`);
 (VECTOR_ARITH_TAC);
 (REWRITE_WITH `norm (m - s2 + s2 - u1) pow 2 = 
   norm (m - s2) pow 2 + norm (s2 - u1:real^3) pow 2`);
 (NEW_GOAL `(m - s2) dot (s2 - u1:real^3) = &0`);
 (ONCE_REWRITE_TAC[VECTOR_ARITH 
   `(m - s2) dot (s2 - u1) = -- ((m - s2) dot (u1 - s2))`]);
 (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
 (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
 (REWRITE_WITH `s2:real^3 = omega_list V zl`);
 (EXPAND_TAC "s2");
 (EXPAND_TAC "zl");
 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;    
   Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
 (MATCH_MP_TAC Rogers.XNHPWAB1);
 (EXISTS_TAC `2`);
 (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V zl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);
 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);

 (REWRITE_WITH 
  `norm (z - s2 + s2 - u1) pow 2 = 
   norm (z - s2) pow 2 + norm (s2 - u1:real^3) pow 2`);
 (NEW_GOAL `(z - s2) dot (s2 - u1:real^3) = &0`);
 (ONCE_REWRITE_TAC[VECTOR_ARITH 
   `(z - s2) dot (s2 - u1) = -- ((z - s2) dot (u1 - s2))`]);
 (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
 (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
 (REWRITE_WITH `s2:real^3 = omega_list V zl`);
 (EXPAND_TAC "s2");
 (EXPAND_TAC "zl");
 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;    
   Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
 (MATCH_MP_TAC Rogers.XNHPWAB1);
 (EXISTS_TAC `2`);
 (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V zl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);
 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
 (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);

 (MP_TAC (ASSUME `between m (s2,z:real^3)`));
 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN STRIP_TAC);
 (REWRITE_TAC[ASSUME `m = u % s2 + v % z:real^3`]);
 (REWRITE_WITH 
  `(u % s2 + v % z) - s2 = (u % s2 + v % z) - (u + v) % s2:real^3`);
 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
 (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % z) - (u + v) % s2 = v % (z - s2)`]);
 (REWRITE_TAC[NORM_MUL; REAL_ARITH `(a*b) pow 2 = a pow 2 * b pow 2`;
   REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[REAL_LE_POW_2]);
 (REWRITE_WITH `abs (v:real) = v`);
 (ASM_REWRITE_TAC[REAL_ABS_REFL]);
 (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1 pow 2`]);
 (REWRITE_WITH ` v pow 2 <= &1 pow 2 <=> v <= &1`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Collect_geom.POW2_COND);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `norm (m - u1:real^3) = dist (u0, s:real^3)`);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (ASM_REWRITE_TAC[GSYM dist]);
 (UNDISCH_TAC `m IN voronoi_list V zl`);
 (ASM_REWRITE_TAC[VORONOI_LIST; VORONOI_SET]);
 (EXPAND_TAC "zl");
 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     set_of_list]);
 (STRIP_TAC);
 (NEW_GOAL `s:real^3 IN voronoi_closed V u0 /\ s IN voronoi_closed V u1`);
 (UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`);
 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);


 (NEW_GOAL `dist (s,u0) <= dist (s,u1:real^3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ONCE_REWRITE_TAC[MESON[IN] `V s <=> s IN V`]);
 (ASM_SET_TAC[]);
 (NEW_GOAL `dist (s,u1) <= dist (s,u0:real^3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ONCE_REWRITE_TAC[MESON[IN] `V s <=> s IN V`]);
 (ASM_SET_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `norm (m - u1:real^3) = sqrt (&2)`);
 (ASM_REAL_ARITH_TAC);

 (REWRITE_WITH `(z - u1) dot (u0 - u1:real^3) = &2 *  norm (u0 - s1) pow 2`);
 (REWRITE_WITH `(z - u1) dot (u0 - u1) = (z - s1) dot (u0 - u1) + 
                 (s1 - u1) dot (u0 - u1:real^3)`);
 (VECTOR_ARITH_TAC);
 (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; DOT_RMUL]);
 (REWRITE_WITH `(s1 - u1) = (u0 - s1:real^3)`);
 (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);

 (NEW_GOAL `&2 * norm (u0 - s1:real^3) pow 2 <= 
             norm (m - u1) * norm (u0 - u1) * a`);
 (EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `u0:real^3 = HD vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
 (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; NORM_MUL]);
 (REWRITE_WITH `abs (&2) = &2`);
 (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
 (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
 (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
 (REWRITE_WITH `sqrt (&2) / sqrt (&2) = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
 (REAL_ARITH_TAC);

 (NEW_GOAL `norm (m - u1) * norm (u0 - u1:real^3) * a <= 
             norm (z - u1) * norm (u0 - u1) * a`);
 (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=> 
                           &0 <= (x * y) * (b - a)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[NORM_POS_LE]);
 (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (REWRITE_TAC[DIST_POS_LE]);
 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `t1 * norm (u0 - u1:real^3) pow 2 + t5 * ((z - u1) dot (u0 - u1)) 
  <= t1 * norm (u0 - u1) pow 2 + t5 * (norm (z - u1) * norm (u0 - u1) * a)`);
 (REWRITE_TAC[REAL_ARITH `a + b * c <= a + b * d <=> &0 <= b * (d - c)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL 
 `t1 * norm (u0 - u1) pow 2 + t5 * norm (z - u1:real^3) * norm (u0 - u1) * a 
 < norm (t1 % (u0 - u1) + t5 % (z - u1)) * norm (u0 - u1) * a`);

 (REWRITE_TAC[REAL_ARITH 
 `t1 * norm (u0 - u1) pow 2 + t5 * norm (z - u1:real^3) * norm (u0 - u1) * a 
  < norm (t1 % (u0 - u1) + t5 % (z - u1)) * norm (u0 - u1) * a <=> 
  &0 < (a * norm (t1 % (u0 - u1) + t5 % (z - u1)) - t1 * norm (u0 - u1) - 
  t5 * a * norm (z - u1)) * norm (u0 - u1)`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH `&0 < a - b - c <=> b + c < a`]);

 (NEW_GOAL `t1 * norm (u0 - u1) < a * t1 * norm (u0 - u1:real^3)`);
 (REWRITE_TAC[REAL_ARITH `a * b < c * a * b <=> &0 < (--a) * b  * (&1 - c)`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LT_MUL);
 (STRIP_TAC);
 (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) / sqrt (&2) < &1 <=> hl vl < &1 * sqrt (&2) `);
 (MATCH_MP_TAC REAL_LT_LDIV_EQ);
 (MATCH_MP_TAC SQRT_POS_LT);
 (REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[REAL_MUL_LID]);

 (NEW_GOAL `a * t1 * norm (u0 - u1) + t5 * a * norm (z - u1) <=
 a * norm (t1 % (u0 - u1) + t5 % (z - u1:real^3))`);
 (REWRITE_TAC[REAL_ARITH 
  `a * t1 * norm (u0 - u1) + t5 * a * norm (z - u1) <=
   a * norm (t1 % (u0 - u1) + t5 % (z - u1)) <=>
   &0 <= a * (norm (t1 % (u0 - u1) + t5 % (z - u1)) + (--t1 * norm (u0 - u1)) -     t5 * norm (z - u1))`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `u0:real^3 = HD vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_TAC[DIST_POS_LE]);
 (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);

 (ONCE_REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
 (ABBREV_TAC `k1 = t1 % (u0 - u1) + t5 % (z - u1:real^3)`);
 (REWRITE_WITH `t5 * norm (z - u1) = norm (t5 % (z - u1:real^3))`);
 (REWRITE_TAC[NORM_MUL]);
 (REWRITE_WITH `abs t5 = t5`);
 (REWRITE_TAC[REAL_ABS_REFL]);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_WITH `--t1 * norm (u0 - u1) = norm ((--t1) % (u0 - u1:real^3))`);
 (REWRITE_TAC[NORM_MUL]);
 (REWRITE_WITH `abs (--t1) = --t1`);
 (REWRITE_TAC[REAL_ABS_REFL]);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_WITH `t5 % (z - u1) = k1 + --t1 % (u0 - u1:real^3)`);
 (EXPAND_TAC "k1" THEN VECTOR_ARITH_TAC);
 (REWRITE_TAC[NORM_TRIANGLE]);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

(* ----------------------------------------------------------------------- *)
(* Half of the proof *)


 (ASM_CASES_TAC `t2 < &0`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`);
 (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
 (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
 (NEW_GOAL `x = t1 % u0 + t2 % u1 + t5 % (z:real^3)`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "z" THEN EXPAND_TAC "t5");
 (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
 (REWRITE_TAC[REAL_ARITH `a * b / a = b * (a / a)`]);
 (ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ARITH `&0 < y ==> ~(y = &0)`;
  REAL_MUL_RID]);
 (REWRITE_TAC[dist]);
 (REWRITE_WITH `x - u0:real^3 = t2 % (u1 - u0) + t5 % (z - u0)`);
 (REWRITE_WITH `x - u0:real^3 = x - (t1 + t2 + t5) % u0`);
 (REWRITE_WITH `t1 + t2 + t5 = &1`);
 (ASM_REAL_ARITH_TAC);
 (VECTOR_ARITH_TAC);
 (REWRITE_TAC[ASSUME `x = t1 % u0 + t2 % u1 + t5 % z:real^3`]);
 (VECTOR_ARITH_TAC);

 (REWRITE_TAC[DOT_LADD; DOT_LMUL; GSYM NORM_POW_2]);
 (NEW_GOAL `(z - u0) dot (u1 - u0:real^3) <= 
             norm (z - u0:real^3) * norm (u1 - u0) * a`);

 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
 (NEW_GOAL `m = s2:real^3`);
 (EXPAND_TAC "m" THEN REWRITE_TAC[mxi] THEN COND_CASES_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `u1 - u0 = &2 % (u1 - s1:real^3)`);
 (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
  midpoint; VECTOR_ARITH `u1 - inv (&2) % (u0 + u1) = inv (&2) % (u1 - u0)`]);
 (VECTOR_ARITH_TAC);

 (NEW_GOAL `(z - s1) dot (u1 - s1:real^3) = &0`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V vl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);

 (NEW_GOAL `norm (s2 - u0) <= norm (z - u0:real^3)`);
 (REWRITE_WITH `norm (s2 - u0) <= norm (z - u0:real^3) <=> 
                 norm (s2 - u0) pow 2 <= norm (z - u0:real^3) pow 2`);
 (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
 (REWRITE_WITH `s2 - u0 = (s2 - s1) + (s1 - u0:real^3) /\ 
                  z - u0 = (z - s1) + (s1 - u0:real^3)`);
 (VECTOR_ARITH_TAC);
 (REWRITE_WITH `norm (s2 - s1 + s1 - u0) pow 2 = 
   norm (s2 - s1) pow 2 + norm (s1 - u0:real^3) pow 2`);
 (NEW_GOAL `(s2 - s1) dot (s1 - u0:real^3) = &0`);
 (REWRITE_WITH `s1 - u0 = u1 - s1:real^3`);
 (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V vl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);
 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);

 (REWRITE_WITH `norm (z - s1 + s1 - u0:real^3) pow 2 = 
                 norm (z - s1) pow 2 + norm (s1 - u0) pow 2`);
 (NEW_GOAL `(z - s1) dot (s1 - u0:real^3) = &0`);
 (REWRITE_WITH `s1 - u0 = u1 - s1:real^3`);
 (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
 (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
 (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] THEN
   REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]);
 (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);
 (REWRITE_TAC[GSYM dist; DIST_SYM]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `!a b c d:real^3. 
   dist (a, b:real^3) pow 2 <= dist (c,d) pow 2 <=> dist (a,b) <= dist (c,d)`);
 (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (SIMP_TAC[Collect_geom.POW2_COND; DIST_POS_LE]);
 (MATCH_MP_TAC CLOSEST_POINT_LE);
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);

 (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
 (EXPAND_TAC "zl" THEN REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
 (EXPAND_TAC "zl" THEN EXPAND_TAC "s3");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 (ASM_MESON_TAC[]);
 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=> 
   convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
 (REWRITE_TAC[CONVEX_HULL_EQ]);
 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (REWRITE_WITH `(z - u0) dot (u1 - u0:real^3) = &2 *  norm (u1 - s1) pow 2`);
 (REWRITE_WITH `(z - u0) dot (u1 - u0) = (z - s1) dot (u1 - u0) + 
                 (s1 - u0) dot (u1 - u0:real^3)`);
 (VECTOR_ARITH_TAC);
 (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; DOT_RMUL]);
 (REWRITE_WITH `(s1 - u0) = (u1 - s1:real^3)`);
 (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);


 (NEW_GOAL `&2 * norm (u1 - s1:real^3) pow 2 <= 
             norm (s2 - u0) * norm (u1 - u0) * a`);
 (NEW_GOAL `norm (s2 - u0:real^3) >= sqrt (&2)`);
 (NEW_GOAL `norm (s2 - u0:real^3) >= 
             hl (truncate_simplex 2 (ul:(real^3)list))`);
 (REWRITE_TAC[GSYM dist]);
 (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
 (ABBREV_TAC `xl:(real^3)list = truncate_simplex 2 ul`);

 (REWRITE_WITH `s2 = omega_list V xl`);
 (ONCE_REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
 (REWRITE_TAC[Marchal_cells.OMEGA_LIST_TRUNCATE_2; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (EXPAND_TAC "xl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (REWRITE_WITH `u0:real^3 = HD xl`);
 (EXPAND_TAC "xl");
 (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; 
   TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
 (MATCH_MP_TAC Rogers.WAUFCHE1);
 (EXISTS_TAC `2`);
 (REWRITE_TAC[IN] THEN EXPAND_TAC "xl");
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

 (EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `!w:real^3. w IN set_of_list vl
                  ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
 (MATCH_MP_TAC Rogers.HL_PROPERTIES);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (EXPAND_TAC "vl");
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (SET_TAC[]);

 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
 (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; NORM_MUL]);
 (REWRITE_WITH `abs (&2) = &2`);
 (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
 (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
 (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
 (REWRITE_WITH `&1 <= norm (s2 - u0) / sqrt (&2) <=> 
                 &1 * sqrt (&2) <= norm (s2 - u0:real^3)`);
 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
 (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `norm (s2 - u0) * norm (u1 - u0:real^3) * a <= 
             norm (z - u0) * norm (u1 - u0) * a`);
 (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=> 
                           &0 <= (x * y) * (b - a)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[NORM_POS_LE]);
 (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (REWRITE_TAC[DIST_POS_LE]);
 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

(* ------------------------------------------------------------------------- *)
(* OK here too *)

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

 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
                  dist (u0,s) = sqrt (&2) /\
                  mxi V ul = s`);
 (MATCH_MP_TAC MXI_EXPLICIT);
 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
 (ASM_REWRITE_TAC[]);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (UP_ASM_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN STRIP_TAC);

 (NEW_GOAL `u1 - u0 = &2 % (u1 - s1:real^3)`);
 (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
  midpoint; VECTOR_ARITH `u1 - inv (&2) % (u0 + u1) = inv (&2) % (u1 - u0)`]);
 (VECTOR_ARITH_TAC);

 (NEW_GOAL `(z - s1) dot (u1 - s1:real^3) = &0`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V vl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);

 (NEW_GOAL `between m (s2, z:real^3)`);
 (MATCH_MP_TAC BETWEEN_TRANS_2);
 (EXISTS_TAC `s3:real^3`);
 (STRIP_TAC);
 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);

 (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
 (EXPAND_TAC "s2" THEN EXPAND_TAC "zl");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 
 (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
 (EXPAND_TAC "s3" THEN EXPAND_TAC "zl");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);

 (NEW_GOAL `m:real^3 IN voronoi_list V zl`);
 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=> 
   convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
 (REWRITE_TAC[CONVEX_HULL_EQ]);
 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (NEW_GOAL `z:real^3 IN voronoi_list V zl`);
 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 (EXISTS_TAC `convex hull {m, s3:real^3}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V zl <=> 
   convex hull {m, s3} SUBSET (convex hull (voronoi_list V zl))`);
 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
 (REWRITE_TAC[CONVEX_HULL_EQ]);
 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (NEW_GOAL `norm (m - u0) <= norm (z - u0:real^3)`);
 (REWRITE_WITH `norm (m - u0) <= norm (z - u0:real^3) <=> 
                 norm (m - u0) pow 2 <= norm (z - u0:real^3) pow 2`);
 (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
 (REWRITE_WITH `m - u0 = (m - s2) + (s2 - u0:real^3) /\ 
                 z - u0 = (z - s2) + (s2 - u0:real^3)`);
 (VECTOR_ARITH_TAC);
 (REWRITE_WITH `norm (m - s2 + s2 - u0) pow 2 = 
   norm (m - s2) pow 2 + norm (s2 - u0:real^3) pow 2`);
 (NEW_GOAL `(m - s2) dot (s2 - u0:real^3) = &0`);
 (ONCE_REWRITE_TAC[VECTOR_ARITH 
   `(m - s2) dot (s2 - u0) = -- ((m - s2) dot (u0 - s2))`]);
 (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
 (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
 (REWRITE_WITH `s2:real^3 = omega_list V zl`);
 (EXPAND_TAC "s2");
 (EXPAND_TAC "zl");
 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;    
   Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
 (MATCH_MP_TAC Rogers.XNHPWAB1);
 (EXISTS_TAC `2`);
 (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V zl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);
 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);

 (REWRITE_WITH 
  `norm (z - s2 + s2 - u0) pow 2 = 
   norm (z - s2) pow 2 + norm (s2 - u0:real^3) pow 2`);
 (NEW_GOAL `(z - s2) dot (s2 - u0:real^3) = &0`);
 (ONCE_REWRITE_TAC[VECTOR_ARITH 
   `(z - s2) dot (s2 - u0) = -- ((z - s2) dot (u0 - s2))`]);
 (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
 (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
 (REWRITE_WITH `s2:real^3 = omega_list V zl`);
 (EXPAND_TAC "s2");
 (EXPAND_TAC "zl");
 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;    
   Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
 (MATCH_MP_TAC Rogers.XNHPWAB1);
 (EXISTS_TAC `2`);
 (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `voronoi_list V zl`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
   ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (SET_TAC[]);
 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
 (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);

 (MP_TAC (ASSUME `between m (s2,z:real^3)`));
 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN STRIP_TAC);
 (REWRITE_TAC[ASSUME `m = u % s2 + v % z:real^3`]);
 (REWRITE_WITH 
  `(u % s2 + v % z) - s2 = (u % s2 + v % z) - (u + v) % s2:real^3`);
 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
 (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % z) - (u + v) % s2 = v % (z - s2)`]);
 (REWRITE_TAC[NORM_MUL; REAL_ARITH `(a*b) pow 2 = a pow 2 * b pow 2`;
   REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[REAL_LE_POW_2]);
 (REWRITE_WITH `abs (v:real) = v`);
 (ASM_REWRITE_TAC[REAL_ABS_REFL]);
 (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1 pow 2`]);
 (REWRITE_WITH ` v pow 2 <= &1 pow 2 <=> v <= &1`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Collect_geom.POW2_COND);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `norm (m - u0:real^3) = dist (u0, s:real^3)`);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (ASM_REWRITE_TAC[GSYM dist]);
 (NEW_GOAL `norm (m - u0:real^3) = sqrt (&2)`);
 (ASM_REAL_ARITH_TAC);

 (REWRITE_WITH `(z - u0) dot (u1 - u0:real^3) = &2 *  norm (u1 - s1) pow 2`);
 (REWRITE_WITH `(z - u0) dot (u1 - u0) = (z - s1) dot (u1 - u0) + 
                 (s1 - u0) dot (u1 - u0:real^3)`);
 (VECTOR_ARITH_TAC);
 (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; DOT_RMUL]);
 (REWRITE_WITH `(s1 - u0) = (u1 - s1:real^3)`);
 (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);

 (NEW_GOAL `&2 * norm (u1 - s1:real^3) pow 2 <= 
             norm (m - u0) * norm (u1 - u0) * a`);
 (EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `!w:real^3. w IN set_of_list vl
                  ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
 (MATCH_MP_TAC Rogers.HL_PROPERTIES);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (EXPAND_TAC "vl");
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (SET_TAC[]);

 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
 (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; NORM_MUL]);
 (REWRITE_WITH `abs (&2) = &2`);
 (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
 (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
 (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
 (REWRITE_WITH `sqrt (&2) / sqrt (&2) = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
 (REAL_ARITH_TAC);

 (NEW_GOAL `norm (m - u0) * norm (u1 - u0:real^3) * a <= 
             norm (z - u0) * norm (u1 - u0) * a`);
 (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=> 
                           &0 <= (x * y) * (b - a)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[NORM_POS_LE]);
 (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `!w:real^3. w IN set_of_list vl
                  ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
 (MATCH_MP_TAC Rogers.HL_PROPERTIES);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (EXPAND_TAC "vl");
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (SET_TAC[]);
 (REWRITE_TAC[DIST_POS_LE]);
 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);


 (NEW_GOAL `t2 * norm (u1 - u0:real^3) pow 2 + t5 * ((z - u0) dot (u1 - u0)) 
  <= t2 * norm (u1 - u0) pow 2 + t5 * (norm (z - u0) * norm (u1 - u0) * a)`);
 (REWRITE_TAC[REAL_ARITH `a + b * c <= a + b * d <=> &0 <= b * (d - c)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL 
 `t2 * norm (u1 - u0) pow 2 + t5 * norm (z - u0:real^3) * norm (u1 - u0) * a 
 < norm (t2 % (u1 - u0) + t5 % (z - u0)) * norm (u1 - u0) * a`);

 (REWRITE_TAC[REAL_ARITH 
 `t2 * norm (u1 - u0) pow 2 + t5 * norm (z - u0:real^3) * norm (u1 - u0) * a 
  < norm (t2 % (u1 - u0) + t5 % (z - u0)) * norm (u1 - u0) * a <=> 
  &0 < (a * norm (t2 % (u1 - u0) + t5 % (z - u0)) - t2 * norm (u1 - u0) - 
  t5 * a * norm (z - u0)) * norm (u1 - u0)`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH `&0 < a - b - c <=> b + c < a`]);

 (NEW_GOAL `t2 * norm (u1 - u0) < a * t2 * norm (u1 - u0:real^3)`);
 (REWRITE_TAC[REAL_ARITH `a * b < c * a * b <=> &0 < (--a) * b  * (&1 - c)`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (MATCH_MP_TAC REAL_LT_MUL);
 (STRIP_TAC);
 (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> b = a`]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) / sqrt (&2) < &1 <=> hl vl < &1 * sqrt (&2) `);
 (MATCH_MP_TAC REAL_LT_LDIV_EQ);
 (MATCH_MP_TAC SQRT_POS_LT);
 (REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[REAL_MUL_LID]);

 (NEW_GOAL `a * t2 * norm (u1 - u0) + t5 * a * norm (z - u0) <=
 a * norm (t2 % (u1 - u0) + t5 % (z - u0:real^3))`);
 (REWRITE_TAC[REAL_ARITH 
  `a * t2 * norm (u1 - u0) + t5 * a * norm (z - u0) <=
   a * norm (t2 % (u1 - u0) + t5 % (z - u0)) <=>
   &0 <= a * (norm (t2 % (u1 - u0) + t5 % (z - u0)) + (--t2 * norm (u1 - u0)) -     t5 * norm (z - u0))`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `!w:real^3. w IN set_of_list vl
                  ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
 (MATCH_MP_TAC Rogers.HL_PROPERTIES);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (EXPAND_TAC "vl");
 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   
   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (SET_TAC[]);

 (MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_TAC[DIST_POS_LE]);
 (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);

 (ONCE_REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
 (ABBREV_TAC `k1 = t2 % (u1 - u0) + t5 % (z - u0:real^3)`);
 (REWRITE_WITH `t5 * norm (z - u0) = norm (t5 % (z - u0:real^3))`);
 (REWRITE_TAC[NORM_MUL]);
 (REWRITE_WITH `abs t5 = t5`);
 (REWRITE_TAC[REAL_ABS_REFL]);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_WITH `--t2 * norm (u1 - u0) = norm ((--t2) % (u1 - u0:real^3))`);
 (REWRITE_TAC[NORM_MUL]);
 (REWRITE_WITH `abs (--t2) = --t2`);
 (REWRITE_TAC[REAL_ABS_REFL]);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_WITH `t5 % (z - u0) = k1 + --t2 % (u1 - u0:real^3)`);
 (EXPAND_TAC "k1" THEN VECTOR_ARITH_TAC);
 (REWRITE_TAC[NORM_TRIANGLE]);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (ASM_REAL_ARITH_TAC);

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

 (NEW_GOAL `t3 = &0 /\ t4 = &0`);
 (ASM_REAL_ARITH_TAC);

 (ASM_CASES_TAC `t1 < &0`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`);
 (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
 (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);

 (REWRITE_TAC[dist]);
 (REWRITE_WITH `x - u1 = t1 % (u0 - u1:real^3)`);
 (REWRITE_WITH `x - u1 = x - (t1 + t2) % u1:real^3`);
 (REWRITE_WITH `t1 + t2 = &1`);
 (ASM_REAL_ARITH_TAC);
 (VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (VECTOR_ARITH_TAC);

 (REWRITE_TAC[DOT_LMUL;GSYM NORM_POW_2]);
 (NEW_GOAL `t1 * norm (u0 - u1:real^3) pow 2 < &0`);
 (REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < (--a) * b`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]);
 (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);

 (NEW_GOAL `&0 <= norm (t1 % (u0 - u1:real^3)) * norm (u0 - u1) * a`);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[NORM_POS_LE]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[NORM_POS_LE]);
 (EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) = 
   dist (circumcenter (set_of_list vl),HD vl)`);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_TAC[DIST_POS_LE]);
 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `t2 < &0`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`);
 (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
 (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);

 (REWRITE_TAC[dist]);
 (REWRITE_WITH `x - u0 = t2 % (u1 - u0:real^3)`);
 (REWRITE_WITH `x - u0 = x - (t1 + t2) % u0:real^3`);
 (REWRITE_WITH `t1 + t2 = &1`);
 (ASM_REAL_ARITH_TAC);
 (VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (VECTOR_ARITH_TAC);

 (REWRITE_TAC[DOT_LMUL;GSYM NORM_POW_2]);
 (NEW_GOAL `t2 * norm (u1 - u0:real^3) pow 2 < &0`);
 (REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < (--a) * b`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]);
 (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);

 (NEW_GOAL `&0 <= norm (t2 % (u1 - u0:real^3)) * norm (u1 - u0) * a`);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[NORM_POS_LE]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (REWRITE_TAC[NORM_POS_LE]);
 (EXPAND_TAC "a");
 (REWRITE_WITH `hl (vl:(real^3)list) = 
   dist (circumcenter (set_of_list vl),HD vl)`);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 (MATCH_MP_TAC REAL_LE_DIV);
 (REWRITE_TAC[DIST_POS_LE]);
 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (ASM_REAL_ARITH_TAC);

 (REWRITE_TAC[CONVEX_HULL_4; IN; IN_ELIM_THM]);
 (NEW_GOAL `between m (s2, s3:real^3)`);
 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
 (EXPAND_TAC "m");
 (REWRITE_TAC[mxi]);
 (COND_CASES_TAC);
 (ASM_REWRITE_TAC[BETWEEN_REFL]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
                  dist (u0,s) = sqrt (&2) /\
                  mxi V ul = s`);
 (MATCH_MP_TAC MXI_EXPLICIT);
 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
 (ASM_REWRITE_TAC[]);
 (FIRST_ASSUM CHOOSE_TAC THEN UP_ASM_TAC);
 (ASM_REWRITE_TAC[] THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);

 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
 (EXISTS_TAC `t3 * u` THEN EXISTS_TAC `t3 * v + t4`);
 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD]);
 (STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH `t1 + t2 + t3 * u + t3 * v + t4 = 
   t1 + t2 + t3 * (u + v) + t4`]);
 (ASM_REWRITE_TAC[REAL_MUL_RID]);
 (VECTOR_ARITH_TAC);
 (SET_TAC[])]);;
(* Finished *)

end;;