(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma:  URRPHBZ2                                                *)
(*      Chaper    : Packing (Marchal Cells)                                  *)
(*      Date      : December 2011                                            *)
(*      With special thanks to John Harrison for the lemma OPEN_RCONE_GT     *)
(* ========================================================================= *)
(*                     FILES NEED TO BE LOADED                               *)

(*  flyspeck_needs "packing/marchal_cells_2.hl";;                            *)
(* flyspeck_needs "packing/LEPJBDJ.hl"                                       *)

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

module Urrphbz2 = 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;;

let EVENTUALLY_RADIAL_RCONE_GE_ABC_A = prove_by_refinement (
 `!a u0 u1:real^3. eventually_radial u0 (rcone_ge u0 u1 a)`,
[(STRIP_TAC THEN REWRITE_TAC[eventually_radial; radial]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[SET_RULE `a INTER b SUBSET b`]);
 (EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_ARITH `&1 > &0`]);
 (REPEAT STRIP_TAC);
 (UNDISCH_TAC `u0 + u IN rcone_ge u0 u1 a INTER ball (u0:real^3,&1)`);
 (REWRITE_TAC[rcone_ge; rconesgn; IN_INTER; ball; IN; IN_ELIM_THM; dist;  
   VECTOR_ARITH `(u + v) - u:real^3 = v /\ (u - (u + t % v)) = (--t % v)`;  
   NORM_MUL; REAL_ABS_NEG]);
 (REWRITE_WITH `abs t = t`);
 (ASM_SIMP_TAC[REAL_ARITH `t > &0 ==> &0 <= t`; REAL_ABS_REFL]);
 (ASM_REWRITE_TAC[DOT_LMUL]);
 (STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH `t * a >= (t * b) * c <=> &0 <= (a - b * c) * t`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC)]);;


(* ========================================================================== *)
(*      This lemma is in multivariate/flyspeck.hl                             *)
(* ========================================================================== *)
 
let OPEN_RCONE_GT = prove
  (`!v0 v1:real^N a. open(rcone_gt v0 v1 a)`,
   REWRITE_TAC[rcone_gt; rconesgn] THEN
   GEOM_ORIGIN_TAC `v0:real^N` THEN REPEAT GEN_TAC THEN
   REWRITE_TAC[VECTOR_SUB_RZERO; DIST_0] THEN
   MP_TAC(ISPECL [`\x:real^N. lift(x dot v1 - norm x * norm v1 * a)`;
                  `{x:real^1 | x$1 > &0}`]
         CONTINUOUS_OPEN_PREIMAGE_UNIV) THEN
   REWRITE_TAC[OPEN_HALFSPACE_COMPONENT_GT] THEN REWRITE_TAC[GSYM drop] THEN
   REWRITE_TAC[IN_ELIM_THM; real_gt; REAL_SUB_LT; LIFT_DROP] THEN
   DISCH_THEN MATCH_MP_TAC THEN GEN_TAC THEN REWRITE_TAC[LIFT_SUB] THEN
   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[LIFT_CMUL] THEN
   MATCH_MP_TAC CONTINUOUS_SUB THEN ONCE_REWRITE_TAC[DOT_SYM] THEN
   REWRITE_TAC[REWRITE_RULE[o_DEF] CONTINUOUS_AT_LIFT_DOT] THEN
   MATCH_MP_TAC CONTINUOUS_CMUL THEN
   REWRITE_TAC[REWRITE_RULE[o_DEF] CONTINUOUS_AT_LIFT_NORM]);;

let EVENTUALLY_RADIAL_RCONE_GE_ABC_B = prove_by_refinement (
 `!a u0 u1:real^3. ~(u0 = u1) /\ (&0 < a) /\ (a < &1) ==> 
    eventually_radial u1 (rcone_ge u0 u1 a)`,
[(STRIP_TAC THEN REWRITE_TAC[eventually_radial; radial]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[SET_RULE `a INTER b SUBSET b`]);

 (NEW_GOAL `u1:real^3 IN rcone_gt u0 u1 a`);
 (REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; GSYM NORM_POW_2; GSYM dist; REAL_POW_2; REAL_ARITH `x * x > x * x * a <=> &0 < (&1 - a) * x * x`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (ASM_SIMP_TAC[REAL_ARITH `&0 < a - b <=> b < a`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (ASM_SIMP_TAC[DIST_POS_LT]);

 (NEW_GOAL `open (rcone_gt (u0:real^3) u1 a)`);
 (ASM_SIMP_TAC[OPEN_RCONE_GT]);
 (UP_ASM_TAC THEN REWRITE_TAC[open_def] THEN DISCH_TAC);
 (NEW_GOAL `?e. &0 < e /\
                   (!x'. dist (x',u1:real^3) < e ==> x' IN rcone_gt u0 u1 a)`);

 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC THEN EXISTS_TAC `e:real`);
 (REPEAT STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[IN_INTER] THEN STRIP_TAC);
 (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
 (EXISTS_TAC `rcone_gt (u0:real^3) u1 a`);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (REWRITE_TAC[dist; VECTOR_ARITH `(a +b:real^3) - a = b`; NORM_MUL]);
 (REWRITE_WITH `abs t = t`);
 (ASM_SIMP_TAC[REAL_ABS_REFL; REAL_ARITH `t > &0 ==> &0 <= t`]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]);
 (REWRITE_TAC[ball; IN; IN_ELIM_THM; dist; VECTOR_ARITH `a - (a + t % b) = (-- t) % b`; NORM_MUL; REAL_ABS_NEG]);
 (REWRITE_WITH `abs t = t`);
 (ASM_SIMP_TAC[REAL_ABS_REFL; REAL_ARITH `t > &0 ==> &0 <= t`]);
 (ASM_REWRITE_TAC[])]);;

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

let EVENTUALLY_RADIAL_AFF_GE = prove_by_refinement(
 `!a b c d:real^3. DISJOINT {a,b} {c, d}  
   ==> eventually_radial a (aff_ge {a,b}{c,d})`,
[(STRIP_TAC THEN REWRITE_TAC[eventually_radial; radial]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[SET_RULE `a INTER b SUBSET b`]);
 (EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_ARITH `&1 > &0`]);
 (ASM_SIMP_TAC[AFF_GE_2_2]);
 (REWRITE_TAC[IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (EXISTS_TAC `&1 - t * t2 - t * t3 - t * t4`);
 (EXISTS_TAC `t * t2` THEN EXISTS_TAC `t * t3` THEN EXISTS_TAC `t * t4`);
 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_ARITH `t > &0 ==> &0 <= t`]);
 (STRIP_TAC);
 (REAL_ARITH_TAC);
 (REWRITE_WITH `u = t1 % a + t2 % b + t3 % c + t4 % d - a:real^3`);
 (UNDISCH_TAC `a + u:real^3 = t1 % a + t2 % b + t3 % c + t4 % d` THEN VECTOR_ARITH_TAC);
 (REWRITE_WITH 
`a + t % (t1 % a + t2 % b + t3 % c + t4 % d - a) =
 (&1 - t * t2 - t * t3 - t * t4) % a +
 (t * t2) % (b:real^3) + (t * t3) % c + (t * t4) % d 
 <=> (t * t1 + t * t2 + t * t3 + t * t4 - t) % a = vec 0`);
 (VECTOR_ARITH_TAC);
 (ASM_REWRITE_TAC[REAL_ARITH `t * t1 + t * t2 + t * t3 + t * t4 - t = t * ((t1
  + t2 + t3 + t4) - &1)`; REAL_SUB_REFL; REAL_MUL_RZERO; VECTOR_MUL_LZERO]);
 (REWRITE_TAC[ball; IN_ELIM_THM; dist; VECTOR_ARITH `a - (a + t % s) =
  (-- t) % s`; NORM_MUL; REAL_ABS_NEG]);
 (REWRITE_WITH `abs t = t`);
 (ASM_SIMP_TAC[REAL_ABS_REFL; REAL_ARITH `t > &0 ==> &0 <= t`]);
 (ASM_REWRITE_TAC[])]);;

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

let FUN_AFFINE_KLEMMA = prove_by_refinement (
 `!a:real^3 b c d. 
    aff_dim {a,b,c} = &2 /\ ~(d IN affine hull {a,b,c}) 
    ==> ~(a IN convex hull {b,c,d})`,
[(REWRITE_TAC[CONVEX_HULL_3;AFFINE_HULL_3; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `~(w = &0)`);
 (NEW_GOAL `?u v w. u + v + w = &1 /\ d = u % a + v % b + w % c:real^3`);
 (EXISTS_TAC `&1 / w` THEN EXISTS_TAC `-- u / w` THEN EXISTS_TAC `-- v/ w`);
 (STRIP_TAC);
 (REWRITE_TAC[REAL_ARITH `&1 / w + --u / w + --v / w = (&1 - u - v) / w`;
   GSYM (ASSUME `u + v + w = &1`); REAL_ARITH `(u + v + w) - u - v = w`]); 
 (ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_DIV_REFL]);
 (REWRITE_TAC[VECTOR_ARITH `&1 / w % a + --u / w % b + --v / w % c = 
   (&1 / w) % (a - u % b - v % c)`]);
 (ASM_REWRITE_TAC[VECTOR_ARITH `(a + b + c) - a - b = c:real^3`;   VECTOR_MUL_ASSOC]);
 (REWRITE_WITH `&1 / w * w = &1`);
 (ASM_REWRITE_TAC[GSYM Trigonometry2.NOT_0_INVERTABLE]);
 (VECTOR_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[]);
 (STRIP_TAC);
 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID]);
 (STRIP_TAC);
 (UNDISCH_TAC `aff_dim {a, b, c:real^3} = &2`);
 (REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
 (REWRITE_WITH `affine hull {a,b,c} = affine hull {b,c:real^3}`);
 (MATCH_MP_TAC AFFINE_HULLS_EQ);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[SUBSET;AFFINE_HULL_2;
   SET_RULE `x IN {a,b,c} <=> (x = a \/x = b \/ x = c)`; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (VECTOR_ARITH_TAC);
 (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (VECTOR_ARITH_TAC);

 (REWRITE_TAC[SUBSET;AFFINE_HULL_3;
   SET_RULE `x IN {b,c} <=> (x = b \/ x = c)`; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (REAL_ARITH_TAC);
 (VECTOR_ARITH_TAC);

 (EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (REAL_ARITH_TAC);
 (VECTOR_ARITH_TAC);
 (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
 (REWRITE_TAC[AFF_DIM_2]);
 (COND_CASES_TAC);
 (ARITH_TAC);
 (ARITH_TAC)]);;

(* ========================================================================== *)
(* ========================================================================== *)
(*                  The main theorem                                          *)
(* ========================================================================== *)
(* ========================================================================== *)


let URRPHBZ2 = prove_by_refinement (URRPHBZ2_concl,
[(REPEAT STRIP_TAC);
 (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
 (MP_TAC (ASSUME `barV V 3 ul`));
 (REWRITE_TAC[BARV_3_EXPLICIT]);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (ASM_CASES_TAC `~ (mcell k V ul) (v:real^3)`);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_NOT_IN_CLOSED_SET);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[CLOSED_MCELL]);
 (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~A <=> A`] THEN DISCH_TAC);

(* ====Case 1:  k = 0 ====== *) (* FINISHED *)

 (ASM_CASES_TAC `k = 0`);
 (NEW_GOAL `v = u0:real^3`);
 (REWRITE_WITH `u0:real^3 = HD ul`);
 (ASM_REWRITE_TAC[HD]);
 (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell0]);
 (REWRITE_TAC[DIFF;IN_ELIM_THM]);
 (MESON_TAC[IN]);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_NOT_IN_CLOSED_SET );
 (STRIP_TAC);
 (REWRITE_TAC[MCELL_EXPLICIT; mcell0]);
 (REWRITE_TAC[DIFF;IN_ELIM_THM; MESON[] `!X Y. ~(X /\ ~Y) <=> (~X \/ Y) `]);
 (DISJ2_TAC);
 (REWRITE_TAC[HD;ball;IN;IN_ELIM_THM;DIST_REFL]);
 (MATCH_MP_TAC SQRT_POS_LT); 
 (REAL_ARITH_TAC);
 (MATCH_MP_TAC CLOSED_MCELL);
 (ASM_MESON_TAC[]);

(* ====Case 2:  k = 1 ====== *)  (* Finished *)

 (ASM_CASES_TAC `k = 1`);
 (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell1]);
 (COND_CASES_TAC);
 (REWRITE_TAC[HD;TL;TRUNCATE_SIMPLEX_EXPLICIT_1;rcone_gt;rconesgn]);
 (REWRITE_WITH 
` rogers V [u0; u1; u2; u3:real^3] INTER cball (u0,sqrt (&2)) DIFF
  {x | (x - u0) dot (u1 - u0) >
       dist (x,u0) * dist (u1,u0) * hl [u0; u1] / sqrt (&2)} =
  rogers V [u0; u1; u2; u3] INTER cball (u0,sqrt (&2)) INTER
  {x | (x - u0) dot (u1 - u0) <=
       dist (x,u0) * dist (u1,u0) * hl [u0; u1] / sqrt (&2)}`);
 (REWRITE_TAC[Vol1.SET_EQ; IN_INTER; IN_DIFF; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `v = u0:real^3`);
 (REWRITE_WITH `u0:real^3 = HD ul`);
 (ASM_REWRITE_TAC[HD]);
 (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[IN]);
 (NEW_GOAL `mcell 1 V ul (v:real^3)`);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[MCELL_EXPLICIT; mcell1]);
 (COND_CASES_TAC);
 (TRUONG_SET_TAC[]);
 (DISCH_TAC THEN NEW_GOAL `F`);
 (UP_ASM_TAC THEN ASM_MESON_TAC[GSYM IN; NOT_IN_EMPTY]);
 (UP_ASM_TAC THEN MESON_TAC[]);

 (MATCH_MP_TAC EVENTUALLY_RADIAL_INTER);
 (STRIP_TAC);
  (* e_radial rogers *) 
 (REWRITE_TAC[ROGERS; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
 (REWRITE_TAC [SET_OF_0_TO_3]);
 (REWRITE_WITH `IMAGE (omega_list_n V [u0; u1; u2; u3:real^3]) {0, 1, 2, 3} = 
   {omega_list_n V [u0; u1; u2; u3] 0, omega_list_n V [u0; u1; u2; u3] 1,
    omega_list_n V [u0; u1; u2; u3] 2, omega_list_n V [u0; u1; u2; u3] 3}`);
 (REWRITE_TAC[IMAGE]);
 (SET_TAC[]);
 (ABBREV_TAC `a = omega_list_n V [u0; u1; u2; u3:real^3] 0`);
 (REWRITE_WITH `a = u0:real^3`);
 (EXPAND_TAC "a" THEN REWRITE_TAC[OMEGA_LIST_N;HD]);

 (ONCE_ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 (ABBREV_TAC `vl = [u0;u1;u2;u3:real^3]`);

 (REWRITE_WITH `u0:real^3 = HD vl`);
 (EXPAND_TAC "vl" THEN ASM_REWRITE_TAC[HD]);
 (MATCH_MP_TAC U0_NOT_IN_CONVEX_HULL_FROM_ROGERS) ;
 (ASM_MESON_TAC[]);

  (* e_radial cball *) 

 (MATCH_MP_TAC EVENTUALLY_RADIAL_INTER);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[eventually_radial]);
 (EXISTS_TAC `&1`);
 (REWRITE_TAC[radial; REAL_ARITH `&1 > &0`; INTER_SUBSET]);
 (REPEAT STRIP_TAC);
 (REWRITE_WITH `cball (u0:real^3,sqrt (&2)) INTER ball (u0,&1) = ball (u0, &1)`);
 (MATCH_MP_TAC (SET_RULE `b SUBSET a ==> a INTER b = b`));
 (REWRITE_TAC[SUBSET; ball; cball; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `&1 < sqrt (&2)`);
 (REWRITE_TAC[ZERO_LT_SQRT_2]);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[ball; IN; IN_ELIM_THM; dist; VECTOR_ARITH `a - (a + b:real^3) = --b`; NORM_NEG; NORM_MUL]);
 (REWRITE_WITH `abs t = t`);
 (REWRITE_TAC[REAL_ABS_REFL]);
 (ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[]);

(* e_radial R^3 \ rcone_gt *)

 (ASM_REWRITE_TAC[eventually_radial]);
 (EXISTS_TAC `&1`);
 (REWRITE_TAC[radial; REAL_ARITH `&1 > &0`; INTER_SUBSET; IN_INTER; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);

 (REWRITE_WITH `((u0 + t % u) - u0) dot (u1 - u0:real^3) = 
                  t * (((u0 + u) - u0) dot (u1 - u0))`);
 (VECTOR_ARITH_TAC);
 (REWRITE_WITH `dist (u0 + t % u,u0) = abs t * dist (u0 + u,u0:real^3)`);
 (REWRITE_TAC[dist; VECTOR_ARITH `(a + (b:real^3)) - a = b`; NORM_MUL]);
 (REWRITE_WITH `abs t = t`);
 (REWRITE_TAC[REAL_ABS_REFL]);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC [REAL_ARITH  `t * s <= (t * a) * b <=> &0 <= t * (a * b - s)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[ball;IN_ELIM_THM]);
 (REWRITE_WITH `dist (u0,u0 + t % u) = abs t * norm (u:real^3)`);
 (REWRITE_TAC[dist; VECTOR_ARITH `(a + (b:real^3)) - a = b /\ 
               r:real^3 - (r + t) = -- t`; NORM_MUL; NORM_NEG]);
 (REWRITE_WITH `abs t = t`);
 (REWRITE_TAC[REAL_ABS_REFL]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[EVENTUALLY_RADIAL_EMPTY]);

(* ======================================================================= *)
(* ====Case 2:  k >= 4 ====== *) 

 (ASM_CASES_TAC `k >= 4`);
 (UNDISCH_TAC `mcell k V ul v`);
 (REWRITE_WITH `mcell k V ul = mcell4 V ul`);
 (MP_TAC MCELL_EXPLICIT THEN STRIP_TAC);
 (NEW_GOAL `mcell 0 V ul = mcell0 V ul /\
             mcell 1 V ul = mcell1 V ul /\
             mcell 2 V ul = mcell2 V ul /\
             mcell 3 V ul = mcell3 V ul /\
            (k >= 4 ==> mcell k V ul = mcell4 V ul)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SIMP_TAC[]);
 (REWRITE_TAC[mcell4]);
 (COND_CASES_TAC);
 (ASM_REWRITE_TAC[set_of_list]);
 (STRIP_TAC);
 (ABBREV_TAC `S = {u0, u1,u2, u3:real^3}`);
 (ABBREV_TAC `s3 = omega_list V (ul:(real^3)list)`);

 (NEW_GOAL `v IN {u0, u1 ,u2:real^3, u3}`);
 (ASM_CASES_TAC `(v:real^3) IN S`);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `!x:real^3. x IN convex hull S /\ ~(x IN S)
                  ==> (?y. y IN S /\ norm (x - s3) < norm (y - s3))`);
 (MATCH_MP_TAC SIMPLEX_FURTHEST_LT_2);
 (EXPAND_TAC "S");
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (NEW_GOAL `?y:real^3. y IN S /\ norm (v - s3) < norm (y - s3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[IN]);
 (UP_ASM_TAC THEN EXPAND_TAC "S" THEN STRIP_TAC);
 (NEW_GOAL `s3 IN (voronoi_closed V (y:real^3))`);
 (EXPAND_TAC "s3");
 (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`)); 
 (EXISTS_TAC `voronoi_list V (ul:(real^3)list)`);
 (STRIP_TAC);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[VORONOI_LIST; VORONOI_SET; set_of_list]);
 (NEW_GOAL `y:real^3 IN S`);
 (ASM_MESON_TAC[]);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (REWRITE_TAC[dist]);
 (STRIP_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `norm (y - s3) <= norm (v - s3:real^3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (UNDISCH_TAC `v:real^3 IN V` THEN MESON_TAC[IN]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

(* Case v = u0 *)
 (ASM_CASES_TAC `v = u0:real^3`);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "S");
 (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 (NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} = &3`);
 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (MATCH_MP_TAC Rogers.MHFTTZN1);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} <= &3 - &1`);
 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = u0 INSERT {u1,u2,u3:real^3}`);
 (SET_TAC[]);
 (ONCE_REWRITE_TAC[AFF_DIM_INSERT]);
 (COND_CASES_TAC);

 (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (NEW_GOAL `aff_dim {u1, u2, u3} <= &(CARD{u1,u2,u3:real^3}) - &1`);
 (MATCH_MP_TAC AFF_DIM_LE_CARD);
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `u0 IN affine hull {u1,u2,u3:real^3}`);
 (UNDISCH_TAC `u0 IN convex hull {u1, u2, u3:real^3}`);
 (MATCH_MP_TAC (SET_RULE `(b SUBSET c) ==> ((a IN b) ==> (a IN c))`));
 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

(* Case v = u1 *)
 (ASM_CASES_TAC `v = u1:real^3`);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "S");
 (REWRITE_WITH `{u0, u1, u2, u3} = {u1, u0, u2, u3:real^3}`);
 (SET_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 (NEW_GOAL `aff_dim {u1, u0, u2, u3:real^3} = &3`);
 (REWRITE_WITH `{u1, u0, u2, u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (EXPAND_TAC "S" THEN SET_TAC[]);
 (MATCH_MP_TAC Rogers.MHFTTZN1);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `aff_dim {u1, u0, u2, u3:real^3} <= &3 - &1`);
 (REWRITE_WITH `{u1, u0, u2, u3:real^3} = u1 INSERT {u0,u2,u3:real^3}`);
 (SET_TAC[]);
 (ONCE_REWRITE_TAC[AFF_DIM_INSERT]);
 (COND_CASES_TAC);

 (NEW_GOAL `CARD {u0,u2,u3:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (NEW_GOAL `aff_dim {u0, u2, u3} <= &(CARD{u0,u2,u3:real^3}) - &1`);
 (MATCH_MP_TAC AFF_DIM_LE_CARD);
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `u1 IN affine hull {u0,u2,u3:real^3}`);
 (UNDISCH_TAC `u1 IN convex hull {u0, u2, u3:real^3}`);
 (MATCH_MP_TAC (SET_RULE `(b SUBSET c) ==> ((a IN b) ==> (a IN c))`));
 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

(* Case v = u2 *)
 (ASM_CASES_TAC `v = u2:real^3`);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "S");
 (REWRITE_WITH `{u0, u1, u2, u3} = {u2, u0, u1, u3:real^3}`);
 (SET_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 (NEW_GOAL `aff_dim {u2, u0, u1, u3:real^3} = &3`);
 (REWRITE_WITH `{u2, u0, u1, u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (EXPAND_TAC "S" THEN SET_TAC[]);
 (MATCH_MP_TAC Rogers.MHFTTZN1);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `aff_dim {u2, u0, u1, u3:real^3} <= &3 - &1`);
 (REWRITE_WITH `{u2, u0, u1, u3:real^3} = u2 INSERT {u0,u1,u3:real^3}`);
 (SET_TAC[]);
 (ONCE_REWRITE_TAC[AFF_DIM_INSERT]);
 (COND_CASES_TAC);
 (NEW_GOAL `CARD {u0,u1,u3:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (NEW_GOAL `aff_dim {u0,u1,u3:real^3} <= &(CARD {u0,u1,u3:real^3}) - &1`);
 (MATCH_MP_TAC AFF_DIM_LE_CARD);
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `u2 IN affine hull {u0,u1,u3:real^3}`);
 (UNDISCH_TAC `u2 IN convex hull {u0,u1,u3:real^3}`);
 (MATCH_MP_TAC (SET_RULE `(b SUBSET c) ==> ((a IN b) ==> (a IN c))`));
 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

(* Case v = u2 *)
 (ASM_CASES_TAC `v = u3:real^3`);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "S");
 (REWRITE_WITH `{u0, u1, u2, u3} = {u3, u0, u1, u2:real^3}`);
 (SET_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 (NEW_GOAL `aff_dim {u3, u0, u1, u2:real^3} = &3`);
 (REWRITE_WITH `{u3, u0, u1, u2:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (EXPAND_TAC "S" THEN SET_TAC[]);
 (MATCH_MP_TAC Rogers.MHFTTZN1);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `aff_dim {u3, u0, u1, u2:real^3} <= &3 - &1`);
 (ONCE_REWRITE_TAC[AFF_DIM_INSERT]);
 (COND_CASES_TAC);
 (NEW_GOAL `CARD {u0,u1,u2:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (NEW_GOAL `aff_dim {u0,u1,u2:real^3} <= &(CARD {u0,u1,u2:real^3}) - &1`);
 (MATCH_MP_TAC AFF_DIM_LE_CARD);
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `u3 IN affine hull {u0,u1,u2:real^3}`);
 (UNDISCH_TAC `u3 IN convex hull {u0,u1,u2:real^3}`);
 (MATCH_MP_TAC (SET_RULE `(b SUBSET c) ==> ((a IN b) ==> (a IN c))`));
 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);
 (STRIP_TAC);
 (NEW_GOAL `v:real^3 IN {}`);
 (ASM_REWRITE_TAC[IN]);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN REWRITE_TAC[NOT_IN_EMPTY]);
 (ASM_MESON_TAC[]);

(* ======================================================================= *)
(* ====Case 4:  k = 3 ====== *) 

 (ASM_CASES_TAC `k = 3`);
 (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell3]);
 (COND_CASES_TAC);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
 (NEW_GOAL 
 `V INTER mcell k V ul = set_of_list (truncate_simplex (k - 1) ul)`);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 4`]);
 (STRIP_TAC);
 (NEW_GOAL `v IN mcell 3 V ul`);
 (ASM_SET_TAC[]);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ARITH_RULE `3 - 1 = 2`]);
 (STRIP_TAC);

 (NEW_GOAL `v IN {u0, u1, u2:real^3}`);
 (ASM_SET_TAC[]);
 (ABBREV_TAC `m = mxi V [u0;u1;u2;u3:real^3]`);
 (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
 (NEW_GOAL `aff_dim {u0, u1, u2:real^3} = &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.MHFTTZN1);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `~(m IN affine hull {u0,u1,u2:real^3})`);
 (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3] 2`);
 (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3] 3`);

 (NEW_GOAL `s2 IN voronoi_list V [u0;u1;u2:real^3]`);
 (EXPAND_TAC "s2");
 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]);
 (ASM_REWRITE_TAC[ARITH_RULE `SUC 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
 (UNDISCH_TAC `barV V 3 ul` THEN REWRITE_TAC[BARV]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `voronoi_nondg V ([u0;u1;u2:real^3])`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (REWRITE_TAC[Sphere.INITIAL_SUBLIST; LENGTH; ARITH_RULE `0 < SUC (SUC (SUC 0))`]);
 (EXISTS_TAC `[u3:real^3]` THEN ASM_REWRITE_TAC[APPEND]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[VORONOI_NONDG; LENGTH; 
   ARITH_RULE `SUC (SUC (SUC 0)) = 3`; AFF_DIM_EMPTY]);
 (REWRITE_TAC[ARITH_RULE `-- &1 + &3:int = &3 - &1`]);  
 (REWRITE_TAC[MESON[INT_OF_NUM_SUB; ARITH_RULE `1 <= 3`] `&3:int - &1 = &(3 - 1)`]);
 (REWRITE_TAC[ARITH_RULE `3 - 1= 2 /\ ~(&2:int = &4)`]);


 (NEW_GOAL `s3 IN voronoi_list V [u0;u1;u2:real^3]`);
 (EXPAND_TAC "s3");
 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]);
 (ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);   
 (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
 (EXISTS_TAC `voronoi_list V [u0; u1; u2; u3:real^3]`);
 (STRIP_TAC);
 (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
 (UNDISCH_TAC `barV V 3 ul` THEN REWRITE_TAC[BARV]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `voronoi_nondg V ([u0;u1;u2;u3:real^3])`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (REWRITE_TAC[Sphere.INITIAL_SUBLIST; LENGTH; ARITH_RULE `0 < SUC (SUC (SUC (SUC 0)))`]);
 (EXISTS_TAC `[]:(real^3)list` THEN ASM_REWRITE_TAC[APPEND]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[VORONOI_NONDG; LENGTH; 
   ARITH_RULE `SUC(SUC (SUC (SUC 0))) = 4`; AFF_DIM_EMPTY]);
 (REWRITE_TAC[ARITH_RULE `-- &1 + &4:int = &4 - &1`]);
 (REWRITE_TAC[MESON[INT_OF_NUM_SUB; ARITH_RULE `1 <= 4`] `&4:int - &1 = &(4 - 1)`]);
 (REWRITE_TAC[ARITH_RULE `4 - 1= 3 /\ ~(&3:int = &4)`]);
 (REWRITE_TAC[VORONOI_LIST; set_of_list; VORONOI_SET]);
 (SET_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[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 [u0; u1; u2; u3]`);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (ASM_REWRITE_TAC[]);

 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC);
 (NEW_GOAL `convex hull {s2,s3:real^3} SUBSET voronoi_list V [u0; u1; u2]`);
 (REWRITE_WITH `convex hull {s2, s3} SUBSET voronoi_list V [u0; u1; u2:real^3]    <=> convex hull {s2, s3} SUBSET convex hull (voronoi_list V [u0; u1; u2])`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_WITH `convex hull (voronoi_list V [u0; u1; u2]) = voronoi_list V [u0; u1; u2:real^3]`);
 (REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (NEW_GOAL `s IN voronoi_list V [u0;u1;u2:real^3]`);
 (UNDISCH_TAC `between s (s2, s3:real^3)`);
 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
 (ASM_SET_TAC[]);

 (NEW_GOAL `s2 = circumcenter (set_of_list [u0;u1;u2:real^3])`);
 (REWRITE_TAC[set_of_list]);
 (EXPAND_TAC "s2");
 (MATCH_MP_TAC OMEGA_LIST_2_EXPLICIT_NEW);
 (EXISTS_TAC `u3:(real^3)` THEN ASM_REWRITE_TAC[]);
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`); IN]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 [u0; u1; u2; u3]`);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (ASM_REWRITE_TAC[]);

 (STRIP_TAC);
 (NEW_GOAL `(m - s2:real^3) dot (m - s2) = &0`);
 (REWRITE_TAC[ASSUME `s2 = circumcenter (set_of_list [u0; u1; u2:real^3])`]);
 (MATCH_MP_TAC Rogers.MHFTTZN4);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
 (REWRITE_TAC[set_of_list]);
 (ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
 (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (UP_ASM_TAC THEN REWRITE_TAC[DOT_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
 (STRIP_TAC);
 (NEW_GOAL `hl (truncate_simplex 2 [u0;u1;u2;u3]) = dist (s, u0:real^3)`);
 (REWRITE_WITH `s = s2:real^3`);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[ASSUME `s2 = circumcenter (set_of_list [u0; u1; u2:real^3])`]);
 (REWRITE_WITH `dist (circumcenter (set_of_list [u0; u1; u2]),u0) = dist 
  (circumcenter (set_of_list [u0; u1; u2]),HD [u0; u1; u2:real^3])`);
 (REWRITE_TAC[HD]);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (UP_ASM_TAC THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[DIST_SYM]);
 (ASM_REAL_ARITH_TAC);


 (ASM_CASES_TAC `v = u0:real^3`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 (MATCH_MP_TAC FUN_AFFINE_KLEMMA);
 (ASM_SET_TAC[]);

 (ASM_CASES_TAC `v = u1:real^3`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0, u1, u2, m:real^3} = {u1, u0, u2, m}`);
 (SET_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 (MATCH_MP_TAC FUN_AFFINE_KLEMMA);
 (REWRITE_WITH `{u1, u0, u2} = {u0, u1, u2:real^3}`);
 (SET_TAC[]);
 (ASM_SET_TAC[]);

 (ASM_CASES_TAC `v = u2:real^3`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0, u1, u2, m:real^3} = {u2, u0, u1, m}`);
 (SET_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 (MATCH_MP_TAC FUN_AFFINE_KLEMMA);
 (REWRITE_WITH `{u2, u0, u1} = {u0, u1, u2:real^3}`);
 (SET_TAC[]);
 (ASM_SET_TAC[]);

 (NEW_GOAL `F`);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[EVENTUALLY_RADIAL_EMPTY]);

(* ======================================================================= *)
(* ====Case 5:  k = 2 ====== *) 

 (ASM_CASES_TAC `k = 2`);
 (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell2]);
 (COND_CASES_TAC);
 (LET_TAC);
 (REWRITE_TAC[HD;TL]);
 (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3] 3`);
 (ABBREV_TAC `m = mxi V [u0; u1; u2; u3]`);

 (NEW_GOAL 
 `V INTER mcell k V ul = set_of_list (truncate_simplex (k - 1) ul)`);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2 /\ 2 <= 4`]);
 (STRIP_TAC);
 (NEW_GOAL `v IN mcell 3 V ul`);
 (ASM_SET_TAC[]);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ARITH_RULE `2 - 1 = 1`]);
 (STRIP_TAC);

 (NEW_GOAL `v IN {u0, u1:real^3}`);
 (ASM_SET_TAC[]);
 (NEW_GOAL `~(u0 = u1:real^3)`);
 (STRIP_TAC);
 (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} = 4`);
 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (REWRITE_WITH `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` THEN ASM_REWRITE_TAC[]);
 (ARITH_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{a,a,b,c} = {a,b,c}`]);
 (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (ASM_ARITH_TAC);



 (NEW_GOAL `hl [u0;u1:real^3] = inv(&2) * dist (u1,u0)`);
 (REWRITE_WITH `hl [u0;u1:real^3] = 
   dist (circumcenter (set_of_list [u0;u1]),HD [u0;u1])`);
 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 (REWRITE_TAC[set_of_list; Rogers.CIRCUMCENTER_2; midpoint; HD; dist]);
 (NORM_ARITH_TAC);

 (NEW_GOAL `&0 < a /\ a < &1`);
 (EXPAND_TAC "a");
 (REWRITE_TAC[]);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LT_DIV);
 (SIMP_TAC[SQRT_POS_LT; ARITH_RULE `&0 < &2`]);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (ASM_SIMP_TAC[REAL_LT_INV; ARITH_RULE `&0 < &2`]);
 (MATCH_MP_TAC DIST_POS_LT THEN ASM_MESON_TAC[]);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (REWRITE_WITH `hl [u0; u1:real^3] / sqrt (&2) < &1 <=> 
                 hl [u0; u1] < &1 * sqrt (&2)`);
 (MATCH_MP_TAC REAL_LT_LDIV_EQ);
 (SIMP_TAC[SQRT_POS_LT; ARITH_RULE `&0 < &2`]);
 (REWRITE_TAC[REAL_MUL_LID]);
 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 [u0; u1; u2; u3]`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC EVENTUALLY_RADIAL_INTER);
 (STRIP_TAC);
 (ASM_CASES_TAC `v = u0:real^3`);
 (ASM_REWRITE_TAC[EVENTUALLY_RADIAL_RCONE_GE_ABC_A]);
 (ASM_CASES_TAC `v = u1:real^3`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_RCONE_GE_ABC_B);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);

 (MATCH_MP_TAC EVENTUALLY_RADIAL_INTER);
 (STRIP_TAC);
 (ASM_CASES_TAC `v = u1:real^3`);
 (ASM_REWRITE_TAC[EVENTUALLY_RADIAL_RCONE_GE_ABC_A]);
 (ASM_CASES_TAC `v = u0:real^3`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_RCONE_GE_ABC_B);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);

(* ========================================================================== *)
 (NEW_GOAL `DISJOINT {u0, u1:real^3} {m, s3}`);
(* ========================================================================== *)

 (ABBREV_TAC `s2 = omega_list_n V ul 2`);
 (NEW_GOAL `s2 IN voronoi_list V [u0;u1]`);
 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (EXPAND_TAC "s2");
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3`);
 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2 /\ 2 <= 3`]);

 (NEW_GOAL `s3 IN voronoi_list V [u0;u1]`);
 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (EXPAND_TAC "s3");
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 (EXISTS_TAC `3`);
 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 3`]);
 (NEW_GOAL `m IN voronoi_list V [u0; u1]`);
 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) < sqrt (&2)`);
 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
                  dist (u0,s) = sqrt (&2) /\
                  m = s`);
 (EXPAND_TAC "m");
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
 (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 STRIP_TAC);


 (NEW_GOAL `convex hull {s2,s3:real^3} SUBSET voronoi_list V [u0; u1]`);
 (REWRITE_WITH `convex hull {s2, s3} SUBSET voronoi_list V [u0; u1:real^3]    <=> convex hull {s2, s3} SUBSET convex hull (voronoi_list V [u0; u1])`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_WITH `convex hull (voronoi_list V [u0; u1]) = voronoi_list V [u0; u1:real^3]`);
 (REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (ASM_SET_TAC[]);

 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `between s (s2, s3:real^3)`);
 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
 (ASM_SET_TAC[]);

 (EXPAND_TAC "m" THEN REWRITE_TAC[mxi]);
 (COND_CASES_TAC);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `~(m IN {u0,u1:real^3})`);
 (REWRITE_TAC[SET_RULE `a IN {b,c} <=> a = b \/ a = c`] THEN STRIP_TAC);
 (NEW_GOAL `m:real^3 IN voronoi_closed V u1`);
 (UNDISCH_TAC `m IN voronoi_list V [u0; u1]` THEN REWRITE_TAC[VORONOI_LIST; 
   VORONOI_SET; set_of_list]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL; REAL_ARITH `~(a <= b) <=> b < a`]);
 (ASM_SIMP_TAC[DIST_POS_LT]);

 (NEW_GOAL `m:real^3 IN voronoi_closed V u0`);
 (UNDISCH_TAC `m IN voronoi_list V [u0; u1]` THEN REWRITE_TAC[VORONOI_LIST; 
   VORONOI_SET; set_of_list]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL; REAL_ARITH `~(a <= b) <=> b < a`]);
 (ASM_SIMP_TAC[DIST_POS_LT]);

 (NEW_GOAL `~(s3 IN {u0, u1:real^3})`);
 (REWRITE_TAC[SET_RULE `a IN {b,c} <=> a = b \/ a = c`] THEN STRIP_TAC);
 (NEW_GOAL `s3:real^3 IN voronoi_closed V u1`);
 (UNDISCH_TAC `s3 IN voronoi_list V [u0; u1]` THEN REWRITE_TAC[VORONOI_LIST; 
   VORONOI_SET; set_of_list]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL; REAL_ARITH `~(a <= b) <=> b < a`]);
 (ASM_SIMP_TAC[DIST_POS_LT]);

 (NEW_GOAL `s3:real^3 IN voronoi_closed V u0`);
 (UNDISCH_TAC `s3 IN voronoi_list V [u0; u1]` THEN REWRITE_TAC[VORONOI_LIST; 
   VORONOI_SET; set_of_list]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL; REAL_ARITH `~(a <= b) <=> b < a`]);
 (ASM_SIMP_TAC[DIST_POS_LT]);

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

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

 (ASM_CASES_TAC `v = u0:real^3`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_AFF_GE);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `v = u1:real^3`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `{u0,u1:real^3} = {u1,u0}`);
 (SET_TAC[]);
 (MATCH_MP_TAC EVENTUALLY_RADIAL_AFF_GE);
 (REWRITE_WITH `{u1,u0:real^3} = {u0,u1}`);
 (SET_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `F`);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[EVENTUALLY_RADIAL_EMPTY]);

 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[])]);;


end;;