(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Packing                                                           *)
(* Lemma: OXLZLEZ                                                             *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-12-21                                                           *)
(* ========================================================================== *)

(* Leaf and Cell Lemmas *)

module Leaf_cell = struct

  open Hales_tactic;;
  open Bump;;

let leaf = new_definition `leaf V ul <=> ul IN barV V 2 /\ hl ul < sqrt2`;;
let stem = new_definition `stem (ul:(A)list) = set_of_list (truncate_simplex 1 ul)`;;
(* START WITH GENERIC LEMMAS *)

let coplanar_eq_coplanar_alt = 
prove(
  `!s:real^N->bool. 2 <= dimindex(:N) ==> (coplanar s <=> coplanar_alt s)`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[COPLANAR; Collect_geom.coplanar_alt]);;
let RE_EQVL_IMP_SYM = 
prove_by_refinement(
  `!a b. re_eqvl a b ==> re_eqvl b a`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Trigonometry2.re_eqvl];
  REPEAT WEAK_STRIP_TAC;
  EXISTS_TAC(`inv t`);
  GMATCH_SIMP_TAC REAL_LT_INV;
  ASM_REWRITE_TAC[];
  Calc_derivative.CALC_ID_TAC;
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let RE_EQVL_SYM = 
prove_by_refinement(
  `!a b. re_eqvl a b <=> re_eqvl b a`,

  (* {{{ proof *)
  [
  MESON_TAC[RE_EQVL_IMP_SYM]
  ]);;
  (* }}} *)

let RE_EQVL_SCALE1 = 
prove_by_refinement(
  `!a b t. &0 < t ==> (re_eqvl (t * a) b <=> re_eqvl a b)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Trigonometry2.re_eqvl];
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[TAUT `(a <=> b) <=> ((a ==> b) /\ (b ==> a))`];
  CONJ_TAC;
    REPEAT WEAK_STRIP_TAC;
    EXISTS_TAC `t' / t`;
    GMATCH_SIMP_TAC REAL_LT_DIV;
    ASM_REWRITE_TAC[];
    Calc_derivative.CALC_ID_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  REPEAT WEAK_STRIP_TAC;
  EXISTS_TAC `t' * t`;
  GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
  ASM_REWRITE_TAC[];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let RE_EQVL_SCALE2 = 
prove_by_refinement(
  `!a b t. &0 < t ==> (re_eqvl a (t* b) <=> re_eqvl a b)`,

  (* {{{ proof *)
  [
  MESON_TAC[RE_EQVL_SCALE1;RE_EQVL_SYM]
  ]);;
  (* }}} *)

let RE_EQVL_REFL = 
prove_by_refinement(
  `!a . re_eqvl a a`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Trigonometry2.re_eqvl];
  GEN_TAC;
  EXISTS_TAC `&1`;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let WEDGE_GE_NULL = 
prove_by_refinement(
  `!u0 u1 v1 v2. ~collinear {u0,u1,v1} /\ ~collinear {u0,u1,v2} /\ azim u0 u1 v1 v2 = &0 ==>
     wedge_ge u0 u1 v1 v2 = aff_ge {u0,u1} {v1}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[EXTENSION];
  GEN_TAC;
  GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
  REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE];
  ASM_REWRITE_TAC[];
  INTRO_TAC Local_lemmas.AZIM_RANGE [`u0`;`u1`;`v1`;`x`];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let X_IN_AFF_GE_LEFT = 
prove_by_refinement(
  `!(x:real^A) S U. (x IN S DIFF U) ==> (x IN aff_ge S U)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `aff_ge S U = aff_ge (S DIFF U) U`) SUBST1_TAC));
    REWRITE_TAC[Sphere.aff_ge_def];
    BY(MESON_TAC[ AFFSIGN_DISJOINT_DIFF]);
  MATCH_MP_TAC Packing3.IN_TRANS;
  GOAL_TERM (fun w -> (EXISTS_TAC ( env w`aff_ge (S DIFF U) {}`)));
  CONJ2_TAC;
    MATCH_MP_TAC AFF_GE_MONO_RIGHT;
    BY(SET_TAC[]);
  REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL];
  MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let WEDGE_WEDGE_GE = 
prove_by_refinement(
  `!u0 u1 v1 v2. ~collinear {u0,u1,v1} /\ ~collinear {u0,u1,v2}  ==>
    wedge_ge u0 u1 v1 v2 SUBSET wedge u0 u1 v1 v2 UNION aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[SUBSET];
  REWRITE_TAC[IN_UNION];
  REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE];
  REPEAT WEAK_STRIP_TAC;
  GOAL_TERM (fun w -> (ASM_CASES_TAC ( env w `x IN affine hull {u0,u1}`)));
    INTRO_TAC AFFINE_HULL_SUBSET_AFF_GE [`{u0,u1}`;`{v1}`];
    REWRITE_TAC[SUBSET];
    ANTS_TAC;
      REWRITE_TAC[DISJOINT];
      REWRITE_TAC[Collect_geom2.INTER_DISJONT_EX];
      REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
      GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `{u0,u1,v1}  = {v1,u0,u1}`) ASSUME_TAC));
        BY(SET_TAC[]);
      BY(ASM_MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
    BY(ASM_MESON_TAC[]);
  GMATCH_SIMP_TAC WEDGE_ALT;
  REWRITE_TAC[IN_ELIM_THM];
  ASM_REWRITE_TAC[];
  SUBCONJ_TAC;
    BY(ASM_MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
  DISCH_TAC;
  GOAL_TERM (fun w -> (ENOUGH_TO_SHOW_TAC ( env w `(azim u0 u1 v1 x = &0 ==> x IN aff_ge {u0,u1} {v1}) /\ (azim u0 u1 v1 x = azim u0 u1 v1 v2 ==> x IN aff_ge {u0,u1} {v2})`)));
    INTRO_TAC Local_lemmas.AZIM_RANGE [`u0`;`u1`;`v1`;`x`];
    FIRST_X_ASSUM_ST `azim` MP_TAC;
    BY(MESON_TAC[arith `x <= y ==> x = y \/ x < y`]);
  GMATCH_SIMP_TAC (Local_lemmas.AZIM_EQ_0_GE_ALT2);
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
  ASM_REWRITE_TAC[];
  ONCE_REWRITE_TAC[arith `x = azim a b c d <=> azim a b c d = x`];
  GMATCH_SIMP_TAC AZIM_EQ;
  GMATCH_SIMP_TAC Local_lemmas.AZIM_EQ_0_GE_ALT2;
  ASM_REWRITE_TAC[];
  INTRO_TAC AFF_GT_SUBSET_AFF_GE [`{u0,u1}`;`{v2}`];
  REWRITE_TAC[SUBSET];
  DISCH_THEN (unlist REWRITE_TAC);
  GMATCH_SIMP_TAC COLLINEAR_3_AFFINE_HULL;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let WEDGE_GE_ALMOST_DISJOINT = 
prove_by_refinement(
  `!u0 u1 v1 v2.  ~collinear {u0,u1,v1} /\ ~collinear {u0,u1,v2}  ==>
    wedge_ge u0 u1 v1 v2 INTER wedge_ge u0 u1 v2 v1 SUBSET aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}
     `,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ASM_CASES_TAC `azim u0 u1 v1 v2 = &0`;
    MATCH_MP_TAC SUBSET_TRANS;
    GOAL_TERM (fun w -> (EXISTS_TAC ( env w `wedge_ge u0 u1 v1 v2`)));
    CONJ_TAC;
      BY(SET_TAC[]);
    GMATCH_SIMP_TAC WEDGE_GE_NULL;
    ASM_REWRITE_TAC[];
    BY(SET_TAC[]);
  SUBGOAL_THEN `&0 < azim u0 u1 v1 v2` ASSUME_TAC;
    MATCH_MP_TAC (arith `~(x = &0) /\ (&0 <= x) ==> (&0 < x)`);
    BY(ASM_REWRITE_TAC[Local_lemmas.AZIM_RANGE;]);
  INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v1`;`v2`];
  INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v2`;`v1`];
  ASM_REWRITE_TAC[];
  GOAL_TERM (fun w -> (ENOUGH_TO_SHOW_TAC ( env w `wedge u0 u1 v1 v2 INTER wedge u0 u1 v2 v1 = {}`)));
    BY(SET_TAC[]);
  INTRO_TAC Counting_spheres.WEDGE_ORDER_DISJOINT [`u0`;`u1`;`v1`;`2`;`\ i. if (i=2) then v2 else v1`];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `~(2 + 1 = 2) /\ ~(1 = 2)`];
  REWRITE_TAC[IN_NUMSEG];
  REWRITE_TAC[arith `!i. (1 <= i /\ i <= 2) <=> (i = 1 \/ i = 2)`];
  ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAK_STRIP_TAC;
        FIRST_X_ASSUM MP_TAC;
        BY(ASM_REWRITE_TAC[arith `~(1=2)`]);
      FIRST_X_ASSUM MP_TAC;
      BY(ASM_REWRITE_TAC[]);
    REWRITE_TAC[arith `! j k. ((j = 1 \/ j = 2) /\ (k = 1 \/ k = 2) /\ j < k) <=> (j=1 /\ k=2)`];
    REPEAT WEAK_STRIP_TAC;
    ASM_REWRITE_TAC[arith `~(1=2)`];
    BY(ASM_REWRITE_TAC[AZIM_REFL]);
  DISCH_THEN (C INTRO_TAC [`1`;`2`]);
  BY(REWRITE_TAC[arith `~(1=2) /\ (1 + 1 = 2) /\ ~(2 + 1 = 2)`])
  ]);;
  (* }}} *)

let AFF_DIM_3 = 
prove_by_refinement(
  `!a (b:real^A) c. aff_dim {a,b,c} <= &2`,

  (* {{{ proof *)
  [
  ONCE_REWRITE_TAC[AFF_DIM_INSERT];
  REWRITE_TAC[AFF_DIM_2];
  REPEAT WEAK_STRIP_TAC;
  BY(REPEAT COND_CASES_TAC THEN INT_ARITH_TAC)
  ]);;
  (* }}} *)

let COPLANAR_IMP_AFF_DIM = 
prove_by_refinement(
  `!(s:real^A->bool). coplanar s ==> aff_dim s <= &2`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Trigonometry2.coplanar];
  REPEAT WEAK_STRIP_TAC;
  MATCH_MP_TAC INT_LE_TRANS;
  TYPIFY `aff_dim (affine hull {u,v,w})` EXISTS_TAC;
  CONJ_TAC;
    MATCH_MP_TAC AFF_DIM_SUBSET;
    BY(ASM_REWRITE_TAC[]);
  REWRITE_TAC[AFF_DIM_AFFINE_HULL];
  ONCE_REWRITE_TAC[AFF_DIM_INSERT];
  REWRITE_TAC[AFF_DIM_2];
  BY(REPEAT COND_CASES_TAC THEN INT_ARITH_TAC)
  ]);;
  (* }}} *)

let COPLANAR_INSERT = 
prove_by_refinement(
  `!s (p:real^A). aff_dim s = &2 /\ coplanar (p INSERT s) ==> p IN affine hull s`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP COPLANAR_IMP_AFF_DIM));
  FIRST_X_ASSUM_ST `INSERT` MP_TAC;
  REWRITE_TAC[AFF_DIM_INSERT];
  ASM_REWRITE_TAC[];
  COND_CASES_TAC THEN REWRITE_TAC[];
  BY(INT_ARITH_TAC)
  ]);;
  (* }}} *)

let COPLANAR_UNION = 
prove_by_refinement(
  `!P Q (a:real^A) b.  ~(P = {}) /\ ~(Q = {}) /\
      (!p. p IN P ==> ~collinear {p,a,b}) /\
    (!q. q IN Q ==> ~collinear {q,a,b}) /\
    (! p q. p IN P /\ q IN Q ==> coplanar {p,q,a,b}) ==>
    coplanar (P UNION Q UNION {a,b})
      `,

  (* {{{ proof *)
  [
  REWRITE_TAC[GSYM MEMBER_NOT_EMPTY];
  REPEAT WEAK_STRIP_TAC;
  ABBREV_TAC `(E:real^A->bool) = affine hull {x,a,b}`;
  TYPIFY `aff_dim {x,a,b} = &2 /\ aff_dim {x',a,b} = &2` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC COLLINEAR_AFF_DIM [`{x,a,b}`];
    INTRO_TAC COLLINEAR_AFF_DIM [`{x',a,b}`];
    ASM_SIMP_TAC[];
    INTRO_TAC AFF_DIM_3 [`x`;`a`;`b`];
    INTRO_TAC AFF_DIM_3 [`x'`;`a`;`b`];
    BY(INT_ARITH_TAC);
  TYPIFY `Q SUBSET E` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[SUBSET];
    REPEAT WEAK_STRIP_TAC;
    EXPAND_TAC "E";
    MATCH_MP_TAC COPLANAR_INSERT;
    ASM_SIMP_TAC[];
    TYPIFY `{x'',x,a,b} = {x,x'',a,b}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(ASM_SIMP_TAC[]);
  TYPIFY `affine hull {x',a,b} = E` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "E";
    TYPIFY `affine hull {x,a,b} = affine hull (affine hull {x,a,b})` (C SUBGOAL_THEN SUBST1_TAC);
      BY(REWRITE_TAC[Planarity.AFFINE_HULL_AFFINE_EQ]);
    MATCH_MP_TAC AFF_DIM_EQ_AFFINE_HULL;
    CONJ_TAC;
      TYPIFY `x' IN affine hull {x,a,b} /\ {a,b} SUBSET affine hull {x,a,b}` ENOUGH_TO_SHOW_TAC;
        BY(SET_TAC[]);
      CONJ_TAC;
        BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
      MATCH_MP_TAC SUBSET_TRANS;
      TYPIFY `{x,a,b}` EXISTS_TAC;
      CONJ_TAC;
        BY(SET_TAC[]);
      BY(REWRITE_TAC[HULL_SUBSET]);
    ASM_REWRITE_TAC[AFF_DIM_AFFINE_HULL];
    BY(INT_ARITH_TAC);
  TYPIFY `P SUBSET E` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[SUBSET];
    REPEAT WEAK_STRIP_TAC;
    EXPAND_TAC "E";
    MATCH_MP_TAC COPLANAR_INSERT;
    BY(ASM_SIMP_TAC[]);
  REWRITE_TAC[coplanar];
  GEXISTL_TAC [`x'`;`a`;`b`];
  TYPIFY `P UNION Q SUBSET affine hull {x',a,b} /\ {a,b} SUBSET {x',a,b} /\ {x',a,b} SUBSET affine hull {x',a,b}` ENOUGH_TO_SHOW_TAC;
    BY(SET_TAC[]);
  CONJ_TAC;
    REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
    BY(SET_TAC[]);
  REWRITE_TAC[HULL_SUBSET];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let CONNECTED_SEGMENT_NOT_COVERED = 
prove_by_refinement(
  `!(A:real^A -> bool) B a b. (open) A /\ (open) B /\ a IN A /\ b IN B /\ (A INTER B = {}) ==>
    (?x. x IN segment [a,b] /\ ~(x IN A) /\ ~(x IN B)) `,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `(!x. x IN segment [a,b] ==> (x IN A) \/ (x IN B)) ==> F ` ENOUGH_TO_SHOW_TAC;
    BY(MESON_TAC[]);
  DISCH_TAC;
  INTRO_TAC (CONJUNCT1 CONNECTED_SEGMENT) [`a`;`b`];
  REWRITE_TAC[connected];
  GEXISTL_TAC [`A`;`B`];
  ASM_REWRITE_TAC[];
  CONJ_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
  CONJ_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  INTRO_TAC ENDS_IN_SEGMENT [`a`;`b`];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
  ]);;
  (* }}} *)

(* END OF GENERIC LEMMAS *)

let GBEWYFX = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul ==> 
   ~(collinear (set_of_list ul)) `,

  (* {{{ proof *)
  [
  REWRITE_TAC[leaf;IN;COLLINEAR_AFF_DIM];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Rogers.MHFTTZN1 [`V`;`ul`;`2`];
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM MP_TAC;
  BY(INT_ARITH_TAC)
  ]);;
  (* }}} *)

let NWVRFMF = 
prove_by_refinement(
  `!V ul p.  packing V /\ saturated V /\ leaf V ul /\ {p} facet_of (voronoi_list V ul) ==>
  (?vl. vl IN barV V 3 /\ truncate_simplex 2 vl = ul /\ omega_list V vl = p)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[leaf;IN];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Rogers.IDBEZAL [`V`;`ul`;`2`;`{p}`];
  ASM_REWRITE_TAC[arith `2 < 3`;arith `2 + 1 = 3`];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `vl` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  INTRO_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST [`V`;`vl`;`3`];
  ASM_REWRITE_TAC[];
  BY(ASM_MESON_TAC[IN_SING])
  ]);;
  (* }}} *)

let YBZFUPO = 
prove_by_refinement(
  `!V ul.  packing V /\ saturated V /\ leaf V ul ==>
   (?p1 p2.  voronoi_list V ul = convex hull {p1,p2} /\ ~(p1 = p2) /\
      (!f. f facet_of voronoi_list V ul <=> f IN {{p1},{p2}}))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[leaf;IN];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Packing3.AFF_DIM_VORONOI_LIST [`V`;`ul`;`2`];
  ASM_REWRITE_TAC[arith `&3 - int_of_num 2 = &1`];
  DISCH_TAC;
  INTRO_TAC Polyhedron.EXPAND_EDGE_POLYTOPE [`voronoi_list V ul`;`voronoi_list V ul`];
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC FACE_OF_REFL;
  REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST];
  GMATCH_SIMP_TAC Packing3.POLYTOPE_VORONOI_LIST_BARV;
  CONJ_TAC;
    EXISTS_TAC `2`;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `a` EXISTS_TAC;
  TYPIFY `b` EXISTS_TAC;
  SUBCONJ_TAC;
    BY(REWRITE_TAC[SEGMENT_CONVEX_HULL]);
  DISCH_TAC;
  INTRO_TAC EXTREME_POINT_OF_SEGMENT [`a`;`b`;`a`];
  INTRO_TAC EXTREME_POINT_OF_SEGMENT [`a`;`b`;`b`];
  INTRO_TAC EXTREME_POINT_OF_SEGMENT [`a`;`b`];
  REWRITE_TAC[];
  REWRITE_TAC[GSYM FACE_OF_SING];
  REWRITE_TAC[facet_of];
  REPEAT WEAK_STRIP_TAC;
  SUBCONJ_TAC;
    DISCH_TAC;
    INTRO_TAC (CONJUNCT1 SEGMENT_EQ_SING) [`b`;`b`;`b`];
    REWRITE_TAC[];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `voronoi_list` MP_TAC;
    FIRST_X_ASSUM_ST `convex` kill;
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `1` MP_TAC;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[AFF_DIM_SING];
    BY(INT_ARITH_TAC);
  DISCH_TAC;
  GEN_TAC;
  TYPIFY `{{a},{b}} f <=> f IN {{a},{b}}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(MESON_TAC[IN]);
  REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
  TYPIFY `aff_dim(segment[a,b]) - &1 = &0` (C SUBGOAL_THEN SUBST1_TAC);
    BY(ASM_MESON_TAC[arith ` &1 - int_of_num 1 = &0`]);
  REWRITE_TAC[AFF_DIM_EQ_0];
  SUBGOAL_THEN `!(x:real^3). ~({x} = {})` ASSUME_TAC;
    BY(SET_TAC[]);
  REWRITE_TAC[TAUT `(b <=> a) <=> ((a ==> b) /\ (b ==> a))`];
  CONJ_TAC;
    BY(DISCH_THEN DISJ_CASES_TAC THEN ASM_MESON_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let PERMUTES_a_PERMUTES_b = 
prove_by_refinement(
  `!p a b. a <= b /\ p permutes 0..a ==> p permutes 0..b`,

  (* {{{ proof *)
  [
  REWRITE_TAC[permutes;IN_NUMSEG];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MATCH_MP_TAC;
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
  ]);;
  (* }}} *)

let PERMUTE_BARV3 = 
prove_by_refinement(
  `!V ul p.  packing V /\ saturated V /\  ul IN barV V 3 /\
    hl (truncate_simplex 2 ul) < sqrt2 /\ p permutes 0..1 ==>
   left_action_list p ul IN barV V 3`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `hl ul < sqrt2` ASM_CASES_TAC;
    MATCH_MP_TAC Rogers.YIFVQDV_1;
    ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
    MATCH_MP_TAC PERMUTES_a_PERMUTES_b;
    BY(ASM_MESON_TAC[arith `1 <= 3`]);
  INTRO_TAC Ynhyjit.YNHYJIT [`V`;`ul`;`3`;`p`;`left_action_list p ul`];
  ASM_SIMP_TAC[GSYM Sphere.sqrt2;arith `3 -1 = 2`];
  ASM_SIMP_TAC[arith `~(x < y) ==> y <= x`];
  ANTS_TAC;
    CONJ_TAC;
      BY(ASM_MESON_TAC[IN]);
    CONJ_TAC;
      BY(SET_TAC[]);
    MATCH_MP_TAC PERMUTES_a_PERMUTES_b;
    BY(ASM_MESON_TAC[arith `1 <= 2`]);
  BY(MESON_TAC[IN])
  ]);;
  (* }}} *)

let ZASUVOR = 
prove_by_refinement(
  `!V u0 u1 u2.  packing V /\ saturated V /\ leaf V [u0;u1;u2] ==>
   leaf V [u1;u0;u2] /\ (stem [u0;u1;u2] = stem [u1;u0;u2])`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC YBZFUPO [`V`;`[u0;u1;u2]`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC NWVRFMF [`V`;`[u0;u1;u2]`;`p1`];
  FIRST_X_ASSUM_ST `convex` kill;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[IN_INSERT];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC PERMUTES_SWAP [`0`;`1`;`0..1`];
  ANTS_TAC;
    REWRITE_TAC[IN_NUMSEG];
    BY(ARITH_TAC);
  DISCH_TAC;
  CONJ2_TAC;
    REWRITE_TAC[stem];
    REWRITE_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_1];
    REWRITE_TAC[set_of_list];
    BY(SET_TAC[]);
  SUBGOAL_THEN `left_action_list (swap(0,1)) vl IN barV V 3` ASSUME_TAC;
    MATCH_MP_TAC PERMUTE_BARV3;
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[leaf]);
  FIRST_X_ASSUM_ST `leaf` MP_TAC;
  REWRITE_TAC[leaf;IN];
  REWRITE_TAC[Pack_defs.HL;set_of_list];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `{u1,u0,u2} = {u0,u1,u2}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  ASM_REWRITE_TAC[];
  INTRO_TAC Packing3.TRUNCATE_SIMPLEX_BARV [`V`;`2`;`3`;`left_action_list (swap(0,1)) vl`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[IN;arith `2 <= 3`]);
  TYPIFY `truncate_simplex 2 (left_action_list (swap (0,1)) vl) = [u1;u0;u2]` ENOUGH_TO_SHOW_TAC;
    DISCH_THEN SUBST1_TAC;
    BY(MESON_TAC[]);
  TYPIFY `?w. left_action_list (swap (0,1)) vl = [u1;u0;u2;w]` ENOUGH_TO_SHOW_TAC;
    REPEAT WEAK_STRIP_TAC;
    ASM_REWRITE_TAC[];
    BY(REWRITE_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_2]);
  TYPIFY `EL 3 vl` EXISTS_TAC;
  REWRITE_TAC[Pack_defs.left_action_list];
  REWRITE_TAC[Packing3.LIST_EL_EQ];
  TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT (FIRST_X_ASSUM_ST `barV` MP_TAC);
    REWRITE_TAC[Sphere.BARV;IN];
    BY(MESON_TAC[arith `3 + 1 = 4`]);
  REWRITE_TAC[Packing3.LENGTH_TABLE];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[LENGTH];
  CONJ_TAC;
    BY(ARITH_TAC);
  GEN_TAC;
  SIMP_TAC[Packing3.EL_TABLE];
  REWRITE_TAC[INVERSE_SWAP];
  REWRITE_TAC[arith `j< 4 <=> (j = 0 \/ j = 1 \/ j = 2 \/ j = 3)`];
  INTRO_TAC (GSYM Packing3.EL_TRUNCATE_SIMPLEX) [`vl`;`2`];
  ASM_REWRITE_TAC[arith `2 + 1 <= 4`];
  BY(REPEAT WEAK_STRIP_TAC THEN ASM_SIMP_TAC[swap;EL;HD;arith `0 <= 2 /\ 1 <= 2 /\ 2 <= 2 /\ ~(1 = 0) /\ ~(2 = 1) /\ ~(2=0) /\ ~(3=0) /\ ~(3=1)`] THEN REWRITE_TAC[arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;EL;HD;TL])
  ]);;
  (* }}} *)

let NORM_FLATTEN = 
prove_by_refinement(
  `!u w (p:real^A). norm (u - p) pow 2 - norm (w - p) pow 2 = (u dot u) - (w dot w) + &2 % (w - u) dot p`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[NORM_POW_2];
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let truncate_set_of_list = 
prove_by_refinement(
  `!(vl:(A)list) k. 0 < k /\ LENGTH vl = (k+1) ==>
    set_of_list vl SUBSET set_of_list(truncate_simplex (k-1) vl) UNION {EL k vl}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[SUBSET];
  REWRITE_TAC[IN_SET_OF_LIST;IN_UNION;IN_SING];
  REWRITE_TAC[MEM_EXISTS_EL];
  REPEAT WEAK_STRIP_TAC;
  GMATCH_SIMP_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX;
  TYPIFY `k - 1 + 1 = k` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  CONJ_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  ASM_CASES_TAC `i = (k:num)`;
    BY(ASM_REWRITE_TAC[]);
  DISJ1_TAC;
  EXISTS_TAC `i:num`;
  GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX;
  ASM_REWRITE_TAC[];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
  ]);;
  (* }}} *)

let DIST_LE_HALF_PLANE = 
prove_by_refinement(
  `!x:real^A a:real^A b:real^A.
    dist(x,a) <= dist(x,b) <=> &0 <= (a - b) dot (&2 % x - (a + b))`,

[
  ABBREV_TAC ` an a b x = ((a:real^A) - b) dot (&2 % x - (a + b))`;
  REWRITE_TAC[dist; vector_norm];
  REWRITE_TAC[MESON[DOT_POS_LE; SQRT_MONO_LE_EQ]` sqrt ( x dot x) <= sqrt (y dot y) <=>   x dot x <= y dot y `];
  REWRITE_TAC[DOT_LSUB; DOT_RSUB];
  SIMP_TAC[DOT_SYM];
  ONCE_REWRITE_TAC[ GSYM REAL_SUB_LE];
  REWRITE_TAC[ REAL_ARITH ` x dot x -     b dot x -     (b dot x - b dot b) -     (x dot x - a dot x - (a dot x - a dot a)) =     &2 * (a dot x - b dot x) + b dot b - a dot a`];
  REWRITE_TAC[GSYM DOT_LSUB; GSYM DOT_RMUL];
  REPEAT GEN_TAC;
  TYPIFY `(a - b) dot &2 % x + b dot b - a dot a = (a - b) dot (&2 % x - (a + b))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  REWRITE_TAC[arith `x - &0 = x`];
  BY(ASM_MESON_TAC[])
]);;
let DIST_EQ_HALF_PLANE = 
prove_by_refinement(
  `!x:real^A a:real^A b:real^A.
    dist(x,a) = dist(x,b) <=> &0 = (a - b) dot (&2 % x - (a + b))`,

[
  ABBREV_TAC ` an a b x = ((a:real^A) - b) dot (&2 % x - (a + b))`;
  REWRITE_TAC[dist; vector_norm];
  REWRITE_TAC[MESON[DOT_POS_LE; SQRT_INJ]` sqrt ( x dot x) = sqrt (y dot y) <=>   x dot x = y dot y `];
  REPEAT GEN_TAC;
  ONCE_REWRITE_TAC[arith `x = y <=> y - x = &0`];
  TYPIFY `(x - b) dot (x - b) - (x - a) dot (x - a) =  ((a - b) dot (&2 % x - (a + b)))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  BY(ASM_MESON_TAC[arith `x - &0 = x`])
]);;
let FUZBZGI_0 = 
prove_by_refinement(
`!V ul p1 p2 t1 t2.  packing V /\ saturated V /\ leaf V ul /\
    (voronoi_list V ul = convex hull {p1, p2}) /\
   ~(p1 = p2) /\
      (circumcenter (set_of_list ul) = t1 % p1 + t2 % p2) /\
    (t1 + t2 = &1) /\
  (!f. f facet_of voronoi_list V ul <=> f IN {{p1}, {p2}}) ==>
    (&0 < t2)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  COMMENT "insert";
  TYPIFY `barV V 2 ul` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[leaf;IN]);
  COMMENT "end insert";
  COMMENT "borrowed_from   _1 lemma";
  INTRO_TAC NWVRFMF [`V`;`ul`;`p1`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(SET_TAC[]);
  WEAK_STRIP_TAC;
  ABBREV_TAC `q = t1 % p1 + t2 % (p2:real^3)`;
  INTRO_TAC Rogers.XYOFCGX [`V`;`set_of_list ul`;`q`];
  ASM_REWRITE_TAC[];
  TYPIFY `set_of_list ul SUBSET V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Packing3.BARV_SUBSET;leaf;IN]);
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    CONJ2_TAC;
      FIRST_X_ASSUM_ST `leaf` MP_TAC;
      REWRITE_TAC[leaf;Sphere.sqrt2;Pack_defs.HL];
      BY(MESON_TAC[]);
    MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT;
    BY(ASM_MESON_TAC[leaf;IN]);
  ONCE_REWRITE_TAC[DIST_SYM];
  REWRITE_TAC[arith `x > y <=> y < x`];
  REWRITE_TAC[Collect_geom.DIST_LT_HALF_PLANE];
  DISCH_THEN (C INTRO_TAC [`HD ul`;`EL 3 vl`]);
  REWRITE_TAC[IN_DIFF];
  TYPIFY `HD ul IN set_of_list ul` (C SUBGOAL_THEN (ASSUME_TAC));
    REWRITE_TAC[IN_SET_OF_LIST];
    REWRITE_TAC[MEM_EXISTS_EL];
    EXISTS_TAC `0`;
    REWRITE_TAC[EL];
    FIRST_X_ASSUM_ST `leaf` MP_TAC;
    REWRITE_TAC[leaf;Sphere.BARV;IN];
    BY(ARITH_TAC);
  TYPIFY `barV V 3 vl` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[IN]);
  TYPIFY `EL 3 vl IN V` (C SUBGOAL_THEN (ASSUME_TAC));
    INTRO_TAC Packing3.BARV_SUBSET [`V`;`3`;`vl`];
    ASM_REWRITE_TAC[];
    REWRITE_TAC[ IN_SET_OF_LIST ; SUBSET; MEM_EXISTS_EL];
    (FIRST_X_ASSUM_ST `barV V 3` MP_TAC);
    REWRITE_TAC[Sphere.BARV;IN];
    BY(MESON_TAC[arith `3 < 3 + 1`]);
  ASM_REWRITE_TAC[];
  COMMENT "back to 1";
  TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Sphere.BARV;arith `4 = 3 + 1`]);
  INTRO_TAC Rogers.MHFTTZN1 [`V`;`vl`;`3`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ANTS_TAC;
    DISCH_TAC;
    INTRO_TAC truncate_set_of_list [`vl`;`3`];
    ASM_SIMP_TAC[arith `0 < 3 /\ 3 + 1 = 4 /\ 3 - 1 = 2`];
    DISCH_TAC;
    INTRO_TAC AFF_DIM_SUBSET [`set_of_list vl`;`set_of_list ul`];
    ANTS_TAC;
      REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
      BY(SET_TAC[]);
    ASM_REWRITE_TAC[];
    TYPIFY `aff_dim (set_of_list ul) = &2` (C SUBGOAL_THEN SUBST1_TAC);
      MATCH_MP_TAC Rogers.MHFTTZN1;
      BY(ASM_MESON_TAC[leaf;IN]);
    BY(INT_ARITH_TAC);
  DISCH_TAC;
  COMMENT "back to 1'  do <=.";
  TYPIFY `voronoi_list V ul SUBSET voronoi_closed V (HD ul)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Packing3.VORONOI_LIST_SUBSET_VORONOI_CLOSED;
    FIRST_X_ASSUM_ST `leaf` MP_TAC;
    REWRITE_TAC[IN;leaf;Sphere.BARV];
    BY(ARITH_TAC);
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[Pack2.VORONOI_CLOSED;SUBSET];
  REWRITE_TAC[IN_ELIM_THM];
  REWRITE_TAC[DIST_LE_HALF_PLANE];
  DISCH_THEN (C INTRO_TAC [`p2`]);
  ASM_REWRITE_TAC[];
  (GMATCH_SIMP_TAC Marchal_cells_2_new.IN_SET_IMP_IN_CONVEX_HULL_SET);
  CONJ_TAC;
    BY(SET_TAC[]);
  GOAL_TERM (fun w -> (DISCH_THEN (MP_TAC o (ISPEC ( env w `EL 3 vl`)))));
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  COMMENT "back to 1a, do =.";
  INTRO_TAC Marchal_cells_2_new.VORONOI_LIST_3_SINGLETON_EXPLICIT [`V`;`vl`];
  ASM_REWRITE_TAC[];
  WEAK_STRIP_TAC;
  INTRO_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST [`V`;`vl`;`3`];
  ASM_REWRITE_TAC[IN_SING];
  DISCH_TAC;
  COMMENT "back to 1b";
  INTRO_TAC Rogers.HL_PROPERTIES [`V`;`vl`;`3`];
  ASM_REWRITE_TAC[];
  GOAL_TERM (fun w -> (DISCH_THEN (MP_TAC o (ISPEC ( env w `EL 3 vl`)))));
  REWRITE_TAC[IN_SET_OF_LIST];
  REWRITE_TAC[MEM_EXISTS_EL];
  ANTS_TAC;
    EXISTS_TAC `3`;
    BY(ASM_REWRITE_TAC[arith `3 < 4`]);
  TYPIFY `dist (HD vl,circumcenter (set_of_list vl)) = dist (circumcenter (set_of_list vl), HD vl)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(MESON_TAC[DIST_SYM]);
  REWRITE_TAC[DIST_EQ_HALF_PLANE];
  COMMENT "1c";
  TYPIFY `HD vl = HD ul` (C SUBGOAL_THEN SUBST1_TAC);
    EXPAND_TAC "ul";
    MATCH_MP_TAC (GSYM Packing3.HD_TRUNCATE_SIMPLEX);
    BY(ASM_REWRITE_TAC[arith `2 + 1 <= 4`]);
  ONCE_REWRITE_TAC[arith `&0 = x <=> &0 = -- x`];
  TYPIFY ` --((EL 3 vl - HD ul) dot (&2 % circumcenter (set_of_list vl) - (EL 3 vl + HD ul))) =  (( HD ul - EL 3 vl) dot     (&2 % p1 - (HD ul + EL 3 vl)))` (C SUBGOAL_THEN SUBST1_TAC);
    ASM_REWRITE_TAC[];
    BY(VECTOR_ARITH_TAC);
  DISCH_TAC;
  FIRST_X_ASSUM_ST `&0 < x` MP_TAC;
  EXPAND_TAC "q";
  ABBREV_TAC `(w:real^3) = HD ul - EL 3 vl`;
  TYPIFY `w dot (&2 % (t1 % p1 + t2 % p2) - (HD ul + EL 3 vl)) = t1 * (w dot (&2 % p1 - (HD ul + EL 3 vl))) + t2 * ( w dot (&2 % p2 - (HD ul + EL 3 vl)))` (C SUBGOAL_THEN SUBST1_TAC);
    FIRST_X_ASSUM_ST `x = &1` MP_TAC;
    REWRITE_TAC[arith `t1 + t2 = &1 <=> t2 = &1 - t1`];
    DISCH_THEN SUBST1_TAC;
    BY(VECTOR_ARITH_TAC);
  FIRST_X_ASSUM_ST `circumcenter` kill;
  FIRST_X_ASSUM_ST `&0` (SUBST1_TAC o GSYM);
  REWRITE_TAC[arith `t1 * &0 + x = x`];
  ASM_CASES_TAC `((w:real^3) dot (&2 % p2 - (HD ul + EL 3 vl))) = &0`;
    BY(ASM_MESON_TAC[arith `~(&0 < t * &0)`]);
  REWRITE_TAC[REAL_MUL_POS_LT];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let FUZBZGI_1 = 
prove_by_refinement(
  `!V ul.  packing V /\ saturated V /\ leaf V ul ==>
    ?p1 p2 t1 t2.
    (voronoi_list V ul = convex hull {p1, p2}) /\
    ~(p1 = p2) /\
      (circumcenter (set_of_list ul) = t1 % p1 + t2 % p2) /\
    (t1 + t2 = &1) /\
    (&0 < t1 /\ &0 < t2)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC YBZFUPO [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `p1` EXISTS_TAC;
  TYPIFY `p2` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `circumcenter (set_of_list ul) IN affine hull voronoi_list V ul` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC Rogers.MHFTTZN3 [`V`;`ul`;`2`];
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      BY(ASM_MESON_TAC[leaf;IN]);
    BY(SET_TAC[]);
  ASM_REWRITE_TAC[AFFINE_HULL_CONVEX_HULL;AFFINE_HULL_2];
  ABBREV_TAC `(q:real^3) = circumcenter (set_of_list ul)`;
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `u` EXISTS_TAC;
  TYPIFY `v` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
    MATCH_MP_TAC FUZBZGI_0;
    GOAL_TERM (fun w -> (GEXISTL_TAC ( envl w [`V`;`ul`;`p2`;`p1`;`v`])));
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      AP_TERM_TAC;
      BY(SET_TAC[]);
    CONJ_TAC;
      BY(VECTOR_ARITH_TAC);
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    TYPIFY `{{p1},{p2}} = {{p2},{p1}}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(REWRITE_TAC[]);
  MATCH_MP_TAC FUZBZGI_0;
  GOAL_TERM (fun w -> (GEXISTL_TAC ( envl w [`V`;`ul`;`p1`;`p2`;`u`])));
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let chi_msb = new_definition `chi_msb ul p = 
   ((EL 1 ul - EL 0 ul) cross (EL 2 ul - EL 0 ul)) dot (p - EL 0 ul)`;;
let chi_msb_swap_01 = 
prove_by_refinement(
  `!a b c d. chi_msb [a;b;c] d = -- chi_msb [b;a;c] d`,

  (* {{{ proof *)
  [
 REWRITE_TAC[chi_msb;EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`];
  REPEAT WEAK_STRIP_TAC;
  SUBGOAL_THEN `(d - a) = (d - b) + (b - (a:real^3))` SUBST1_TAC;
    BY(VECTOR_ARITH_TAC);
  SUBGOAL_THEN `(c - a) = (c - b) + (b - (a:real^3))` SUBST1_TAC;
    BY(VECTOR_ARITH_TAC);
  REWRITE_TAC[CROSS_RADD;DOT_RADD];
  REWRITE_TAC[DOT_LADD];
  REWRITE_TAC[CROSS_REFL];
  REWRITE_TAC[DOT_LZERO];
  REWRITE_TAC[arith `x + &0 = x`];
  SUBGOAL_THEN `((b - a) cross (c - b)) dot (b - a) = &0` SUBST1_TAC;
    BY(MESON_TAC[CROSS_TRIPLE;CROSS_REFL;DOT_LZERO]);
  REWRITE_TAC[arith `x + &0 = x`];
  REWRITE_TAC[GSYM DOT_LNEG];
  AP_THM_TAC;
  AP_TERM_TAC;
  REWRITE_TAC[GSYM CROSS_LNEG];
  AP_THM_TAC THEN AP_TERM_TAC;
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let chi_msb_swap_23 = 
prove_by_refinement(
  `!a b c d. chi_msb [a;b;c] d = -- chi_msb[a;b;d] c`,

  (* {{{ proof *)
  [
  REWRITE_TAC[chi_msb;EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`];
  REPEAT WEAK_STRIP_TAC;
  ONCE_REWRITE_TAC[CROSS_TRIPLE];
  REWRITE_TAC[GSYM DOT_LNEG];
  BY(REWRITE_TAC[GSYM CROSS_SKEW])
  ]);;
  (* }}} *)

let chi_msb_swap_12 = 
prove_by_refinement(
  `!a b c d. chi_msb [a;b;c] d = -- chi_msb [a;c;b] d`,

  (* {{{ proof *)
  [
  REWRITE_TAC[chi_msb;EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`];
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[GSYM DOT_LNEG];
  AP_THM_TAC;
  AP_TERM_TAC;
  BY(REWRITE_TAC[GSYM CROSS_SKEW])
  ]);;
  (* }}} *)

let chi_msb_additive_a = 
prove_by_refinement(
  `!a b c d t1 t2 t3 t4. (t1 + t2 + t3 + t4 = &1)  ==>
     (chi_msb [t1 % a + t2 % b + t3 % c + t4 % d;b;c] d) = t1 * (chi_msb [a;b;c] d)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ONCE_REWRITE_TAC[chi_msb_swap_01];
  REWRITE_TAC[chi_msb;EL;HD;TL;arith`2 = SUC 1 /\ 1 = SUC 0`];
  TYPIFY `(t1 % a + t2 % b + t3 % c + t4 % d) - b = t1 % (a - b) + t3 % (c - b) + t4 % (d - b)` (C SUBGOAL_THEN SUBST1_TAC);
    FIRST_X_ASSUM (SUBST1_TAC o (MATCH_MP (arith `t1 + t2 + t3 + t4 = &1 ==> t2 = &1 - t1 - t3 -t4`)));
    BY(VECTOR_ARITH_TAC);
  REWRITE_TAC[GSYM DOT_LNEG;GSYM CROSS_LNEG];
  REWRITE_TAC[GSYM DOT_LMUL];
  TYPIFY `--(t1 % (a - b) + t3 % (c - b) + t4 % (d - b)) = t1 % (--(a-b)) + (-- t3) % (c - b) + (-- t4) % (d - b)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  REWRITE_TAC[CROSS_LADD];
  REWRITE_TAC[DOT_LADD];
  REWRITE_TAC[CROSS_REFL;CROSS_LMUL];
  TYPIFY ` --t4 % ((d - b) cross (c - b)) dot (d - b) = &0` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[ DOT_LMUL];
    BY(MESON_TAC[CROSS_TRIPLE;CROSS_REFL;DOT_LZERO;arith `t * &0 = &0`]);
  REWRITE_TAC[DOT_LMUL;DOT_LZERO];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let chi_msb_additive_d = 
prove_by_refinement(
  `!a b c d t1 t2 t3 t4. (t1 + t2 + t3 + t4 = &1) ==>
    chi_msb [a;b;c] (t1 % a + t2 % b + t3 % c + t4 % d) = t4 * chi_msb [a;b;c] d`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ONCE_REWRITE_TAC[chi_msb_swap_23];
  ONCE_REWRITE_TAC[chi_msb_swap_12];
  REWRITE_TAC[arith `-- -- x = x`];
  ONCE_REWRITE_TAC[chi_msb_swap_01];
  SUBST1_TAC (varith `t1 % a + t2 % b + t3 % c + t4 % d = t4 % d + t1 % (a:real^3) + t2 % b + t3 % c`);
  REWRITE_TAC[arith `-- x = t * -- y <=> x = t * y`];
  MATCH_MP_TAC chi_msb_additive_a;
  BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let CHI_MSB_ADDITIVE = 
prove_by_refinement(
  `!ul t1 t2 p1 p2. (t1 + t2 = &1) ==> 
    chi_msb ul (t1 % p1 + t2 % p2) = t1 * chi_msb ul p1 + t2 * chi_msb ul p2`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[chi_msb];
  FIRST_X_ASSUM (SUBST1_TAC o (MATCH_MP (arith `t1 + t2 = &1 ==> t1 = &1 - t2`)));
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let CHI_MSB_CONVEX = 
prove_by_refinement(
  `!ul. convex { p | &0 <= chi_msb ul p }`,

  (* {{{ proof *)
  [
  GEN_TAC;
  REWRITE_TAC[ CONVEX_ALT];
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  GMATCH_SIMP_TAC CHI_MSB_ADDITIVE;
  CONJ_TAC;
    BY(REAL_ARITH_TAC);
  MATCH_MP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`);
  GMATCH_SIMP_TAC REAL_LE_MUL;
  GMATCH_SIMP_TAC REAL_LE_MUL;
  ASM_REWRITE_TAC[];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let CHI_MSB_INCLUDES_CONVEX_HULL = 
prove_by_refinement(
  `!S ul.  S SUBSET {p | &0 <= chi_msb ul p } ==> 
    convex hull S SUBSET {p | &0 <= chi_msb ul p}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM (MP_TAC o (MATCH_MP Marchal_cells.CONVEX_HULL_SUBSET));
  BY(MESON_TAC[CHI_MSB_CONVEX;CONVEX_HULL_EQ])
  ]);;
  (* }}} *)


let AFFINE_IMP_CHI_MSB_0 = 
prove_by_refinement(
  `!ul (p:real^3). LENGTH ul = 3 /\ p IN affine hull (set_of_list ul) ==> 
    chi_msb ul p = &0`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP set_of_list3));
  FIRST_X_ASSUM_ST `IN` MP_TAC;
  ASM_REWRITE_TAC[AFFINE_HULL_3];
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[chi_msb];
  FIRST_X_ASSUM_ST `&1` (unlist REWRITE_TAC o (MATCH_MP (arith `u + v + w = &1 ==> u = &1 - v - w`)));
  TYPIFY `((EL 1 ul - EL 0 ul) cross (EL 2 ul - EL 0 ul)) dot  (((&1 - v - w) % EL 0 ul + v % EL 1 ul + w % EL 2 ul) - EL 0 ul)  =  v * (((EL 1 ul - EL 0 ul) cross (EL 2 ul - EL 0 ul)) dot (EL 1 ul - EL 0 ul)) + w * (((EL 1 ul - EL 0 ul) cross (EL 2 ul - EL 0 ul)) dot (EL 2 ul - EL 0 ul))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  MATCH_MP_TAC (arith `a = &0 /\ b = &0 ==> v *a + w * b = &0`);
  CONJ_TAC;
    ONCE_REWRITE_TAC[Trigonometry1.cross_triple];
    ONCE_REWRITE_TAC[Trigonometry1.cross_triple];
    BY(REWRITE_TAC[CROSS_REFL;DOT_LZERO]);
  ONCE_REWRITE_TAC[Trigonometry1.cross_triple];
  BY(REWRITE_TAC[CROSS_REFL;DOT_LZERO])
  ]);;
  (* }}} *)

let CHI_MSB_IMP_COPLANAR = 
prove_by_refinement(
  `!ul p. chi_msb ul p = &0 ==> coplanar { EL 0 ul, EL 1 ul, EL 2 ul, p}`,

  (* {{{ proof *)
  [
  BY(REWRITE_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT;chi_msb])
  ]);;
  (* }}} *)

let CHI_MSB_COPLANAR = 
prove_by_refinement(
  `!a b c d. coplanar {a,b,c,d} <=> chi_msb [a;b;c] d = &0`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT];
  REWRITE_TAC[chi_msb];
  BY(REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`])
  ]);;
  (* }}} *)


let JDHAWAY_0 = 
prove_by_refinement(
  `!V ul p1 p2 t1 t2. packing V /\ saturated V /\ leaf V ul /\
    (voronoi_list V ul = convex hull {p1, p2}) /\
    ~(p1 = p2) /\
      (circumcenter (set_of_list ul) = t1 % p1 + t2 % p2) /\
    (t1 + t2 = &1) /\
    (&0 < t1 /\ &0 < t2) ==>
     ~(chi_msb ul p1 = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP CHI_MSB_IMP_COPLANAR));
  TYPIFY `p1 IN affine hull (set_of_list ul)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC COPLANAR_INSERT;
    CONJ2_TAC;
      TYPIFY `p1 INSERT set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul, p1}` ENOUGH_TO_SHOW_TAC;
        BY(DISCH_THEN (unlist ASM_REWRITE_TAC));
      GMATCH_SIMP_TAC set_of_list3;
      CONJ2_TAC;
        BY(SET_TAC[]);
      BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
    MATCH_MP_TAC Rogers.MHFTTZN1;
    BY(ASM_MESON_TAC[leaf;IN]);
  INTRO_TAC Rogers.MHFTTZN3 [`V`;`ul`;`2`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[leaf;IN]);
  REWRITE_TAC[EXTENSION;IN_INTER;IN_SING];
  DISCH_THEN (MP_TAC o (ISPEC `p1:real^3`));
  ASM_REWRITE_TAC[];
  REWRITE_TAC[AFFINE_HULL_CONVEX_HULL];
  TYPIFY `p1 IN affine hull {p1, p2}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    INTRO_TAC Qzksykg.SET_SUBSET_AFFINE_HULL [`{p1,p2}`];
    BY(SET_TAC[]);
  FIRST_X_ASSUM_ST `&1` MP_TAC;
  REWRITE_TAC[arith `t1 + t2 = &1 <=> t1 = &1 - t2`];
  DISCH_THEN SUBST1_TAC;
  TYPIFY `p1 = (&1 - t2) % p1 + t2 % p2 <=> t2 % p1 = t2 % p2` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  REWRITE_TAC[VECTOR_MUL_LCANCEL];
  BY(ASM_SIMP_TAC[arith `&0 < t ==> ~(t = &0)`])
  ]);;
  (* }}} *)

let JDHAWAY_1 = 
prove_by_refinement(
  `!V ul.
    packing V /\ saturated V /\ leaf V ul ==>
    chi_msb ul (circumcenter (set_of_list ul)) = &0`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  MATCH_MP_TAC AFFINE_IMP_CHI_MSB_0;
  CONJ_TAC;
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2+1 = 3`]);
  MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS;
  BY(ASM_MESON_TAC[leaf;IN])
  ]);;
  (* }}} *)

let JDWAWAY = 
prove_by_refinement(
  `!V ul p1 p2 t1 t2.
    packing V /\ saturated V /\ leaf V ul /\
(voronoi_list V ul = convex hull {p1, p2}) /\
    ~(p1 = p2) /\
      (circumcenter (set_of_list ul) = t1 % p1 + t2 % p2) /\
    (t1 + t2 = &1) /\
    (&0 < t1 /\ &0 < t2) ==>
     ~(chi_msb ul p1 = &0) /\ ~(chi_msb ul p2 = &0) /\
     (chi_msb ul p1 < &0 <=> &0 < chi_msb ul p2)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  SUBCONJ_TAC;
    INTRO_TAC JDHAWAY_0 [`V`;`ul`;`p1`;`p2`;`t1`;`t2`];
    DISCH_THEN MATCH_MP_TAC;
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  SUBCONJ_TAC;
    INTRO_TAC JDHAWAY_0 [`V`;`ul`;`p2`;`p1`;`t2`;`t1`];
    DISCH_THEN MATCH_MP_TAC;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      AP_TERM_TAC;
      BY(SET_TAC[]);
    CONJ_TAC;
      BY(VECTOR_ARITH_TAC);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  DISCH_TAC;
  INTRO_TAC JDHAWAY_1 [`V`;`ul`];
  ASM_SIMP_TAC[CHI_MSB_ADDITIVE];
  TYPIFY `&0 < chi_msb ul p2  <=> &0 < t2 * chi_msb ul p2` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[REAL_MUL_POS_LT];
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  DISCH_THEN (SUBST1_TAC o (MATCH_MP (arith `t1 * x + y = &0 ==> y = t1 * (--x)`)));
  REWRITE_TAC[REAL_MUL_POS_LT];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let cc_pe_exists = 
prove_by_refinement(
  `!V ul. ?p1. (?p2. packing V /\ saturated V /\ leaf V ul ==>
   (voronoi_list V ul = convex hull {p1, p2}) /\
      ~(p1 = p2) /\
      &0 < chi_msb ul p1)
     `,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[MESON[] `(?p. x ==> R p) <=> (x ==> ?p. R p)`];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC FUZBZGI_1 [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  ASM_CASES_TAC `&0 < chi_msb ul p1`;
    GEXISTL_TAC [`p1`;`p2`];
    BY(ASM_REWRITE_TAC[]);
  GEXISTL_TAC [`p2`;`p1`];
  ASM_REWRITE_TAC[];
  CONJ_TAC;
    AP_TERM_TAC;
    BY(SET_TAC[]);
  INTRO_TAC (GSYM JDWAWAY) [`V`;`ul`;`p1`;`p2`;`t1`;`t2`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let cc_pe = new_specification ["cc_pe1";
"cc_pe2"] 
  (REWRITE_RULE[SKOLEM_THM] cc_pe_exists);;

let FACET_OF_SEGMENT = 
prove_by_refinement(
  `!a (b:real^A). ~(a = b) ==> {a} facet_of segment [a,b]`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[facet_of];
  REWRITE_TAC[AFF_DIM_SING];
  CONJ_TAC;
    REWRITE_TAC[FACE_OF_SING];
    BY(REWRITE_TAC[EXTREME_POINT_OF_SEGMENT]);
  CONJ_TAC;
    BY(SET_TAC[]);
  REWRITE_TAC[SEGMENT_CONVEX_HULL];
  REWRITE_TAC[AFF_DIM_CONVEX_HULL];
  REWRITE_TAC[AFF_DIM_2];
  ASM_REWRITE_TAC[];
  BY(INT_ARITH_TAC)
  ]);;
  (* }}} *)

let CC_PE_FACET_OF = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul ==>
    {cc_pe1 V ul} facet_of (voronoi_list V ul)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC cc_pe [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL ];
  MATCH_MP_TAC FACET_OF_SEGMENT;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let cc_uh_exists = 
prove_by_refinement(
  `!V ul. ?vl. packing V /\ saturated V /\ leaf V ul ==>
    vl IN barV V 3 /\ truncate_simplex 2 vl = ul /\ omega_list V vl = (cc_pe1 V ul)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[MESON[] `(?p. x ==> R p) <=> (x ==> ?p. R p)`];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC NWVRFMF [`V`;`ul`;`cc_pe1 V ul`];
  BY(ASM_SIMP_TAC[CC_PE_FACET_OF])
  ]);;
  (* }}} *)

let cc_uh = new_specification ["cc_uh"] 
  (REWRITE_RULE[SKOLEM_THM] cc_uh_exists);;
let cc_ke = new_definition `cc_ke V ul = 
  if hl (cc_uh V ul) < sqrt2 then 4 else 3`;;
let cc_A0 = new_definition 
  `cc_A0 (ul:(real^A) list) = aff_gt {EL 0 ul,EL 1 ul} {EL 2 ul}`;;
let cc_cell = new_definition `cc_cell V ul = mcell (cc_ke V ul) V (cc_uh V ul)`;;
let CC_CELL4 = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul /\ cc_ke V ul = 4 ==>
    cc_cell V ul = convex hull set_of_list (cc_uh V ul)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[cc_cell;Pack_defs.mcell;arith `~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)`];
  REWRITE_TAC[Pack_defs.mcell4];
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[cc_ke];
  REWRITE_TAC[Sphere.sqrt2];
  COND_CASES_TAC;
    BY(REWRITE_TAC[]);
  BY(REWRITE_TAC[arith `~(3=4)`])
  ]);;
  (* }}} *)

let CC_CELL3 = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul /\ cc_ke V ul = 3 ==>
    cc_cell V ul = convex hull
           (set_of_list (ul) UNION
            {mxi V (cc_uh V ul)})`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[cc_cell;Pack_defs.mcell;arith `~(3=0) /\ ~(3=1) /\ ~(3=2)`];
  REWRITE_TAC[Pack_defs.mcell3];
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[cc_ke;GSYM Sphere.sqrt2];
  COND_CASES_TAC;
    BY(REWRITE_TAC[arith `~(4=3)`]);
  REWRITE_TAC[arith `3=3`];
  ASM_SIMP_TAC[arith `~(x < y) ==> (y <= x)`];
  INTRO_TAC cc_uh [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM_ST `leaf` MP_TAC;
  REWRITE_TAC[leaf;IN;Sphere.BARV];
  REPEAT WEAK_STRIP_TAC;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let CC_KE_34 = 
prove_by_refinement(
  `!V ul. cc_ke V ul = 3 \/ cc_ke V ul = 4`,

  (* {{{ proof *)
  [
  BY(MESON_TAC[cc_ke])
  ]);;
  (* }}} *)

let CC_CELL34 = 
prove_by_refinement(
  `!V ul pp. packing V /\ saturated V /\ leaf V ul /\
  ((if (cc_ke V ul = 3) then mxi V (cc_uh V ul) else (EL 3 (cc_uh V ul))) = pp) ==> 
    cc_cell V ul = convex hull { EL 0 ul, EL 1 ul, EL 2 ul, pp}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  COND_CASES_TAC;
    ASM_SIMP_TAC[CC_CELL3];
    DISCH_TAC;
    AP_TERM_TAC;
    GMATCH_SIMP_TAC set_of_list3;
    CONJ_TAC;
      BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
    BY(SET_TAC[]);
  SUBGOAL_THEN `cc_ke V ul = 4` ASSUME_TAC;
    BY(ASM_MESON_TAC[CC_KE_34]);
  ASM_SIMP_TAC[CC_CELL4];
  DISCH_TAC;
  AP_TERM_TAC;
  GMATCH_SIMP_TAC set_of_list4;
  EXPAND_TAC "pp";
  CONJ_TAC;
    INTRO_TAC cc_uh [`V`;`ul`];
    ASM_REWRITE_TAC[];
    BY(MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
  INTRO_TAC cc_uh [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Packing3.EL_TRUNCATE_SIMPLEX [`cc_uh V ul`;`2`];
  ASM_REWRITE_TAC[];
  TYPIFY `2 + 1 <= LENGTH (cc_uh V ul)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    FIRST_X_ASSUM_ST `barV` MP_TAC;
    REWRITE_TAC[Sphere.BARV;IN];
    BY(MESON_TAC[arith `2 + 1 <= 3 + 1`]);
  BY(MESON_TAC[arith `0 <= 2 /\ 1 <= 2 /\ 2 <= 2`])
  ]);;
  (* }}} *)

let U2_IN_CC_CELL = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul ==>
    (EL 2 ul IN cc_cell V ul)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ABBREV_TAC `p = (if (cc_ke V ul = 3) then mxi V (cc_uh V ul) else (EL 3 (cc_uh V ul)))`;
  INTRO_TAC CC_CELL34 [`V`;`ul`;`p`];
  ASM_REWRITE_TAC[];
  DISCH_THEN SUBST1_TAC;
  MATCH_MP_TAC Marchal_cells_2_new.IN_SET_IMP_IN_CONVEX_HULL_SET;
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let U2_IN_AFF_GT = 
prove_by_refinement(
  `!V ul.  packing V /\ saturated V /\ leaf V ul ==>
    EL 2 ul IN aff_gt {EL 0 ul, EL 1 ul} {EL 2 ul}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  MATCH_MP_TAC Local_lemmas.DISJOINT_IMP_Z_IN_AFF_GT;
  REWRITE_TAC[DISJOINT;EXTENSION;NOT_IN_EMPTY;IN_INTER;IN_INSERT];
  GEN_TAC;
  DISCH_TAC;
  INTRO_TAC GBEWYFX [`V`;`ul`];
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC set_of_list3;
  CONJ_TAC;
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  FIRST_X_ASSUM MP_TAC;
  REPEAT WEAK_STRIP_TAC;
    TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul} = { EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
    BY(REWRITE_TAC[COLLINEAR_2]);
  TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul} = { EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  BY(REWRITE_TAC[COLLINEAR_2])
  ]);;
  (* }}} *)

let EL_CC_UH = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul ==>
    EL 0 (cc_uh V ul) = EL 0 ul /\
    EL 1 (cc_uh V ul) = EL 1 ul /\
    EL 2 (cc_uh V ul) = EL 2 ul`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC cc_uh [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Packing3.EL_TRUNCATE_SIMPLEX [`cc_uh V ul`;`2`];
  TYPIFY `2 + 1 <= LENGTH (cc_uh V ul)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `2 + 1 <= 3 + 1`]);
  BY(ASM_MESON_TAC[arith `0 <= 2 /\ 1 <= 2 /\ 2 <= 2`])
  ]);;
  (* }}} *)

let NUNRRDS_0 = 
prove_by_refinement(
  `!V ul.  packing V /\ saturated V /\ leaf V ul ==>
    ~(cc_A0 ul INTER cc_cell V ul = {})`,

  (* {{{ proof *)
  [
  REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER];
  REPEAT WEAK_STRIP_TAC;
  GOAL_TERM (fun w -> (FIRST_X_ASSUM (MP_TAC o (ISPEC ( env w `EL 2 ul`)))));
  REWRITE_TAC[];
  REWRITE_TAC[cc_A0];
  CONJ2_TAC;
    MATCH_MP_TAC U2_IN_CC_CELL;
    BY(ASM_REWRITE_TAC[]);
  COMMENT "second side";
  MATCH_MP_TAC U2_IN_AFF_GT;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let AFF_GE_MONO_TRANS = 
prove_by_refinement(
  `!X Y (S:real^A->bool). S SUBSET X ==> aff_ge (X DIFF S) (Y UNION S) SUBSET aff_ge X Y`,

  (* {{{ proof *)
  [
  BY(MESON_TAC[Local_lemmas.AFF_GE_MONO_TRANS])
  ]);;
  (* }}} *)

let NUNRRDS_1 = 
prove_by_refinement(
  `!V ul pp. packing V /\ saturated V /\ leaf V ul /\
   (if (cc_ke V ul = 3) then mxi V (cc_uh V ul) else (EL 3 (cc_uh V ul))) = pp 
  ==>
    cc_cell V ul SUBSET aff_ge {EL 0 ul, EL 1 ul, EL 2 ul} {pp}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC CC_CELL34 [`V`;`ul`;`pp`];
  ASM_REWRITE_TAC[];
  DISCH_THEN SUBST1_TAC;
  REWRITE_TAC[CONVEX_HULL_AFF_GE];
  INTRO_TAC (AFF_GE_MONO_TRANS) [`{EL 0 ul, EL 1 ul, EL 2 ul}`;`{pp}`;`{EL 0 ul, EL 1 ul, EL 2 ul}`];
  ANTS_TAC;
    BY(SET_TAC[]);
  TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul} DIFF {EL 0 ul, EL 1 ul, EL 2 ul} = {}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  TYPIFY `{pp} UNION {EL 0 ul, EL 1 ul, EL 2 ul} = {EL 0 ul, EL 1 ul, EL 2 ul, pp}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

let CELL4_NONDEG = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul /\ (cc_ke V ul = 4) ==>
    ~(EL 3 (cc_uh V ul) IN affine hull (set_of_list ul))`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Rogers.MHFTTZN1 [`V`;`ul`;`2`];
  INTRO_TAC Rogers.MHFTTZN1 [`V`;`cc_uh V ul`;`3`];
  INTRO_TAC cc_uh [`V`;`ul`];
  ASM_SIMP_TAC[IN];
  WEAK_STRIP_TAC;
  WEAK_STRIP_TAC;
  TYPIFY `barV V 2 ul` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(ASM_MESON_TAC[leaf;IN]);
  DISCH_TAC;
  TYPIFY `set_of_list (cc_uh V ul) = (EL 3 (cc_uh V ul)) INSERT (set_of_list ul)` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC set_of_list4;
    GMATCH_SIMP_TAC set_of_list3;
    CONJ_TAC;
      BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2+1=3`]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[Sphere.BARV;arith `3 + 1 = 4`]);
    ASM_SIMP_TAC[EL_CC_UH];
    BY(SET_TAC[]);
  COMMENT "1";
  FIRST_X_ASSUM_ST `int_of_num 3` MP_TAC;
  ASM_REWRITE_TAC[];
  ASM_REWRITE_TAC[AFF_DIM_INSERT];
  BY(INT_ARITH_TAC)
  ]);;
  (* }}} *)

let K4_CHI_MSB_EQVL = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul /\ 
    (cc_ke V ul = 4) 
  ==>
  re_eqvl (chi_msb ul (EL 3 (cc_uh V ul))) (chi_msb ul (cc_pe1 V ul))`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC cc_uh [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Rogers.XNHPWAB2 [`V`;`cc_uh V ul`;`3`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(ASM_MESON_TAC[cc_ke;arith `~(3 = 4)`;Sphere.sqrt2]);
  GMATCH_SIMP_TAC set_of_list4;
  CONJ_TAC;
    BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 =4`]);
  REWRITE_TAC[Marchal_cells_2_new.CONVEX_HULL_4;IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `chi_msb ul = chi_msb [EL 0 ul;EL 1 ul;EL 2 ul]` (C SUBGOAL_THEN SUBST1_TAC);
    ONCE_REWRITE_TAC[FUN_EQ_THM];
    BY(REWRITE_TAC[chi_msb;HD;TL;EL;arith `1 = SUC 0 /\ 2 = SUC 1`]);
  INTRO_TAC EL_CC_UH [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC chi_msb_additive_d;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC RE_EQVL_SCALE2;
  REWRITE_TAC[RE_EQVL_REFL];
  ASM_SIMP_TAC[arith `&0 <= z ==> (&0 < z <=> ~(z = &0))`];
  DISCH_TAC;
  TYPIFY `chi_msb ul (cc_pe1 V ul) = &0` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_REWRITE_TAC[];
    TYPIFY `chi_msb ul = chi_msb [EL 0 ul;EL 1 ul;EL 2 ul]` (C SUBGOAL_THEN SUBST1_TAC);
      ONCE_REWRITE_TAC[FUN_EQ_THM];
      BY(REWRITE_TAC[chi_msb;HD;TL;EL;arith `1 = SUC 0 /\ 2 = SUC 1`]);
    GMATCH_SIMP_TAC chi_msb_additive_d;
    ASM_REWRITE_TAC[arith `&0 * t = &0`];
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  INTRO_TAC cc_pe [`V`;`ul`];
  ASM_REWRITE_TAC[];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let K4_CHI_MSB_POS = 
prove_by_refinement(
    `!V ul. packing V /\ saturated V /\ leaf V ul /\ 
    (cc_ke V ul = 4) 
  ==>
   ( &0 < chi_msb ul (EL 3 (cc_uh V ul )))`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC K4_CHI_MSB_EQVL [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[Trigonometry2.re_eqvl];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
  ASM_REWRITE_TAC[];
  INTRO_TAC cc_pe [`V`;`ul`];
  ASM_REWRITE_TAC[];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let MXI_BETWEEN = 
prove_by_refinement(
  `!V ul vl. packing V /\ saturated V /\ leaf V ul /\ cc_ke V ul = 3 /\
    cc_uh V ul = vl ==>
    between (mxi V vl) (omega_list_n V vl 2, omega_list_n V vl 3) /\
    dist(EL 0 ul, mxi V vl) = sqrt2`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Marchal_cells_2_new.MXI_EXPLICIT [`V`;`cc_uh V ul`;`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 (cc_uh V ul)`];
  INTRO_TAC EL_CC_UH [`V`;`ul`];
  INTRO_TAC cc_uh [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
  ANTS_TAC;
    CONJ_TAC;
      BY(ASM_MESON_TAC[IN]);
    CONJ_TAC;
      FIRST_X_ASSUM_ST `barV` MP_TAC;
      REWRITE_TAC[LENGTH4;IN;Sphere.BARV;arith `3 + 1 =4`];
      REPEAT WEAK_STRIP_TAC;
      BY(ASM_MESON_TAC[ LENGTH4]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[leaf]);
    BY(ASM_MESON_TAC[cc_ke;arith `~(4 = 3)`;arith `sqrt2 <= x <=> ~(x < sqrt2)`]);
  REPEAT WEAK_STRIP_TAC;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let affine_invert = 
prove_by_refinement(
  `!u p (q:real^A) s. ~(u= &0) /\ affine s /\ (&1 - u) % p + u % q IN s /\ p IN s ==>
    q IN s`,

  (* {{{ proof *)
  [
  REWRITE_TAC[affine];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`((&1 - u) % p + u % q)`;`p`;`inv u`;`&1 - inv u`]);
  ASM_REWRITE_TAC[arith `x + &1 - x = &1`];
  TYPIFY `inv u % ((&1 - u) % p + u % q) + (&1 - inv u) % p = q` (C SUBGOAL_THEN SUBST1_TAC);
    TYPIFY `inv u % ((&1 - u) % p + u % q) + (&1 - inv u) % p = (inv u * (&1 - u) + (&1 - inv u)) % p + (inv u * u) % q` (C SUBGOAL_THEN SUBST1_TAC);
      BY(VECTOR_ARITH_TAC);
    TYPIFY `(inv u * (&1 - u) + &1 - inv u) = &0` (C SUBGOAL_THEN SUBST1_TAC);
      Calc_derivative.CALC_ID_TAC;
      BY(ASM_REWRITE_TAC[]);
    TYPIFY `(inv u * u) = &1` (C SUBGOAL_THEN SUBST1_TAC);
      Calc_derivative.CALC_ID_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(VECTOR_ARITH_TAC);
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let CELL3_NONDEG = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul /\ cc_ke V ul = 3 ==>
  ~(mxi V (cc_uh V ul) IN affine hull (set_of_list ul)) /\
  &0 < chi_msb ul (mxi V (cc_uh V ul))`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ABBREV_TAC `vl = cc_uh V ul`;
  INTRO_TAC MXI_BETWEEN [`V`;`ul`;`vl`];
  ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT;closed_segment;IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC cc_pe [`V`;`ul`];
  INTRO_TAC cc_uh [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
  INTRO_TAC Sphere.OMEGA_LIST [`V`;`vl`];
  ASM_REWRITE_TAC[arith `4 - 1 = 3`];
  DISCH_TAC;
  INTRO_TAC EL_CC_UH [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `omega_list_n V vl 2 = circumcenter (set_of_list ul)` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC (GSYM Rogers.XNHPWAB1) [`V`;`ul`;`2`];
    ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
    ANTS_TAC;
      BY(ASM_MESON_TAC[leaf;IN]);
    DISCH_THEN SUBST1_TAC;
    FIRST_X_ASSUM_ST `leaf` MP_TAC;
    REWRITE_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 =3`];
    REPEAT WEAK_STRIP_TAC;
    ASM_REWRITE_TAC[Pack_concl.JJGTQMN;arith `3 - 1 = 2`];
    INTRO_TAC Packing3.TRUNCATE_SIMPLEX_REFL [`2`;`ul`];
    ASM_REWRITE_TAC[arith `3 = 2 + 1`];
    REPEAT (GMATCH_SIMP_TAC (GSYM Packing3.OMEGA_LIST_LEMMA));
    ASM_REWRITE_TAC[arith `2 + 1 <= 3 /\ 2 + 1 <= 4`];
    BY(ASM_MESON_TAC[]);
  GMATCH_SIMP_TAC CHI_MSB_ADDITIVE;
  ASM_REWRITE_TAC[arith `&1 - u + u = &1`];
  GMATCH_SIMP_TAC JDHAWAY_1;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[arith `x * &0 + v = v`];
  GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
  ASM_SIMP_TAC[arith `&0 <= u ==> (&0 < u <=> ~(u = &0))`];
  SUBGOAL_THEN ` &0 < chi_msb ul (omega_list_n V vl 3)` (unlist REWRITE_TAC);
    BY(ASM_MESON_TAC[]);
  COMMENT "1";
  ASM_CASES_TAC `u = &0`;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `&1 - u` MP_TAC;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[VECTOR_MUL_LID;arith `&1 - &0 = &1 /\ x + &0 = x`;VECTOR_MUL_LZERO;VECTOR_ADD_RID];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `leaf` MP_TAC;
    REWRITE_TAC[leaf;IN];
    REPEAT WEAK_STRIP_TAC;
    FIRST_X_ASSUM_ST `hl` MP_TAC;
    REWRITE_TAC[];
    GMATCH_SIMP_TAC Rogers.HL_EQ_DIST0;
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    BY(ASM_MESON_TAC[DIST_SYM;EL;arith `~(sqrt2 < sqrt2)`]);
  ASM_REWRITE_TAC[];
  SUBGOAL_THEN `&0 < u` ASSUME_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  DISCH_TAC;
  TYPIFY `cc_pe1 V ul IN affine hull set_of_list ul` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC affine_invert;
    GEXISTL_TAC [`u`;`circumcenter (set_of_list ul)`];
    ASM_REWRITE_TAC[AFFINE_AFFINE_HULL];
    MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS;
    BY(ASM_MESON_TAC[leaf;IN]);
  DISCH_TAC;
  FIRST_X_ASSUM_ST `chi_msb` MP_TAC;
  REWRITE_TAC[];
  MATCH_MP_TAC (arith `(x = &0) ==> ~(&0 < x)`);
  MATCH_MP_TAC AFFINE_IMP_CHI_MSB_0;
  ASM_REWRITE_TAC[];
  BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`])
  ]);;
  (* }}} *)

let CELL_NN = 
prove_by_refinement(
  `!V ul p.  packing V /\ saturated V /\ leaf V ul /\ 
    p IN cc_cell V ul ==> &0 <= chi_msb ul p`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  INTRO_TAC CHI_MSB_CONVEX [`ul`];
  FIRST_X_ASSUM_ST `cc_cell` MP_TAC;
  GMATCH_SIMP_TAC CC_CELL34;
  ABBREV_TAC `pp = (if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul))`;
  GEXISTL_TAC [`pp`];
  ASM_REWRITE_TAC[];
  INTRO_TAC Marchal_cells.CONVEX_HULL_SUBSET [`{EL 0 ul, EL 1 ul, EL 2 ul, pp}`;`{p | &0 <= chi_msb ul p}`];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM_ST `SUBSET` MP_TAC;
  ANTS_TAC;
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_ELIM_THM];
    GEN_TAC;
    SUBGOAL_THEN `&0 <= chi_msb ul pp` ASSUME_TAC;
      MATCH_MP_TAC (arith `&0 < x ==> &0 <= x`);
      EXPAND_TAC "pp";
      COND_CASES_TAC;
        INTRO_TAC CELL3_NONDEG [`V`;`ul`];
        BY(ASM_MESON_TAC[]);
      SUBGOAL_THEN `cc_ke V ul = 4` ASSUME_TAC;
        BY(ASM_MESON_TAC[CC_KE_34]);
      MATCH_MP_TAC K4_CHI_MSB_POS;
      BY(ASM_REWRITE_TAC[]);
    SUBGOAL_THEN `x IN set_of_list ul ==> &0 <= chi_msb ul x` ASSUME_TAC;
      DISCH_TAC;
      MATCH_MP_TAC (arith ` x = &0 ==> &0 <= x`);
      MATCH_MP_TAC AFFINE_IMP_CHI_MSB_0;
      BY(ASM_MESON_TAC[SUBSET;Qzksykg.SET_SUBSET_AFFINE_HULL]);
    FIRST_X_ASSUM MP_TAC;
    GMATCH_SIMP_TAC set_of_list3;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(ASM_MESON_TAC[]);
  TYPIFY `convex hull {p | &0 <= chi_msb ul p} =  {p | &0 <= chi_msb ul p}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(ASM_MESON_TAC[CONVEX_HULL_EQ]);
  REWRITE_TAC[SUBSET;IN_ELIM_THM];
  DISCH_THEN MATCH_MP_TAC;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let delta_delta_x = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. delta x1 x2 x3 x6 x5 x4 = delta_x x1 x2 x3 x4 x5 x6 `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Collect_geom.delta;Sphere.delta_x];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let ZWVCBMN = 
prove_by_refinement(
  `!a b c d.  ~coplanar {a,b,c,d} ==> &0 < vol (convex hull {a,b,c,d})`,

  (* {{{ proof *)
  [
  REWRITE_TAC[VOLUME_OF_CLOSED_TETRAHEDRON];
  REPEAT WEAK_STRIP_TAC;
  GMATCH_SIMP_TAC REAL_LT_DIV;
  REWRITE_TAC[ REAL_OF_NUM_LT];
  GMATCH_SIMP_TAC REAL_LT_RSQRT;
  REWRITE_TAC[GSYM delta_delta_x];
  INTRO_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] (GSYM Collect_geom.POLFLZY)) [`a`;`b`;`c`;`d`];
  INTRO_TAC coplanar_eq_coplanar_alt [`{a,b,c,d}`];
  REWRITE_TAC[DIMINDEX_3];
  ANTS_TAC;
    BY(ARITH_TAC);
  DISCH_THEN (SUBST1_TAC o GSYM);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ASM_SIMP_TAC[arith `0 < 12`;arith `~(x = &0)  ==> (&0 pow 2 < x <=> &0 <= x)`];
  BY(MESON_TAC[Collect_geom2.DELTA_POS_4POINTS])
  ]);;
  (* }}} *)

let MCELL4_NONPLANAR  = 
prove_by_refinement(
  `!V vl. packing V /\ saturated V /\ barV V 3 vl /\ hl vl < sqrt2 ==>
    ~coplanar (mcell4 V vl)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Rogers.MHFTTZN1 [`V`;`vl`;`3`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC Pack_defs.mcell4 [`V`;`vl`];
  ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
  DISCH_TAC;
  FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP COPLANAR_IMP_AFF_DIM));
  INTRO_TAC AFF_DIM_SUBSET [`set_of_list vl`;`convex hull set_of_list vl`];
  ANTS_TAC;
    BY(MESON_TAC[HULL_SUBSET]);
  REPEAT (FIRST_X_ASSUM_ST `aff_dim` MP_TAC);
  ASM_REWRITE_TAC[];
  BY(INT_ARITH_TAC)
  ]);;
  (* }}} *)

let MXI_IN_VORONOI_LIST = 
prove_by_refinement(
  `!V vl. packing V /\ saturated V /\ barV V 3 vl /\ sqrt2 <= hl vl /\
   hl (truncate_simplex 2 vl) < sqrt2 ==>
   mxi V vl IN voronoi_list V (truncate_simplex 2 vl) /\
   dist(EL 0 vl,mxi V vl) = sqrt2`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN [`V`;`vl`;`3`;`2`;`2`];
  INTRO_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN [`V`;`vl`;`3`;`2`;`3`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(ARITH_TAC);
  DISCH_TAC;
  ANTS_TAC;
    BY(ARITH_TAC);
  DISCH_TAC;
  INTRO_TAC Packing3.CONVEX_VORONOI_LIST [`V`;`truncate_simplex 2 vl`];
  DISCH_TAC;
  INTRO_TAC Marchal_cells_2_new.MXI_EXPLICIT [`V`;`vl`;`EL 0 vl`;`EL 1 vl`;`EL 2 vl`;`EL 3 vl`];
  REWRITE_TAC[BETWEEN_IN_CONVEX_HULL];
  ANTS_TAC;
    ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
    GMATCH_SIMP_TAC LENGTH4;
    REWRITE_TAC[EL;HD;TL;arith `3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`];
    BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3+1=4`]);
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[Sphere.sqrt2];
  TYPED_ABBREV_TAC `(a:real^3->bool) = voronoi_list V (truncate_simplex 2 vl)` ;
  TYPIFY `{omega_list_n V vl 2,omega_list_n V vl 3} SUBSET a` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP Marchal_cells.CONVEX_HULL_SUBSET));
  BY(ASM_MESON_TAC[CONVEX_HULL_EQ;Packing3.IN_TRANS])
  ]);;
  (* }}} *)

let VORONOI_LIST_EQ = 
prove_by_refinement(
  `!V ul p k.  p IN voronoi_list V ul /\ barV V k ul==>
    (?r. !q. q IN set_of_list ul ==> dist(p,q) = r)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.VORONOI_LIST;Sphere.VORONOI_SET;Sphere.voronoi_closed;IN_INTERS;IN_ELIM_THM;LEFT_IMP_EXISTS_THM];
  REPEAT GEN_TAC;
  ONCE_REWRITE_TAC[MESON [] `(!p q. R p q) <=> (!q p. R p q)`];
  REWRITE_TAC[TAUT `(a /\ b ==> c) <=> (a ==> b ==> c)`];
  REWRITE_TAC[MESON[] `!a. (!p. a ==> b p) <=> (a ==> (!p. b p))`];
  REWRITE_TAC[MESON[] `!a p. (!t. (t = a) ==> (p IN t)) <=> (p IN a)`];
  REWRITE_TAC[IN_ELIM_THM];
  TYPIFY `set_of_list ul = {}` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[NOT_IN_EMPTY]);
  FIRST_X_ASSUM (MP_TAC o (REWRITE_RULE[Misc_defs_and_lemmas.EMPTY_EXISTS]));
  REPEAT WEAK_STRIP_TAC;
  GOAL_TERM (fun w -> (EXISTS_TAC ( env w `dist(p,u)`)));
  REPEAT WEAK_STRIP_TAC;
  BY(ASM_MESON_TAC[Packing3.BARV_SUBSET;arith `x <= y /\ y <= x ==> (x = y)`;IN;SUBSET])
  ]);;
  (* }}} *)

let NOT_COL_IMP_RADV = 
prove_by_refinement(
  `!va vb (vc:real^3). ~collinear {va, vb, vc}
        ==> (!w. w IN {va, vb, vc} 
        ==> radV {va, vb, vc} = dist (circumcenter {va, vb, vc},w))`,

  (* {{{ proof *)
  [
  MESON_TAC[IN;Collect_geom.NOT_COL_IMP_RADV_PROPERTIY]
  ]);;
  (* }}} *)

let MCELL3_NONPLANAR = 
prove_by_refinement(
  `!V vl. packing V /\ saturated V /\ barV V 3 vl /\ sqrt2 <= hl vl /\
   hl (truncate_simplex 2 vl) < sqrt2 ==>
    ~coplanar (mcell3 V vl)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3+1 = 4`]);
  INTRO_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX [`2`;`vl`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[arith `2 + 1 <= 4`]);
  REWRITE_TAC[arith `2 + 1 = 3`];
  DISCH_TAC;
  TYPIFY `coplanar (set_of_list (truncate_simplex 2 vl))` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC set_of_list3;
    BY(ASM_REWRITE_TAC[COPLANAR_3]);
  INTRO_TAC Pack_defs.mcell3 [`V`;`vl`];
  ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
  DISCH_TAC;
  TYPIFY `set_of_list(truncate_simplex 2 vl) = {EL 0 vl,EL 1 vl,EL 2 vl}` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC set_of_list3;
    ASM_REWRITE_TAC[];
    REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
    ASM_REWRITE_TAC[];
    BY(ARITH_TAC);
  TYPIFY `barV V 2 (truncate_simplex 2 vl)` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
    BY(ASM_MESON_TAC[arith `2 <= 3`]);
  COMMENT "GBE";
  INTRO_TAC GBEWYFX [`V`;`truncate_simplex 2 vl`];
  ANTS_TAC;
    BY(ASM_SIMP_TAC[leaf;IN]);
  DISCH_TAC;
  COMMENT "main reduction";
  TYPIFY `(mxi V vl IN affine hull set_of_list (truncate_simplex 2 vl))` ENOUGH_TO_SHOW_TAC;
    DISCH_TAC;
    INTRO_TAC Rogers.OAPVION3 [`set_of_list (truncate_simplex 2 vl)`];
    ANTS_TAC;
      DISCH_TAC;
      FIRST_X_ASSUM_ST `collinear` MP_TAC;
      ASM_REWRITE_TAC[];
      MATCH_MP_TAC AFFINE_DEPENDENT_IMP_COLLINEAR_3;
      BY(ASM_MESON_TAC[]);
    GOAL_TERM (fun w -> (DISCH_THEN (MP_TAC o (ISPEC ( env w `mxi V vl`)))));
    ASM_REWRITE_TAC[];
    INTRO_TAC MXI_IN_VORONOI_LIST [`V`;`vl`];
    ASM_REWRITE_TAC[];
    REPEAT WEAK_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    ANTS_TAC;
      GOAL_TERM (fun w -> (EXISTS_TAC ( env w `sqrt2`)));
      REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
      GEN_TAC;
      DISCH_TAC;
      INTRO_TAC VORONOI_LIST_EQ [`V`;`truncate_simplex 2 vl`;`mxi V vl`;`2`];
      ANTS_TAC;
        BY(ASM_REWRITE_TAC[]);
      REPEAT WEAK_STRIP_TAC;
      FIRST_ASSUM MP_TAC;
      DISCH_THEN GMATCH_SIMP_TAC;
      ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
      GOAL_TERM (fun w -> (FIRST_X_ASSUM (MP_TAC o (ISPEC ( env w `EL 0 vl`)))));
      ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
      BY(ASM_MESON_TAC[DIST_SYM]);
    INTRO_TAC GBEWYFX [`V`;`truncate_simplex 2 vl`];
    ANTS_TAC;
      BY(ASM_SIMP_TAC[leaf;IN]);
    FIRST_X_ASSUM_ST `hl` MP_TAC;
    ASM_REWRITE_TAC[Pack_defs.HL];
    INTRO_TAC NOT_COL_IMP_RADV [`EL 0 vl`;`EL 1 vl`; `EL 2 vl`];
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    FIRST_X_ASSUM MP_TAC;
    BY(MESON_TAC[arith `~(sqrt2 < sqrt2)` ; DIST_SYM]);
  COMMENT "back to 1 goal";
  TYPIFY `coplanar (set_of_list (truncate_simplex 2 vl) UNION {mxi V vl})` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC COPLANAR_SUBSET;
    GOAL_TERM (fun w -> (EXISTS_TAC ( env w `mcell3 V vl`)));
    ASM_REWRITE_TAC[];
    BY(MESON_TAC[HULL_SUBSET]);
  COMMENT "1b";
  TYPIFY `aff_dim (set_of_list (truncate_simplex 2 vl) UNION {mxi V vl}) <= &2` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC COPLANAR_IMP_AFF_DIM;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `&2 <= aff_dim (set_of_list (truncate_simplex 2 vl))` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC COLLINEAR_AFF_DIM [`(set_of_list (truncate_simplex 2 vl))`];
    ASM_REWRITE_TAC[];
    BY(INT_ARITH_TAC);
  FIRST_X_ASSUM_ST `UNION` MP_TAC;
  COMMENT "1c";
  INTRO_TAC AFF_DIM_INSERT [`mxi V vl`;`set_of_list (truncate_simplex 2 vl)`];
  COND_CASES_TAC;
    BY(REWRITE_TAC[]);
  FIRST_X_ASSUM_ST `aff_dim` MP_TAC;
  TYPIFY `mxi V vl INSERT set_of_list (truncate_simplex 2 vl) = set_of_list (truncate_simplex 2 vl) UNION {mxi V vl}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  BY(INT_ARITH_TAC)
  ]);;
  (* }}} *)

let MCELL2_SUBSET_AFF_GE = 
prove_by_refinement(
  `!V ul.  mcell2 V ul SUBSET aff_ge {HD ul, HD (TL ul)} {mxi V ul, omega_list_n V ul 3}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[Pack_defs.mcell2];
  COND_CASES_TAC;
    REWRITE_TAC[LET_DEF;LET_END_DEF];
    BY(SET_TAC[]);
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let CONDS_IN_CONV2 = 
prove_by_refinement(
  `!t2 t3 (v:real^A) w. &0 <= t2 /\ &0 <= t3 /\ ~(t2 = &0 /\ t3 = &0)
        ==> t2 / (t2 + t3) % v + t3 / (t2 + t3) % w IN conv {v, w}`,

  (* {{{ proof *)
  [
  MESON_TAC[Local_lemmas.CONDS_IN_CONV2]
  ]);;
  (* }}} *)

let NEG_SIGNS_LEMMA = 
prove_by_refinement(
  `!(a:real^3) b c d t0' t0'' t1 t1' s s'.
  aff {a, b} INTER conv {c, d} = {} /\
 c = t0' % a + t1 % b + s % p /\
 t0' + t1 + s = &1 /\
 d = t0'' % a + t1' % b + s' % p /\
 t0'' + t1' + s' = &1 
==>
 s < &0 ==> s' < &0`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[arith `s' < &0 <=> ~(&0 <= s')`];
  DISCH_TAC;
  FIRST_X_ASSUM_ST `INTER` MP_TAC;
  REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;NOT_FORALL_THM];
  GOAL_TERM (fun w -> (EXISTS_TAC( env w ` (s' / ( s' + (-- s))) % c + ((-- s) / (s' + (--s))) % d`)));
  CONJ2_TAC;
    MATCH_MP_TAC CONDS_IN_CONV2;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  TYPIFY `s' / (s' + --s) % (t0' % a + t1 % b + s % p) + --s / (s' + --s) % (t0'' % a + t1' % b + s' % p) = s' / (s' + --s) % (t0' % a + t1 % b ) + --s / (s' + --s) % (t0'' % a + t1' % b ) + ((s' * s/ (s' + --s)) + ( s' * (--s) / (s' + --s))) % p` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  TYPIFY ` (s' * s / (s' + --s) + s' * --s / (s' + --s)) = &0` (C SUBGOAL_THEN SUBST1_TAC);
    Calc_derivative.CALC_ID_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  REWRITE_TAC[Sphere.aff];
  REWRITE_TAC[AFFINE_HULL_2;IN_ELIM_THM];
  GEXISTL_TAC [`(s' / (s' + --s) * t0' + (-- s)/(s' + --s) * t0'')`;`(s' / (s' + --s) * t1 + (-- s)/(s' + --s) * t1')`];
  CONJ_TAC;
    Calc_derivative.CALC_ID_TAC;
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    REPEAT (FIRST_X_ASSUM_ST `&1` MP_TAC);
    BY(CONV_TAC (REAL_RING));
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let COPLANAR_AFF_GE_REDUCE = 
prove_by_refinement(
  `!(a:real^3) b c d. coplanar {a,b,c,d} /\ aff {a,b} INTER conv {c,d} = {} /\
    ~(a = b) ==> (?p. aff_ge {a,b} {c,d} SUBSET aff_ge {a,b} {p})`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `aff_ge {a,b} {c,d} SUBSET aff{a,b}` ASM_CASES_TAC;
    TYPIFY `?p. DISJOINT {a,b} {p}` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_MESON_TAC[Fan.th3a;Trigonometry2.TOW_DISTINCT_POINTS_EXISTS_RD_NOT_COLLINEAR]);
    REPEAT WEAK_STRIP_TAC;
    GOAL_TERM (fun w -> (EXISTS_TAC ( env w `p`)));
    BY(ASM_MESON_TAC[AFF_GE_MONO_RIGHT;SUBSET_TRANS;EMPTY_SUBSET;AFF_GE_EQ_AFFINE_HULL;Trigonometry2.aff]);
  TYPIFY `?p. p IN aff_ge {a,b} {c,d} DIFF aff{a,b}` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM MP_TAC;
    BY(SET_TAC[]);
  REWRITE_TAC[IN_DIFF];
  REPEAT WEAK_STRIP_TAC;
  GOAL_TERM (fun w -> (EXISTS_TAC ( env w `p`)));
  TYPIFY `p IN affine hull {a,b,c,d}` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC AFF_GE_SUBSET_AFFINE_HULL [`{a,b}`;`{c,d}`];
    TYPIFY `{a,b} UNION {c,d} = {a,b,c,d}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
    BY(SET_TAC[]);
  TYPIFY `~(collinear {a,b,p})` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM (MP_TAC o (MATCH_MP COLLINEAR_3_IN_AFFINE_HULL) o GSYM);
    BY(ASM_MESON_TAC[Sphere.aff]);
  TYPIFY `aff_dim {a,b,p} = &2` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[COLLINEAR_AFF_DIM];
    INTRO_TAC AFF_DIM_2 [`a`;`b`];
    ASM_REWRITE_TAC[];
    INTRO_TAC AFF_DIM_INSERT [`p`;`{a,b}`];
    ASM_REWRITE_TAC[GSYM Sphere.aff];
    TYPIFY `{p,a,b} = {a,b,p}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(INT_ARITH_TAC);
  INTRO_TAC AFF_DIM_EQ_AFFINE_HULL [`{a,b,p}`;`affine hull {a,b,c,d}`];
  ANTS_TAC;
    CONJ_TAC;
      REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
      BY(REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC HULL_INC THEN SET_TAC[]);
    INTRO_TAC COPLANAR_IMP_AFF_DIM [`{a,b,c,d}`];
    ASM_REWRITE_TAC[];
    BY(REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
  REWRITE_TAC[Planarity.AFFINE_HULL_AFFINE_EQ];
  DISCH_TAC;
  TYPIFY `{c,d} SUBSET affine hull {a,b,p}` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_REWRITE_TAC[];
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC HULL_INC THEN SET_TAC[]);
  TYPIFY `(?tt0 t1 s. c = tt0 % a + t1 % b + s % p /\ tt0 + t1 + s = &1) /\ (?tt0' t1' s'. d = tt0' % a + t1' % b + s' % p /\ tt0' + t1' + s' = &1)` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
    REWRITE_TAC[AFFINE_HULL_3;IN_ELIM_THM];
    BY(MESON_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  SUBGOAL_THEN `s < &0 ==> s' < &0` ASSUME_TAC;
    COMMENT "change here";
    MATCH_MP_TAC NEG_SIGNS_LEMMA;
    GEXISTL_TAC [`a`;`b`;`c`;`d`;`tt0`;`tt0'`;`t1`;`t1'`];
    BY(ASM_REWRITE_TAC[]);
  SUBGOAL_THEN `s' < &0 ==> s < &0` ASSUME_TAC;
    MATCH_MP_TAC NEG_SIGNS_LEMMA;
    GEXISTL_TAC [`a`;`b`;`d`;`c`;`tt0'`;`tt0`;`t1'`;`t1`];
    TYPIFY `{d,c} = {c,d}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(ASM_REWRITE_TAC[]);
  COMMENT "back to 1";
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM_ST `x IN aff_ge u v` MP_TAC;
  TYPIFY `DISJOINT {a,b} {c,d}` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `INTER` MP_TAC;
    REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;Sphere.aff;DISJOINT;IN_INSERT];
    TYPIFY `a IN {a,b} /\ b IN {a,b} /\ c IN {c,d} /\ d IN {c,d}` (C SUBGOAL_THEN MP_TAC);
      BY(SET_TAC[]);
    TYPIFY `({a,b} = {b,a}) /\  ({c,d} = {d,c})` (C SUBGOAL_THEN MP_TAC);
      BY(SET_TAC[]);
    BY(MESON_TAC[HULL_INC;Geomdetail.U_IN_CONV2]);
  INTRO_TAC Nkezbfc_local.AFF_GE_2_2 [`a`;`b`;`c`;`d`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_THEN SUBST1_TAC;
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `(p =   t1'' % a +   t2 % b +   t3 % (tt0 % a + t1 % b + s % p) +   t4 % (tt0' % a + t1' % b + s' % p)) <=> (&1 - t3 * s - t4 * s') % p = (t1'' + t3 * tt0 + t4 * tt0' ) % a + (t2 + t3 * t1 + t4 * t1') % b` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  ASM_CASES_TAC `~(&1 - t3 * s - t4 * s' = &0)`;
    DISCH_TAC;
    FIRST_X_ASSUM_ST `aff` MP_TAC;
    REWRITE_TAC[Sphere.aff;AFFINE_HULL_2;IN_ELIM_THM];
    GEXISTL_TAC [`(t1'' + t3 * tt0 + t4 * tt0')/(&1 - t3 * s - t4 * s')`;`(t2 + t3 * t1 + t4 * t1')/(&1 - t3 * s - t4 * s')`];
    CONJ_TAC;
      Calc_derivative.CALC_ID_TAC;
      ASM_REWRITE_TAC[];
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN (CONV_TAC REAL_RING));
    MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP;
    EXISTS_TAC `&1 - t3 * s - t4 * s'`;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC];
    TYPIFY `((&1 - t3 * s - t4 * s') *  (t1'' + t3 * tt0 + t4 * tt0') / (&1 - t3 * s - t4 * s')) = (t1'' + t3 * tt0 + t4 * tt0')` (C SUBGOAL_THEN SUBST1_TAC);
      Calc_derivative.CALC_ID_TAC;
      BY(ASM_REWRITE_TAC[]);
    TYPIFY `((&1 - t3 * s - t4 * s') *  (t2 + t3 * t1 + t4 * t1') / (&1 - t3 * s - t4 * s')) =  (t2 + t3 * t1 + t4 * t1')` (C SUBGOAL_THEN SUBST1_TAC);
      Calc_derivative.CALC_ID_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(REWRITE_TAC[]);
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[];
  (REPEAT WEAK_STRIP_TAC);
  FIRST_X_ASSUM_ST `~` MP_TAC;
  REWRITE_TAC[];
  TYPIFY `&0 <= s /\ &0 <= s'` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[arith `&0 <= s /\ &0 <= s' <=> ~(s < &0 \/ s' < &0)`];
    DISCH_TAC;
    TYPIFY `s < &0 /\ s' < &0` (C SUBGOAL_THEN ASSUME_TAC);
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    TYPIFY `&0 < t3 * s + t4 * s' ` (C SUBGOAL_THEN MP_TAC);
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    REWRITE_TAC[];
    MATCH_MP_TAC (arith `&0 <= t3 * (-- s)  /\ &0 <= t4 * (-- s')  ==> ~(&0 < t3 *( s) + t4 * ( s'))`);
    GMATCH_SIMP_TAC REAL_LE_MUL;
    GMATCH_SIMP_TAC REAL_LE_MUL;
    BY(ASM_SIMP_TAC[arith `ss < &0 ==> &0 <= -- ss`]);
  REWRITE_TAC[SUBSET];
  GEN_TAC;
  GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC AFF_GE_2_1;
  ASM_REWRITE_TAC[IN_ELIM_THM];
  CONJ_TAC;
    MATCH_MP_TAC Fan.th3a;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  GEXISTL_TAC [`t1'''+t3' * tt0 + t4' * tt0'`;`t2' + t3' * t1 + t4' * t1'`;`t3' * s + t4' * s'`];
  CONJ_TAC;
    MATCH_MP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`);
    GMATCH_SIMP_TAC REAL_LE_MUL;
    GMATCH_SIMP_TAC REAL_LE_MUL;
    BY(ASM_REWRITE_TAC[]);
  CONJ_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN (CONV_TAC REAL_RING));
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let AFFINE_DEPENDENT_EXPLICIT_4 = 
prove_by_refinement(
  `!(a:real^A) b c d ta tb tc td. ~affine_dependent {a,b,c,d} /\
    CARD {a,b,c,d} = 4 /\
    ta + tb + tc + td = &0 /\
    ta % a + tb % b + tc % c + td % d = vec 0 ==>
    (ta = &0 /\ tb = &0 /\ tc = &0 /\ td = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC AFFINE_DEPENDENT_EXPLICIT[`{a,b,c,d}`];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[NOT_EXISTS_THM];
  DISCH_THEN (C INTRO_TAC [`{a,b,c,d}`;`\u. if (u=a) then ta else (if (u=b) then tb else (if (u=c) then tc else td))`]);
  TYPIFY `FINITE {a,b,c,d}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
  TYPIFY `{a, b, c, d} SUBSET {a, b, c, d}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(SET_TAC[]);
  TYPIFY `~(a = b) /\ ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d) /\ ~(c = d)` (C SUBGOAL_THEN (ASSUME_TAC));
    TYPIFY ` {a,b,c,d} = {a,c,b,d} /\ {a,b,c,d}= {a,d,b,c} /\ {a,b,c,d} = {b,c,a,d} /\ {a,b,c,d} = {b,d,a,c} /\ {a,b,c,d} = {c,d,a,b}` (C SUBGOAL_THEN MP_TAC);
      BY(SET_TAC[]);
    REPEAT WEAK_STRIP_TAC;
    BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT THEN FIRST_X_ASSUM_ST `4` (SUBST1_TAC o GSYM) THEN (REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC)) THEN MESON_TAC[]);
  TYPIFY `vsum {a, b, c, d}   (\v. (if v = a then ta else if v = b then tb else if v = c then tc else td) %        v) =   vec 0` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    REPEAT (GMATCH_SIMP_TAC (CONJUNCT2 VSUM_CLAUSES));
    REWRITE_TAC[ (CONJUNCT1 VSUM_CLAUSES)];
    ASM_REWRITE_TAC[FINITE_EMPTY;FINITE_INSERT;NOT_IN_EMPTY;IN_INSERT];
    FIRST_X_ASSUM_ST `0` MP_TAC;
    BY(VECTOR_ARITH_TAC);
  TYPIFY `sum {a, b, c, d}    (\u. if u = a then ta else if u = b then tb else if u = c then tc else td) =   &0` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    REPEAT (GMATCH_SIMP_TAC (CONJUNCT2 SUM_CLAUSES));
    REWRITE_TAC[ (CONJUNCT1 SUM_CLAUSES)];
    ASM_REWRITE_TAC[FINITE_EMPTY;FINITE_INSERT;NOT_IN_EMPTY;IN_INSERT];
    FIRST_X_ASSUM_ST `&0` MP_TAC;
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
  REWRITE_TAC[NOT_EXISTS_THM];
  COPY_TAC;
  COPY_TAC;
  COPY_TAC;
  DISCH_THEN (C INTRO_TAC [`a`]);
  FIRST_X_ASSUM (C INTRO_TAC [`b`]);
  FIRST_X_ASSUM (C INTRO_TAC [`c`]);
  FIRST_X_ASSUM (C INTRO_TAC [`d`]);
  ASM_REWRITE_TAC[];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let  COPLANAR_AFF_GE_REDUCE2 = 
prove_by_refinement(
  `!S (a:real^3) b c d.  ~coplanar {a,b,c,d} /\ coplanar S /\ {a,b} SUBSET S /\ S SUBSET aff_ge {a,b} {c,d} ==>
   (?p. S SUBSET aff_ge {a,b} {p})`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(a = b)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM_ST `~` MP_TAC;
    ASM_REWRITE_TAC[];
    TYPIFY `{b,b,c,d} = {b,c,d}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(REWRITE_TAC[COPLANAR_3]);
  TYPIFY `S SUBSET affine hull {a,b}` ASM_CASES_TAC;
    TYPIFY `?p. DISJOINT {a,b} {p}` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_MESON_TAC[Fan.th3a;Trigonometry2.TOW_DISTINCT_POINTS_EXISTS_RD_NOT_COLLINEAR]);
    REPEAT WEAK_STRIP_TAC;
    GOAL_TERM (fun w -> (EXISTS_TAC ( env w `p`)));
    BY(ASM_MESON_TAC[AFF_GE_MONO_RIGHT;SUBSET_TRANS;EMPTY_SUBSET;AFF_GE_EQ_AFFINE_HULL;Trigonometry2.aff]);
  TYPIFY `?p. p IN S DIFF affine hull {a,b}` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM MP_TAC;
    BY(SET_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `p` EXISTS_TAC;
  TYPIFY `p IN aff_ge {a,b} {c,d}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  REWRITE_TAC[SUBSET];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `x IN aff_ge {a,b} {c,d}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  TYPIFY `~(collinear {a,b,p})` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM (MP_TAC o (MATCH_MP COLLINEAR_3_IN_AFFINE_HULL) o GSYM);
    DISCH_THEN (C INTRO_TAC [`p`]);
    DISCH_THEN SUBST1_TAC;
    FIRST_X_ASSUM_ST `DIFF` MP_TAC;
    BY(SET_TAC[]);
  TYPIFY `aff_dim {a,b,p} = &2` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[COLLINEAR_AFF_DIM];
    INTRO_TAC AFF_DIM_2 [`a`;`b`];
    ASM_REWRITE_TAC[];
    INTRO_TAC AFF_DIM_INSERT [`p`;`{a,b}`];
    ASM_REWRITE_TAC[GSYM Sphere.aff];
    TYPIFY `{p,a,b} = {a,b,p}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(INT_ARITH_TAC);
  INTRO_TAC AFF_DIM_EQ_AFFINE_HULL [`{a,b,p}`;`affine hull S`];
  ANTS_TAC;
    CONJ_TAC;
      MATCH_MP_TAC SUBSET_TRANS;
      TYPIFY `S` EXISTS_TAC;
      CONJ2_TAC;
        BY(REWRITE_TAC[HULL_SUBSET]);
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
    INTRO_TAC COPLANAR_IMP_AFF_DIM [`S`];
    ASM_REWRITE_TAC[];
    BY(REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
  REWRITE_TAC[Planarity.AFFINE_HULL_AFFINE_EQ];
  DISCH_TAC;
  TYPIFY `x IN affine hull {a,b,p}` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[HULL_SUBSET;SUBSET;IN]);
  REPEAT (FIRST_X_ASSUM_ST `p IN aff_ge {a,b} {c,d}` MP_TAC);
  REPEAT (GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2);
  CONJ_TAC;
    FIRST_X_ASSUM_ST `~coplanar U` MP_TAC;
    TYPIFY `{a,b,c,d} = {a,c,b,d}` ((C SUBGOAL_THEN SUBST1_TAC));
      BY(SET_TAC[]);
    BY(MESON_TAC[Planarity.notcoplanar_disjoints]);
  GMATCH_SIMP_TAC AFF_GE_2_1;
  CONJ_TAC;
    BY(ASM_MESON_TAC[Fan.th3a]);
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM_ST `affine` MP_TAC;
  REWRITE_TAC[AFFINE_HULL_3];
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  GEXISTL_TAC [`u`;`v`;`w`];
  CONJ2_TAC;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM MP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `(t1' % a + t2' % b + t3' % c + t4' % d =  u % a + v % b + w % (t1 % a + t2 % b + t3 % c + t4 % d)) <=> (t1' - w * t1 - u) % a + (t2' - w * t2 - v) % b + (t3' - w * t3) % c + (t4' - w * t4) % d = vec 0` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(VECTOR_ARITH_TAC);
  DISCH_TAC;
  TYPIFY `CARD {a,b,c,d} = 4` ((C SUBGOAL_THEN ASSUME_TAC));
    MATCH_MP_TAC Collect_geom2.NOT_COPLANAR_IMP_CARD4;
    GMATCH_SIMP_TAC (GSYM coplanar_eq_coplanar_alt);
    REWRITE_TAC[DIMINDEX_3];
    ASM_REWRITE_TAC[];
    BY(ARITH_TAC);
  TYPIFY `~affine_dependent {a,b,c,d}` ((C SUBGOAL_THEN ASSUME_TAC));
    DISCH_TAC;
    FIRST_X_ASSUM (MP_TAC o (MATCH_MP Njiutiu.AFF_DEPENDENT_AFF_DIM_4));
    BY(ASM_MESON_TAC[Rogers.AFF_DIM_LE_2_IMP_COPLANAR]);
  INTRO_TAC AFFINE_DEPENDENT_EXPLICIT_4 [`a`;`b`;`c`;`d`;`t1' - w * t1 - u`;`t2' - w * t2 - v`;`t3' - w * t3`;`t4' - w * t4`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);
  REWRITE_TAC[arith `a - b = &0 <=> a = b`];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `&0 <= w * t3 /\ &0 <= w * t4` ((C SUBGOAL_THEN MP_TAC));
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[Misc_defs_and_lemmas.REAL_MUL_NN];
  ASM_SIMP_TAC[arith `&0 <= t ==> (t <= &0 <=> t = &0)`];
  ENOUGH_TO_SHOW_TAC `t3 = &0 /\ t4 = &0 ==> F`;
    BY(REAL_ARITH_TAC);
  REPEAT WEAK_STRIP_TAC;
  REPEAT (FIRST_X_ASSUM_ST `%` MP_TAC);
  ASM_REWRITE_TAC[];
  TYPIFY `t1 % a + t2 % b + &0 % c + &0 % d = t1 % a + t2 % b` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM_ST `DIFF` MP_TAC;
  REWRITE_TAC[DIFF;AFFINE_HULL_2;IN_ELIM_THM;NOT_EXISTS_THM];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`t1`;`t2`]);
  REWRITE_TAC[];
  CONJ_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let CONVEX_PLANE_INTER = 
prove_by_refinement(
  `!(a:real^A) b p q.  ~(a = b) /\ DISJOINT {a,b} {p} /\ q IN aff_gt {a,b} {p} ==>
    (?c. c IN aff_gt {a,b} {p} /\
      c IN convex hull {a,b,p} INTER convex hull {a,b,q})`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM_ST `IN` MP_TAC;
  (GMATCH_SIMP_TAC AFF_GT_2_1);
  ASM_REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  ABBREV_TAC `(r:real->real^A) t = (&1 - t) % ((&1/ &2) % a + (&1/ &2) % b) + t % p`;
  TYPIFY `!t. &0 <= t /\ t <= &1 ==> r t IN convex hull {a,b,p}` ((C SUBGOAL_THEN ASSUME_TAC));
    REPEAT WEAK_STRIP_TAC;
    REWRITE_TAC[CONVEX_HULL_3;IN_ELIM_THM];
    GEXISTL_TAC [`(&1 -t) / &2`;`(&1- t)/ &2`;`t`];
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    GOAL_TERM (fun w -> (FIRST_X_ASSUM (SUBST1_TAC o GSYM o (ISPEC ( env w `t`)))));
    BY(VECTOR_ARITH_TAC);
  TYPIFY `?t. &0 < t /\ t <= &1 /\ r t IN convex hull {a,b,q}` ENOUGH_TO_SHOW_TAC;
    REPEAT WEAK_STRIP_TAC;
    TYPIFY `r t` EXISTS_TAC;
    CONJ_TAC;
      GEXISTL_TAC [`(&1 - t) / &2 `;`(&1 - t)/ &2`;`t`];
      ASM_REWRITE_TAC[];
      CONJ_TAC;
        BY(REAL_ARITH_TAC);
      GOAL_TERM (fun w -> (FIRST_X_ASSUM (SUBST1_TAC o GSYM o (ISPEC ( env w `t`)))));
      BY(VECTOR_ARITH_TAC);
    REWRITE_TAC[IN_INTER];
    ASM_REWRITE_TAC[];
    REWRITE_TAC[CONVEX_HULL_3];
    REWRITE_TAC[IN_ELIM_THM];
    GEXISTL_TAC [`(&1 - t) / &2 `;`(&1 - t)/ &2`;`t`];
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    GOAL_TERM (fun w -> (FIRST_X_ASSUM (SUBST1_TAC o GSYM o (ISPEC ( env w `t`)))));
    BY(VECTOR_ARITH_TAC);
  REWRITE_TAC[CONVEX_HULL_3;IN_ELIM_THM];
  ASM_REWRITE_TAC[];
  ABBREV_TAC `eps = inv (abs t1 + abs t2 + &2 * abs t3 + &2 * abs (t1 - t2 - &1) + &2 * abs(t2 - t1 - &1) + &10)`;
  EXISTS_TAC `&2 * eps * t3`;
  CONJ_TAC;
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    REWRITE_TAC[ REAL_OF_NUM_LT];
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      EXPAND_TAC "eps";
      GMATCH_SIMP_TAC REAL_LT_INV;
      BY(REAL_ARITH_TAC);
    BY(ARITH_TAC);
  CONJ_TAC;
    EXPAND_TAC "eps";
    REWRITE_TAC[arith `a * inv b * c = (a * c)/ b`];
    GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    BY(REAL_ARITH_TAC);
  TYPIFY `&0 <= eps` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "eps";
    REWRITE_TAC[REAL_LE_INV_EQ];
    BY(REAL_ARITH_TAC);
  GEXISTL_TAC [`&1/ &2 + eps * ( (t2 - t1) - &1 )`;`&1/ &2 + eps * ( (t1 - t2) - &1 )`;`&2 * eps`];
  TYPIFY `(&1 / &2 + eps * (t2 - t1 - &1)) +  (&1 / &2 + eps * (t1 - t2 - &1)) +  &2 * eps =  &1` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(REAL_ARITH_TAC);
  TYPIFY `r (&2 * eps * t3) = (&1 / &2 + eps * (t2 - t1 - &1)) % a + (&1 / &2 + eps * (t1 - t2 - &1)) % b + (&2 * eps) % (t1 % a + t2 % b + t3 % p)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    GOAL_TERM (fun w -> (FIRST_X_ASSUM (SUBST1_TAC o GSYM o (ISPEC ( env w `&2 * eps * t3`)))));
    FIRST_X_ASSUM_ST `t1 + t2 + t3 = &1` ((unlist REWRITE_TAC) o (REWRITE_RULE[arith `t1 + t2 + t3 = &1 <=> t3 = &1 - t2 - t1`]));
    BY(VECTOR_ARITH_TAC);
  TYPIFY `&0 <= &2 * eps` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    GMATCH_SIMP_TAC REAL_LE_MUL;
    BY(ASM_REWRITE_TAC[arith `&0 <= &2`]);
  REPEAT (GMATCH_SIMP_TAC (arith `abs(a * b) <= &1 / &2 ==> &0 <= &1/ &2 + a * b`));
  REWRITE_TAC[REAL_ABS_MUL];
  ASM_SIMP_TAC[arith `&0 <= eps ==> abs (eps) = eps`];
  GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  REWRITE_TAC[ REAL_OF_NUM_LT];
  EXPAND_TAC "eps";
  GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  REWRITE_TAC[ REAL_OF_NUM_LT];
  REWRITE_TAC[arith `0 < 2`];
  REWRITE_TAC[arith `(inv a * b) * d <= c <=> (b * d) / a <= c`];
  GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
  GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let CONVEX_R3_INTER = 
prove_by_refinement(
  `!(a:real^3) b c p q. ~coplanar {a,b,c,p} /\ q IN aff_gt {a,b,c} {p} ==>
    (?d. ~coplanar {a,b,c,d} /\ d IN convex hull {a,b,c,p} INTER convex hull {a,b,c,q})`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `DISJOINT {a,b,c} {p}` ((C SUBGOAL_THEN ASSUME_TAC));
    BY(ASM_MESON_TAC[Planarity.notcoplanar_disjoints]);
  FIRST_X_ASSUM_ST `IN` MP_TAC;
  GMATCH_SIMP_TAC AFF_GT_3_1;
  ASM_REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  ABBREV_TAC `(r:real^3)  = (&1 / &3) % a + (&1/ &3 ) % b + (&1 / &3) % c`;
  TYPIFY `?t. ~coplanar {a,b,c, (&1 - t) % r + t % q} /\ (&1 - t) % r + t % q IN convex hull{a,b,c,p} INTER convex hull {a,b,c,q}` ENOUGH_TO_SHOW_TAC;
    BY(MESON_TAC[]);
  REWRITE_TAC[IN_INTER];
  REWRITE_TAC[Marchal_cells_2_new.CONVEX_HULL_4];
  ASM_REWRITE_TAC[IN_ELIM_THM];
  EXPAND_TAC "r";
  TYPIFY `?s. s <  &1 /\ &0 < s /\ &0 < (&1 - s)/ &3 + s * t1 /\ &0 < (&1 -s)/ &3 + s * t2 /\ &0 < (&1 - s)/ &3 + s * t3 ` (C SUBGOAL_THEN MP_TAC);
    EXISTS_TAC (`inv (&4 + &3 * abs t1 + &3 * abs t2 + &3 * abs t3)`);
    TYPIFY `&0 < &4 + &3 * abs t1 + &3 * abs t2 + &3 * abs t3` ((C SUBGOAL_THEN ASSUME_TAC));
      BY(REAL_ARITH_TAC);
    CONJ_TAC;
      REWRITE_TAC[arith `inv x = &1 / x`];
      ASM_SIMP_TAC[REAL_LT_LDIV_EQ];
      BY(REAL_ARITH_TAC);
    CONJ_TAC;
      GMATCH_SIMP_TAC REAL_LT_INV;
      BY(ASM_REWRITE_TAC[]);
    REWRITE_TAC[arith `&0 < (&1 - inv x)/ &3 + inv x * t <=> (&1 - &3 * t)/x < &1`];
    (ASM_SIMP_TAC[REAL_LT_LDIV_EQ]);
    BY(REAL_ARITH_TAC);
  REPEAT WEAK_STRIP_TAC;
  EXISTS_TAC `s:real`;
  CONJ2_TAC;
    CONJ_TAC;
      GEXISTL_TAC [`(&1 - s)/ &3 + s * t1`;`(&1- s)/ &3 + s * t2`;`(&1- s)/ &3 + s * t3`;`s * t4`];
      ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
      GMATCH_SIMP_TAC REAL_LE_MUL;
      ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
      FIRST_X_ASSUM_ST `t1 + t2 + t3 + t4 = &1` (SUBST1_TAC o (REWRITE_RULE[arith `t1 + t2 + t3 + t4 = &1 <=> t4 = &1 - t1 - t2 - t3`]));
      CONJ_TAC;
        BY(REAL_ARITH_TAC);
      EXPAND_TAC "r";
      BY(VECTOR_ARITH_TAC);
    GEXISTL_TAC [`(&1 - s)/ &3 `;`(&1- s)/ &3 `;`(&1- s)/ &3`;`s `];
    ASM_SIMP_TAC[arith `s < &1 ==> &0 <= (&1 - s) / &3`];
    ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    FIRST_X_ASSUM_ST `t1 + t2 + t3 + t4 = &1` (SUBST1_TAC o (REWRITE_RULE[arith `t1 + t2 + t3 + t4 = &1 <=> t4 = &1 - t1 - t2 - t3`]));
    EXPAND_TAC "r";
    BY(VECTOR_ARITH_TAC);
  (COMMENT "last goal, coplanarity");
  FIRST_X_ASSUM_ST `coplanar` MP_TAC;
  REWRITE_TAC[CHI_MSB_COPLANAR];
  TYPIFY `((&1 - s) % (&1 / &3 % a + &1 / &3 % b + &1 / &3 % c) +         s % (t1 % a + t2 % b + t3 % c + t4 % p)) = ((&1 - s)/ &3 + s * t1) % a + ((&1 - s)/ &3  + s * t2) % b + ((&1 - s) / &3 + s * t3) % c + (s * t4) % p` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  DISCH_TAC;
  GMATCH_SIMP_TAC chi_msb_additive_d;
  CONJ_TAC;
    FIRST_X_ASSUM_ST `x = &1` MP_TAC;
    BY(CONV_TAC REAL_RING);
  REWRITE_TAC[REAL_ENTIRE];
  ASM_REWRITE_TAC[];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let MCELL2_CONVEX = 
prove_by_refinement(
  `!V vl. saturated V /\ packing V /\ barV V 3 vl ==> convex (mcell2 V vl)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Pack_defs.mcell2];
  REPEAT WEAK_STRIP_TAC;
  COND_CASES_TAC;
    REWRITE_TAC[LET_DEF;LET_END_DEF];
    MATCH_MP_TAC CONVEX_INTER;
    GMATCH_SIMP_TAC CONVEX_INTER;
    REWRITE_TAC[CONVEX_AFF_GE];
    TYPIFY `&0 <= hl (truncate_simplex 1 vl) / sqrt (&2)` ENOUGH_TO_SHOW_TAC;
      BY(MESON_TAC[Marchal_cells_2_new.CONVEX_RCONE_GE]);
    GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
    REWRITE_TAC[arith `&0 * x = &0`];
    GMATCH_SIMP_TAC REAL_LT_RSQRT;
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    BY(ASM_MESON_TAC[Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;arith `&0 < x ==> &0 <= x`]);
  BY(REWRITE_TAC[CONVEX_EMPTY])
  ]);;
  (* }}} *)

let MCELL_CONVEX = 
prove_by_refinement(
  `!V vl k. saturated V /\ packing V /\ barV V 3 vl /\ 2 <= k ==> convex (mcell k V vl)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Pack_defs.mcell];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(k=0) /\ ~(k=1)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
  ASM_REWRITE_TAC[];
  REPEAT COND_CASES_TAC;
      BY(ASM_MESON_TAC[MCELL2_CONVEX]);
    REWRITE_TAC[Pack_defs.mcell3];
    COND_CASES_TAC;
      BY(REWRITE_TAC[CONVEX_CONVEX_HULL]);
    BY(REWRITE_TAC[CONVEX_EMPTY]);
  REWRITE_TAC[Pack_defs.mcell4];
  COND_CASES_TAC;
    BY(REWRITE_TAC[CONVEX_CONVEX_HULL]);
  BY(REWRITE_TAC[CONVEX_EMPTY])
  ]);;
  (* }}} *)

let CHI_MSB_AFF_GT_0 = 
prove_by_refinement(
  `!a b c q q'. ~coplanar {a,b,c,q} /\
    &0 < chi_msb [a;b;c] q /\ &0 < chi_msb [a;b;c] q' ==>
    (q' IN aff_gt {a,b,c} {q})`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC AFF_DIM_EQ_AFFINE_HULL [`{a,b,c, q}`;`(:real^3)`];
  REWRITE_TAC[AFFINE_HULL_UNIV];
  ANTS_TAC;
    CONJ_TAC;
      BY(SET_TAC[]);
    REWRITE_TAC[AFF_DIM_UNIV;DIMINDEX_3];
    ENOUGH_TO_SHOW_TAC `~(aff_dim {a,b,c, (q:real^3)} <= &2)`;
      BY(INT_ARITH_TAC);
    BY(ASM_MESON_TAC[Rogers.AFF_DIM_LE_2_IMP_COPLANAR]);
  REWRITE_TAC[EXTENSION;IN_UNIV];
  DISCH_THEN (C INTRO_TAC [`q'`]);
  REWRITE_TAC[Collect_geom2.AFFINE_HULL_4];
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM_ST `chi_msb` MP_TAC;
  ASM_REWRITE_TAC[];
  INTRO_TAC chi_msb_additive_d [`a`;`b`;`c`;`q`;`u`;`v`;`w`;`z`];
  ASM_REWRITE_TAC[];
  DISCH_THEN SUBST1_TAC;
  ASM_SIMP_TAC[Real_ext.REAL_PROP_POS_RMUL];
  DISCH_TAC;
  GMATCH_SIMP_TAC AFF_GT_3_1;
  REWRITE_TAC[IN_ELIM_THM];
  CONJ2_TAC;
    BY(ASM_MESON_TAC[]);
  BY(ASM_MESON_TAC[Planarity.notcoplanar_disjoints])
  ]);;
  (* }}} *)

let CHI_MSB_POS2 = 
prove_by_refinement(
  `!a b c d p. DISJOINT {a,b} {c} /\  d IN aff_gt {a,b} {c} ==> re_eqvl (chi_msb [a;b;d] p) (chi_msb[a;b;c] p)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[Trigonometry2.re_eqvl];
  ASM_SIMP_TAC[AFF_GT_2_1];
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  EXISTS_TAC `t3:real`;
  ASM_REWRITE_TAC[];
  ONCE_REWRITE_TAC[chi_msb_swap_23];
  TYPIFY `t1 % a + t2 % b + t3 % c = t1 % a + t2 % b + (&0) % p + t3 % c` (C SUBGOAL_THEN SUBST1_TAC);
    BY(VECTOR_ARITH_TAC);
  GMATCH_SIMP_TAC chi_msb_additive_d;
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let MCELL_ARG_REDUCE = 
prove_by_refinement(
  `!V ul i. (?j. j <= 4 /\ mcell i V ul = mcell j V ul)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ASM_CASES_TAC `i <= 4`;
    EXISTS_TAC `i:num`;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~(i=0) /\ ~(i=1) /\ ~(i=2) /\ ~(i = 3) /\ ~(i=4)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
  EXISTS_TAC `4`;
  CONJ_TAC;
    BY(ARITH_TAC);
  REWRITE_TAC[Pack_defs.mcell];
  BY(ASM_REWRITE_TAC[arith `~(4 =0) /\ ~(4 = 1) /\ ~(4 = 2) /\ ~(4 =3)`])
  ]);;
  (* }}} *)

let AJRIPQN_0 = 
prove_by_refinement(
  `!V ul vl i j.
    saturated V /\
            packing V /\
            barV V 3 ul /\
            barV V 3 vl /\
            ~NULLSET (mcell i V ul INTER mcell j V vl)
            ==>  mcell j V vl = mcell i V ul 
`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC MCELL_ARG_REDUCE [`V`;`ul`;`i`];
  INTRO_TAC MCELL_ARG_REDUCE [`V`;`vl`;`j`];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Ajripqn.AJRIPQN [`V`;`ul`;`vl`;`j''`;`j'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    BY(ASM_MESON_TAC[]);
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let CFFONNL = 
prove_by_refinement(
  `!V ul X.  packing V /\ saturated V /\ leaf V ul /\ X IN mcell_set V /\
   {EL 0 ul,EL 1 ul} IN edgeX V X /\
     ~(X INTER cc_A0 ul = {}) /\ ~(X = cc_cell V ul) ==> (X = cc_cell V [EL 1 ul;EL 0 ul;EL 2 ul])`,

  (* {{{ proof *)
  [
  REWRITE_TAC[cc_A0;Pack_defs.mcell_set;IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~NULLSET X` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[RIJRIED;EXTENSION;NOT_IN_EMPTY]);
  INTRO_TAC COPLANAR_IMP_NEGLIGIBLE [`X`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC [leaf;Sphere.BARV;IN;arith `3 = 2 + 1`]);
  TYPIFY `[EL 0 ul;EL 1 ul; EL 2 ul] = ul` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[LENGTH3]);
  TYPIFY `{EL 0 ul,EL 1 ul, EL 2 ul} = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[set_of_list3]);
  INTRO_TAC AFF_GT_SUBSET_AFFINE_HULL [`{EL 0 ul, EL 1 ul}`;`{EL 2 ul}`];
  TYPIFY `{EL 0 ul, EL 1 ul} UNION {EL 2 ul} = {EL 0 ul,EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `?p. p IN X INTER aff_gt {EL 0 ul, EL 1 ul} {EL 2 ul}` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM_ST `INTER` MP_TAC;
    BY(SET_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(X SUBSET affine hull set_of_list ul)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM (SUBST1_TAC o GSYM);
    DISCH_TAC;
    INTRO_TAC COPLANAR_3 [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`];
    REWRITE_TAC[];
    ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR];
    BY(ASM_MESON_TAC[COPLANAR_SUBSET]);
  COMMENT "back to 1";
  TYPIFY `aff_dim (set_of_list ul) = &2` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Rogers.MHFTTZN1;
    BY(ASM_MESON_TAC[IN;leaf]);
  TYPIFY `?q. q IN X DIFF affine hull set_of_list ul` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM_ST `SUBSET` MP_TAC;
    BY(SET_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  PROOF_BY_CONTR_TAC;
  TYPIFY `~ (chi_msb ul q = &0)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `[]` (SUBST1_TAC o GSYM);
    REWRITE_TAC[GSYM CHI_MSB_COPLANAR];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `DIFF` MP_TAC;
    REWRITE_TAC[IN_DIFF];
    REPEAT WEAK_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[];
    MATCH_MP_TAC COPLANAR_INSERT;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `coplanar` MP_TAC;
    MATCH_MP_TAC (TAUT (`a = b ==> (a ==> b)`));
    AP_TERM_TAC;
    FIRST_X_ASSUM_ST `{}` (SUBST1_TAC o GSYM);
    BY(SET_TAC[]);
  TYPIFY `{EL 0 ul, EL 1 ul} SUBSET X` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Marchal_cells_3.EDGEX_SUBSET_MCELL;
    TYPIFY `V` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    CONJ2_TAC;
      BY(ASM_MESON_TAC[IN]);
    REWRITE_TAC[Pack_defs.mcell_set];
    REWRITE_TAC[IN_ELIM_THM];
    BY(ASM_MESON_TAC[]);
  COMMENT "redo here";
  TYPIFY `2 <= i` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[arith `2 <= i <=> ~(i <= 1)`];
    REPEAT WEAK_STRIP_TAC;
    INTRO_TAC EDGE_IMP_K2 [`V`;`ul'`;`i`];
    ASM_REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
    DISCH_THEN MP_TAC;
    ANTS_TAC;
      BY(ASM_MESON_TAC[IN]);
    BY(ASM_MESON_TAC[]);
  COMMENT "next show convex SUBSET X";
  TYPIFY `convex hull {EL 0 ul,EL 1 ul,p,q} SUBSET convex hull X` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET;
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  FIRST_X_ASSUM MP_TAC;
  TYPIFY `convex hull X = X` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[CONVEX_HULL_EQ];
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC MCELL_CONVEX;
    BY(ASM_MESON_TAC[IN]);
  DISCH_TAC;
  COMMENT "2.  create Y ";
  ABBREV_TAC `(wl) = (if (&0 < chi_msb ul q ) then ul else [EL 1 ul; EL 0 ul; EL 2 ul])`;
  TYPIFY `&0 < chi_msb wl q` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "wl";
    COND_CASES_TAC;
    ONCE_REWRITE_TAC[chi_msb_swap_01];
    MATCH_MP_TAC(arith `~(x = &0) /\ ~(&0 < x) ==> &0 < -- x`);
    BY(ASM_MESON_TAC[]);
  ABBREV_TAC `k = cc_ke V wl`;
  ABBREV_TAC `Y = cc_cell V (wl)`;
  TYPIFY `EL 2 wl = EL 2 ul` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "wl";
    COND_CASES_TAC;
      BY(REWRITE_TAC[]);
    BY(REWRITE_TAC[EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`]);
  TYPIFY `set_of_list wl = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "wl";
    COND_CASES_TAC;
      BY(REWRITE_TAC[]);
    FIRST_X_ASSUM_ST `x = set_of_list ul` (SUBST1_TAC o GSYM);
    GMATCH_SIMP_TAC set_of_list3;
    REWRITE_TAC[LENGTH;arith `SUC (SUC(SUC 0)) = 3`];
    REWRITE_TAC[EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`];
    BY(SET_TAC[]);
  TYPIFY `leaf V wl` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "wl";
    COND_CASES_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(ASM_MESON_TAC[ ZASUVOR]);
  COMMENT "points in Y";
  TYPIFY `LENGTH wl = 3` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "wl";
    COND_CASES_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(REWRITE_TAC[LENGTH;arith `SUC (SUC(SUC 0)) = 3`]);
  TYPIFY `{EL 0 ul,EL 1 ul, EL 2 ul} SUBSET Y` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "Y";
    GMATCH_SIMP_TAC CC_CELL34;
    ABBREV_TAC `pp = (if k=3 then mxi V (cc_uh V ( wl))        else EL 3 (cc_uh V  wl))`;
    TYPIFY `pp` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    TYPIFY `set_of_list wl SUBSET {EL 0 wl, EL 1 wl, EL 2 ul, pp}` ENOUGH_TO_SHOW_TAC;
      BY(ASM_MESON_TAC[Ldurdpn.SUBSET_P_HULL;SUBSET_TRANS]);
    FIRST_X_ASSUM_ST `x = EL 2 ul` (SUBST1_TAC o GSYM);
    GMATCH_SIMP_TAC set_of_list3;
    CONJ_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(SET_TAC[]);
  COMMENT "3.";
  TYPIFY `EL 2 ul IN Y INTER aff_gt {EL 0 ul, EL 1 ul} {EL 2 ul}` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[IN_INTER];
    CONJ_TAC;
      FIRST_X_ASSUM MP_TAC;
      BY(SET_TAC[]);
    BY((MESON_TAC[Local_lemmas.X_IN_AFF_GT_X]));
  COMMENT "now pos half space point";
  TYPIFY `?q'. &0 < chi_msb wl q' /\ q' IN Y` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC CELL_NN [`V`;`wl`];
    ASM_REWRITE_TAC[];
    REPEAT WEAK_STRIP_TAC;
    ABBREV_TAC `pp  =         (if cc_ke V wl = 3 then mxi V (cc_uh V wl) else EL 3 (cc_uh V wl))`;
    INTRO_TAC CC_CELL34 [`V`;`wl`;`pp`];
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    TYPIFY `pp` EXISTS_TAC;
    CONJ2_TAC;
      MATCH_MP_TAC HULL_INC;
      BY(SET_TAC[]);
    EXPAND_TAC "pp";
    COND_CASES_TAC;
      BY(ASM_MESON_TAC[CELL3_NONDEG]);
    MATCH_MP_TAC K4_CHI_MSB_POS;
    BY(ASM_MESON_TAC[CC_KE_34]);
  FIRST_X_ASSUM MP_TAC;
  WEAK_STRIP_TAC;
  COMMENT "now common point in the plane";
  INTRO_TAC GBEWYFX [`V`;`ul`];
  ASM_REWRITE_TAC[];
  PROOF_BY_CONTR_TAC;
  INTRO_TAC Fan.th3a [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  INTRO_TAC CONVEX_PLANE_INTER [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`p`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      FIRST_X_ASSUM_ST `edgeX` MP_TAC;
      REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
      BY(SET_TAC[]);
    REPEAT (FIRST_X_ASSUM_ST `p IN x INTER  y` MP_TAC);
    BY(SET_TAC[]);
  (REPEAT WEAK_STRIP_TAC);
  TYPIFY `{EL 0 wl,EL 1 wl} = {EL 0 ul,EL 1 ul}` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "wl";
    COND_CASES_TAC;
      BY(REWRITE_TAC[]);
    REWRITE_TAC[EL;HD;TL;arith `1  = SUC 0`];
    BY(SET_TAC[]);
  TYPIFY `[EL 0 wl;EL 1 wl; EL 2 wl] = wl` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[LENGTH3]);
  INTRO_TAC CHI_MSB_POS2 [`EL 0 wl`;`EL 1 wl`;`EL 2 wl`;`c`;`q`];
  INTRO_TAC CHI_MSB_POS2 [`EL 0 wl`;`EL 1 wl`;`EL 2 wl`;`c`;`q'`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REWRITE_TAC[Trigonometry2.re_eqvl];
  WEAK_STRIP_TAC;
  DISCH_THEN MP_TAC;
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  WEAK_STRIP_TAC;
  INTRO_TAC CONVEX_R3_INTER [`EL 0 ul`;`EL 1 ul`;`c`;`q`;`q'`];
  ANTS_TAC;
    TYPIFY `{EL 0 ul, EL 1 ul, c, q} = {EL 0 wl, EL 1 wl, c,q}` (C SUBGOAL_THEN ASSUME_TAC);
      FIRST_X_ASSUM_ST `{EL 0 wl, EL 1 wl} = {EL 0 ul, EL 1 ul}` MP_TAC;
      BY(SET_TAC[]);
    SUBCONJ_TAC;
      ASM_REWRITE_TAC[];
      REWRITE_TAC[CHI_MSB_COPLANAR];
      MATCH_MP_TAC (arith `&0 < x ==> ~(x = &0)`);
      FIRST_X_ASSUM_ST `*` SUBST1_TAC;
      GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
      BY(ASM_REWRITE_TAC[]);
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    TYPIFY ` {EL 0 ul, EL 1 ul, c} =  {EL 0 wl, EL 1 wl, c}` (C SUBGOAL_THEN SUBST1_TAC);
      FIRST_X_ASSUM_ST `{EL 0 wl, EL 1 wl} = {EL 0 ul, EL 1 ul}` MP_TAC;
      BY(SET_TAC[]);
    MATCH_MP_TAC CHI_MSB_AFF_GT_0;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    BY(ASM_REWRITE_TAC[]);
  WEAK_STRIP_TAC;
  (COMMENT "S. back to 1. Show u0 u1 c d in X INTER Y");
  TYPIFY `convex hull X = X /\ convex hull Y = Y` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_REWRITE_TAC[CONVEX_HULL_EQ];
    EXPAND_TAC "Y";
    REWRITE_TAC[cc_cell];
    REPEAT (GMATCH_SIMP_TAC MCELL_CONVEX);
    ASM_SIMP_TAC[CC_KE_34;arith `k= 3 \/ k = 4 ==> 2 <= k`];
    CONJ2_TAC;
      REPEAT (FIRST_X_ASSUM_ST `barV` MP_TAC);
      BY(REWRITE_TAC[IN]);
    BY(ASM_MESON_TAC[IN;cc_uh]);
  COMMENT "S. X";
  TYPIFY `convex hull {EL 0 ul, EL 1 ul, c, q} SUBSET convex hull X` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET;
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
    FIRST_X_ASSUM_ST `convex hull {EL 0 ul, EL 1 ul, p, q} SUBSET X` MP_TAC;
    REPEAT (FIRST_X_ASSUM_ST `INTER` MP_TAC);
    REPEAT (FIRST_X_ASSUM kill);
    REWRITE_TAC[IN_INTER];
    INTRO_TAC Marchal_cells.CONVEX_HULL_SUBSET [`{EL 0 ul,EL 1 ul,p}`;`{EL 0 ul,EL 1 ul,p,q}`];
    ANTS_TAC;
      BY(SET_TAC[]);
    REWRITE_TAC[SUBSET];
    TYPIFY `!y. y = EL 0 ul  \/ y = EL 1 ul ==> y IN {EL 0 ul,EL 1 ul,p}` (C SUBGOAL_THEN MP_TAC);
      BY(SET_TAC[]);
    TYPIFY `q IN {EL 0 ul,EL 1 ul,p,q}` (C SUBGOAL_THEN MP_TAC);
      BY(SET_TAC[]);
    BY(MESON_TAC[HULL_INC]);
  FIRST_ASSUM (unlist REWRITE_TAC);
  DISCH_TAC;
  COMMENT "S. now Y";
  TYPIFY `convex hull {EL 0 ul,EL 1 ul,c,q'} SUBSET convex hull Y` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET;
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
    GEN_TAC;
    TYPIFY `q' IN Y` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM_ST `{EL 0 ul, EL 1 ul, EL 2 ul} SUBSET Y` (MP_TAC o (MATCH_MP Marchal_cells.CONVEX_HULL_SUBSET));
    TYPIFY `{EL 0 ul, EL 1 ul, c} SUBSET convex hull {EL 0 ul, EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN MP_TAC);
      REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `INTER` MP_TAC);
      REWRITE_TAC[IN_INTER;SUBSET;IN_INSERT;NOT_IN_EMPTY];
      TYPIFY `EL 0 ul IN {EL 0 ul,EL 1 ul,EL 2 ul} /\ EL 1 ul IN {EL 0 ul,EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN MP_TAC);
        BY(SET_TAC[]);
      BY(MESON_TAC[HULL_INC]);
    FIRST_X_ASSUM_ST `/\` (unlist REWRITE_TAC);
    BY(SET_TAC[]);
  FIRST_X_ASSUM_ST `/\` (unlist REWRITE_TAC);
  DISCH_TAC;
  COMMENT "S. now X INTER Y";
  TYPIFY `convex hull {EL 0 ul,EL 1 ul, c,d} SUBSET X INTER Y` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SUBSET_TRANS;
    TYPIFY `convex hull {EL 0 ul, EL 1 ul, c, q} INTER  convex hull {EL 0 ul, EL 1 ul, c, q'}` EXISTS_TAC;
    CONJ2_TAC;
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
    REWRITE_TAC[SUBSET_INTER];
    CONJ_TAC;
      INTRO_TAC Marchal_cells.CONVEX_HULL_SUBSET [`{EL 0 ul, EL 1 ul, c, d}`;` convex hull {EL 0 ul, EL 1 ul, c, q}`];
      REWRITE_TAC[HULL_HULL];
      DISCH_THEN MATCH_MP_TAC;
      TYPIFY `d IN convex hull  {EL 0 ul, EL 1 ul, c, q} /\ {EL 0 ul, EL 1 ul, c} SUBSET convex hull {EL 0 ul, EL 1 ul, c, q}` ENOUGH_TO_SHOW_TAC;
        BY(SET_TAC[]);
      CONJ_TAC;
        FIRST_X_ASSUM_ST `INTER` MP_TAC;
        BY(SET_TAC[]);
      REWRITE_TAC[SUBSET];
      BY(MESON_TAC[HULL_INC;MESON[IN_INSERT;NOT_IN_EMPTY] `!x. x IN {EL 0 ul,EL 1 ul,c} ==> x IN {EL 0 ul, EL 1 ul,c,q}`]);
    INTRO_TAC Marchal_cells.CONVEX_HULL_SUBSET [`{EL 0 ul, EL 1 ul, c, d}`;` convex hull {EL 0 ul, EL 1 ul, c, q'}`];
    REWRITE_TAC[HULL_HULL];
    DISCH_THEN MATCH_MP_TAC;
    TYPIFY `d IN convex hull  {EL 0 ul, EL 1 ul, c, q'} /\ {EL 0 ul, EL 1 ul, c} SUBSET convex hull {EL 0 ul, EL 1 ul, c, q'}` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    CONJ_TAC;
      FIRST_X_ASSUM_ST `INTER` MP_TAC;
      BY(SET_TAC[]);
    REWRITE_TAC[SUBSET];
    BY(MESON_TAC[HULL_INC;MESON[IN_INSERT;NOT_IN_EMPTY] `!x. x IN {EL 0 ul,EL 1 ul,c} ==> x IN {EL 0 ul, EL 1 ul,c,q'}`]);
  COMMENT "T. back to 1. now show X = Y ";
  TYPIFY `X = Y` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC AJRIPQN_0 [`V`;`ul'`;`cc_uh V wl`;`i`;`cc_ke V wl`];
    ASM_REWRITE_TAC[GSYM cc_cell];
    DISCH_THEN (MATCH_MP_TAC o GSYM);
    CONJ_TAC;
      FIRST_X_ASSUM_ST `barV` MP_TAC;
      BY(REWRITE_TAC[IN]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[IN;cc_uh]);
    DISCH_TAC;
    TYPIFY `NULLSET (convex hull {EL 0 ul, EL 1 ul, c, d})` (C SUBGOAL_THEN ASSUME_TAC);
      MATCH_MP_TAC NEGLIGIBLE_SUBSET;
      TYPIFY `X INTER Y` EXISTS_TAC;
      FIRST_X_ASSUM_ST `convex` (unlist REWRITE_TAC);
      FIRST_X_ASSUM MP_TAC;
      BY(ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM_ST `coplanar` (MP_TAC o (MATCH_MP ZWVCBMN));
    REWRITE_TAC[];
    MATCH_MP_TAC (arith `x = &0 ==> ~(&0 < x)`);
    FIRST_X_ASSUM MP_TAC;
    BY(MESON_TAC[volume_props]);
  REPEAT (FIRST_X_ASSUM_ST `convex` kill);
  FIRST_X_ASSUM_ST `~(X = (Y:real^3->bool))` MP_TAC;
  REWRITE_TAC[];
  ENOUGH_TO_SHOW_TAC `cc_cell V wl = cc_cell V [EL 1 ul; EL 0 ul; EL 2 ul]`;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM_ST `COND` MP_TAC;
  DISCH_TAC;
  EXPAND_TAC "wl";
  COND_CASES_TAC;
    BY(ASM_MESON_TAC[]);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

let CC_CELL_IN_MCELL_SET = 
prove_by_refinement(
  `!V ul. saturated V /\ packing V /\ leaf V ul ==>
    cc_cell V ul IN mcell_set V`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[Pack_defs.mcell_set;IN_ELIM_THM];
  REWRITE_TAC[cc_cell];
  GEXISTL_TAC [`cc_ke V ul`;`cc_uh V ul`];
  REWRITE_TAC[];
  BY(ASM_MESON_TAC[cc_uh])
  ]);;
  (* }}} *)

let CARD4_ALL_DISTINCT = 
prove_by_refinement(
  `!(a:A) b c d. CARD {a,b,c,d}= 4 ==>
   ~(a = b) /\ ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d) /\ ~(c = d)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY ` {a,b,c,d} = {a,c,b,d} /\ {a,b,c,d}= {a,d,b,c} /\ {a,b,c,d} = {b,c,a,d} /\ {a,b,c,d} = {b,d,a,c} /\ {a,b,c,d} = {c,d,a,b}` (C SUBGOAL_THEN MP_TAC);
    BY(SET_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT THEN FIRST_X_ASSUM_ST `4` (SUBST1_TAC o GSYM) THEN (REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC)) THEN MESON_TAC[])
  ]);;
  (* }}} *)


let LENGTH4_SET2 = 
prove_by_refinement(
  `!(a:A) b c d e f. CARD {a,b,c,d} = 4 /\ set_of_list [a;b;c;d] = set_of_list [a;b;e;f] ==>
    ((e = c /\ (f = d)) \/ ((e = d) /\ (f = c))) `,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[set_of_list4_explicit];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM (MP_TAC o (MATCH_MP CARD4_ALL_DISTINCT));
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[EXTENSION;IN_INSERT;NOT_IN_EMPTY];
  REPEAT WEAK_STRIP_TAC;
  FIRST_ASSUM (C INTRO_TAC [`c`]);
  FIRST_ASSUM (C INTRO_TAC [`d`]);
  FIRST_ASSUM (C INTRO_TAC [`e`]);
  FIRST_X_ASSUM (C INTRO_TAC [`f`]);
  ASM_REWRITE_TAC[];
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let LENGTH4_SET2_SWAP01 = 
prove_by_refinement(
  `!(a:A) b c d e f. CARD {a,b,c,d} = 4 /\ set_of_list [a;b;c;d] = set_of_list [b;a;e;f] ==>
    ((e = c /\ (f = d)) \/ ((e = d) /\ (f = c))) `,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[set_of_list4_explicit];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM (MP_TAC o (MATCH_MP CARD4_ALL_DISTINCT));
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[EXTENSION;IN_INSERT;NOT_IN_EMPTY];
  REPEAT WEAK_STRIP_TAC;
  FIRST_ASSUM (C INTRO_TAC [`c`]);
  FIRST_ASSUM (C INTRO_TAC [`d`]);
  FIRST_ASSUM (C INTRO_TAC [`e`]);
  FIRST_X_ASSUM (C INTRO_TAC [`f`]);
  ASM_REWRITE_TAC[];
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let CC_CELL_NOT_COPLANAR = 
prove_by_refinement(
  `!V ul.    packing V /\
         saturated V /\
         leaf V ul ==> ~coplanar (cc_cell V ul)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[cc_cell];
  REWRITE_TAC[Pack_defs.mcell];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  INTRO_TAC CC_KE_34 [`V`;`ul`];
  DISCH_TAC;
  ABBREV_TAC `k = cc_ke V ul`;
  TYPIFY `~(k=0) /\ ~(k=1) /\ ~(k=2)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  FIRST_X_ASSUM_ST `\/` DISJ_CASES_TAC;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC MCELL3_NONPLANAR;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      BY(ASM_MESON_TAC[cc_uh;IN]);
    FIRST_X_ASSUM_ST `cc_ke` MP_TAC;
    REWRITE_TAC[cc_ke];
    COND_CASES_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    BY(ASM_MESON_TAC[cc_uh;leaf;IN;arith `~(x < sqrt2) ==> sqrt2 <= x`]);
  ASM_REWRITE_TAC[arith `~(4=3)`];
  MATCH_MP_TAC MCELL4_NONPLANAR;
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM_ST `cc_ke` MP_TAC;
  REWRITE_TAC[cc_ke];
  COND_CASES_TAC;
    BY(ASM_MESON_TAC[REWRITE_RULE[IN] cc_uh]);
  BY(ASM_REWRITE_TAC[arith `~(3=4)`])
  ]);;
  (* }}} *)

let CC_CELL_NOT_COPLANAR_EXTREME = 
prove_by_refinement(
  `!V ul pp.    packing V /\
         saturated V /\
         leaf V ul /\
         ((if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul)) =
         pp) ==> ~coplanar  {EL 0 ul, EL 1 ul, EL 2 ul,pp}`,

  (* {{{ proof *)
  [
  ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `coplanar (convex hull {EL 0 ul, EL 1 ul, EL 2 ul, pp})` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[COPLANAR_SUBSET;CONVEX_HULL_SUBSET_AFFINE_HULL]);
  INTRO_TAC CC_CELL34 [`V`;`ul`;`pp`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  BY(ASM_MESON_TAC[CC_CELL_NOT_COPLANAR])
  ]);;
  (* }}} *)

let CC_CELL_NOT_NULLSET = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul ==>
    ~NULLSET (cc_cell V ul)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `vol(cc_cell V ul) = &0` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[volume_props]);
  ABBREV_TAC `(p:real^3) = (if cc_ke V ul = 3  then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul))`;
  INTRO_TAC CC_CELL34 [`V`;`ul`;`p`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC ZWVCBMN [`EL 0 ul`;` EL 1 ul`;` EL 2 ul`;` p`];
  ANTS_TAC;
    MATCH_MP_TAC CC_CELL_NOT_COPLANAR_EXTREME;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM (SUBST1_TAC o GSYM);
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let CC_CELL_EXTREME_CARD = 
prove_by_refinement(
  `!V ul pp.    packing V /\
         saturated V /\
         leaf V ul /\
         ((if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul)) =
         pp) ==> CARD {EL 0 ul, EL 1 ul, EL 2 ul,pp} = 4`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  MATCH_MP_TAC Collect_geom2.NOT_COPLANAR_IMP_CARD4;
  GMATCH_SIMP_TAC (GSYM coplanar_eq_coplanar_alt);
  REWRITE_TAC[DIMINDEX_3;arith `2 <= 3`];
  MATCH_MP_TAC CC_CELL_NOT_COPLANAR_EXTREME;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let CC_CELL_INDEPENDENT = 
prove_by_refinement(
  `!V ul pp.    packing V /\
         saturated V /\
         leaf V ul /\
         (if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul)) =
         pp ==> ~affine_dependent {EL 0 ul, EL 1 ul, EL 2 ul,pp}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD];
  GMATCH_SIMP_TAC CC_CELL_EXTREME_CARD;
  CONJ_TAC;
    TYPIFY `V` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  CONJ_TAC;
    BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
  REWRITE_TAC[INT_ARITH `&4 - (int_of_num) 1 = &3`];
  REWRITE_TAC[INT_ARITH `x = int_of_num 3 <=> x <= &3 /\ ~(x <= &2)`];
  CONJ_TAC;
    INTRO_TAC AFF_DIM_LE_UNIV [`{EL 0 ul, EL 1 ul, EL 2 ul, pp}`];
    BY(REWRITE_TAC[DIMINDEX_3]);
  DISCH_THEN (MP_TAC o (MATCH_MP Rogers.AFF_DIM_LE_2_IMP_COPLANAR));
  REWRITE_TAC[];
  MATCH_MP_TAC CC_CELL_NOT_COPLANAR_EXTREME;
  TYPIFY `V` EXISTS_TAC;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let CC_CELL_CONVEX_HULL_INJ = 
prove_by_refinement(
  `!V ul vl pu pv. packing V /\ saturated V /\ leaf V ul /\ leaf V vl /\
      (if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul)) = pu /\
      (if cc_ke V vl = 3 then mxi V (cc_uh V vl) else EL 3 (cc_uh V vl)) = pv /\
    cc_cell V ul = cc_cell V vl ==>
    {EL 0 ul, EL 1 ul, EL 2 ul, pu} = {EL 0 vl,EL 1 vl, EL 2 vl, pv}
   `,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Packing3.CONVEX_HULL_EQ_EQ_SET_EQ [`    {EL 0 ul, EL 1 ul, EL 2 ul, pu}`;`{EL 0 vl,EL 1 vl, EL 2 vl, pv}`];
  ANTS_TAC;
    BY(CONJ_TAC THEN MATCH_MP_TAC CC_CELL_INDEPENDENT THEN TYPIFY `V` EXISTS_TAC THEN ASM_REWRITE_TAC[]);
  DISCH_THEN (unlist REWRITE_TAC o SYM);
  FIRST_X_ASSUM MP_TAC;
  REPEAT (GMATCH_SIMP_TAC CC_CELL34);
  TYPIFY `pv` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `pu` EXISTS_TAC;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let FUEIMOV_K = 
prove_by_refinement(
  `!V ul vl.   saturated V /\ packing V /\ leaf V ul /\ leaf V vl /\
   cc_cell V ul = cc_cell V vl ==> (cc_ke V ul = cc_ke V vl)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[cc_cell];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Ajripqn.AJRIPQN [`V`;`(cc_uh V ul)`;`(cc_uh V vl)`;`(cc_ke V ul)`;`(cc_ke V vl)`];
  ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
  DISCH_THEN MATCH_MP_TAC;
  TYPIFY `barV V 3 (cc_uh V ul) /\ barV V 3 (cc_uh V vl)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(ASM_MESON_TAC[REWRITE_RULE[IN] cc_uh]);
  ASM_SIMP_TAC[CC_KE_34];
  REWRITE_TAC[INTER_IDEMPOT];
  BY(ASM_MESON_TAC[ CC_CELL_NOT_NULLSET;cc_cell])
  ]);;
  (* }}} *)

let LIST_OF_CC_UH = 
prove_by_refinement(
 `!V ul. saturated V /\ packing V /\ leaf V ul ==>
     (cc_uh V ul) = [EL 0 ul; EL 1 ul; EL 2 ul; EL 3 (cc_uh V ul)]`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `LENGTH (cc_uh V ul) = 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[cc_uh;IN;Sphere.BARV;arith `3 + 1 = 4`]);
  GMATCH_SIMP_TAC LENGTH4;
  ASM_REWRITE_TAC[];
  ASM_SIMP_TAC[EL_CC_UH];
  BY(SIMP_TAC[EL;HD;TL;arith `3  = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`])
  ]);;
  (* }}} *)

let SET_OF_LIST_CC_UH = 
prove_by_refinement(
  `!V ul. saturated V /\ packing V /\ leaf V ul ==>
    set_of_list (cc_uh V ul) = {EL 0 ul, EL 1 ul, EL 2 ul, EL 3 (cc_uh V ul)}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `LENGTH (cc_uh V ul) = 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[cc_uh;IN;Sphere.BARV;arith `3 + 1 = 4`]);
  GMATCH_SIMP_TAC set_of_list4;
  ASM_REWRITE_TAC[];
  BY(ASM_SIMP_TAC[EL_CC_UH])
  ]);;
  (* }}} *)

let MCELL4_EXTREME_POINT = 
prove_by_refinement(
  `!V ul vl. saturated V /\ packing V /\ leaf V ul /\ leaf V vl /\
    cc_cell V ul = cc_cell V vl /\ (cc_ke V ul = 4) ==> set_of_list (cc_uh V ul) = set_of_list (cc_uh V vl)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `cc_ke V vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[FUEIMOV_K]);
  ASM_SIMP_TAC[SET_OF_LIST_CC_UH];
  INTRO_TAC CC_CELL_CONVEX_HULL_INJ[`V`;`ul`;`vl`;`EL 3 (cc_uh V ul)`;`EL 3 (cc_uh V vl)`];
  BY(ASM_SIMP_TAC [arith `k = 4 ==> ~(k = 3)`])
  ]);;
  (* }}} *)

let STEM_OF_LEAF = 
prove_by_refinement(
  `!V ul. leaf V ul ==>
    stem ul = {EL 0 ul, EL 1 ul}`,

  (* {{{ proof *)
  [
  REWRITE_TAC[stem;leaf;IN;Sphere.BARV;arith `2 + 1 = 3`];
  REPEAT WEAK_STRIP_TAC;
  GMATCH_SIMP_TAC set_of_list2;
  SUBCONJ_TAC;
    REWRITE_TAC[arith `2 = 1 + 1`];
    MATCH_MP_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX;
    BY(ASM_REWRITE_TAC[arith `1 + 1 <= 3`]);
  DISCH_TAC;
  BY(ASM_MESON_TAC[arith `1+1<= 3 /\ 0 <= 1 /\ 1 <= 1`;Packing3.EL_TRUNCATE_SIMPLEX])
  ]);;
  (* }}} *)

let FUEIMOV_4 = 
prove_by_refinement(
  `!V ul vl. saturated V /\ packing V /\ leaf V ul /\ leaf V vl /\
    cc_cell V ul = cc_cell V vl /\ (stem ul = stem vl) /\ (cc_ke V ul = 4) /\ ~(ul = vl) ==>
    cc_uh V vl = [EL 1 ul;EL 0 ul;EL 3 (cc_uh V ul);EL 2 ul]`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `cc_ke V vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[FUEIMOV_K]);
  INTRO_TAC MCELL4_EXTREME_POINT [`V`;`ul`;`vl`];
  ASM_REWRITE_TAC[];
  REPEAT (GMATCH_SIMP_TAC SET_OF_LIST_CC_UH);
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM_ST `stem` MP_TAC;
  REPEAT (GMATCH_SIMP_TAC STEM_OF_LEAF);
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  TYPIFY `(EL 0 vl = EL 0 ul /\ EL 1 vl = EL 1 ul) \/ (EL 0 vl = EL 1 ul /\ EL 1 vl = EL 0 ul)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM MP_TAC;
    BY(SET_TAC[]);
  INTRO_TAC K4_CHI_MSB_POS [`V`;`ul`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC K4_CHI_MSB_POS [`V`;`vl`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY ` [EL 0 ul; EL 1 ul; EL 2 ul] = ul /\ [EL 0 vl; EL 1 vl; EL 2 vl] = vl` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[LENGTH3;leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  FIRST_X_ASSUM_ST `\/` DISJ_CASES_TAC;
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    INTRO_TAC LENGTH4_SET2 [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 (cc_uh V ul)`;`EL 2 vl`;`EL 3 (cc_uh V vl)`];
    ANTS_TAC;
      INTRO_TAC CC_CELL_EXTREME_CARD[`V`;`ul`;`EL 3(cc_uh V ul)`];
      ASM_REWRITE_TAC[arith `~(4=3)`];
      DISCH_THEN (SUBST1_TAC);
      BY(ASM_REWRITE_TAC[set_of_list4_explicit]);
    DISCH_THEN DISJ_CASES_TAC;
      BY(ASM_MESON_TAC[]);
    REPEAT (FIRST_X_ASSUM_ST `/\` MP_TAC) THEN REPEAT WEAK_STRIP_TAC;
    PROOF_BY_CONTR_TAC;
    REPEAT (FIRST_X_ASSUM_ST `chi_msb` MP_TAC);
    ABBREV_TAC `c = cc_uh V ul`;
    ABBREV_TAC `d = cc_uh V vl`;
    EXPAND_TAC "ul";
    EXPAND_TAC "vl";
    REPEAT (FIRST_X_ASSUM_ST `CONS x y = z` kill);
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    ONCE_REWRITE_TAC[chi_msb_swap_23];
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  COMMENT "second branch";
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC LENGTH4_SET2_SWAP01 [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 (cc_uh V ul)`;`EL 2 vl`;`EL 3 (cc_uh V vl)`];
  ANTS_TAC;
    INTRO_TAC CC_CELL_EXTREME_CARD[`V`;`ul`;`EL 3(cc_uh V ul)`];
    ASM_REWRITE_TAC[arith `~(4=3)`];
    DISCH_THEN (SUBST1_TAC);
    BY(ASM_REWRITE_TAC[set_of_list4_explicit]);
  DISCH_THEN DISJ_CASES_TAC;
    REPEAT (FIRST_X_ASSUM_ST `/\` MP_TAC) THEN REPEAT WEAK_STRIP_TAC;
    PROOF_BY_CONTR_TAC;
    REPEAT (FIRST_X_ASSUM_ST `chi_msb` MP_TAC);
    ABBREV_TAC `c = cc_uh V ul`;
    ABBREV_TAC `d = cc_uh V vl`;
    EXPAND_TAC "ul";
    EXPAND_TAC "vl";
    REPEAT (FIRST_X_ASSUM_ST `CONS x y = z` kill);
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    ONCE_REWRITE_TAC[chi_msb_swap_01];
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  INTRO_TAC LIST_OF_CC_UH [`V`;`vl`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_THEN SUBST1_TAC;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let MXI_NOT_IN_V = 
prove_by_refinement(
  `!V ul. saturated V /\ packing V /\ leaf V ul /\ (cc_ke V ul = 3)  ==>
    ~(mxi V (cc_uh V ul) IN V)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC MXI_IN_VORONOI_LIST [`V`;`(cc_uh V ul)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      BY(ASM_MESON_TAC[cc_uh;IN]);
    FIRST_X_ASSUM_ST `cc_ke` MP_TAC;
    REWRITE_TAC[cc_ke];
    COND_CASES_TAC;
      BY(REWRITE_TAC[arith `~(4=3)`]);
    ASM_SIMP_TAC[arith `~(x < y) ==> (y <= x)`];
    BY(ASM_MESON_TAC[cc_uh;leaf]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `EL 0 (cc_uh V ul) = EL 0 ul` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[EL_CC_UH]);
  TYPIFY `EL 0 (cc_uh V ul) IN V` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_REWRITE_TAC[EL];
    INTRO_TAC Packing3.BARV_SUBSET [`V`;`2`;`ul`];
    ANTS_TAC;
      BY(ASM_MESON_TAC[leaf;IN]);
    INTRO_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST [`V`;`2`;`ul`];
    ANTS_TAC;
      BY(ASM_MESON_TAC[leaf;IN]);
    BY(ASM_MESON_TAC[Packing3.IN_TRANS]);
  TYPIFY `&0 < sqrt2 /\ sqrt2 < sqrt(&4)` (C SUBGOAL_THEN MP_TAC);
    REWRITE_TAC[Sphere.sqrt2];
    GMATCH_SIMP_TAC REAL_LT_RSQRT;
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    GMATCH_SIMP_TAC REAL_LT_RSQRT;
    GMATCH_SIMP_TAC SQRT_POW_2;
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[Collect_geom2.SQRT4_EQ2];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM_ST `packing` MP_TAC;
  REWRITE_TAC[Sphere.packing;NOT_FORALL_THM];
  GEXISTL_TAC [`EL 0 (cc_uh V ul)`;`mxi V (cc_uh V ul)`];
  ASM_REWRITE_TAC[];
  ASM_SIMP_TAC[arith `x < y ==> ~(y <= x)`];
  CONJ_TAC;
    BY(ASM_MESON_TAC[IN]);
  CONJ_TAC;
    BY(ASM_MESON_TAC[IN]);
  DISCH_TAC;
  FIRST_X_ASSUM_ST `dist` MP_TAC;
  ASM_REWRITE_TAC[DIST_REFL];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let MCELL_V_INTER_EXTREME = 
prove_by_refinement(
 `!V ul .
         saturated V /\ packing V /\ leaf V ul /\ (cc_ke V ul = 3) 
   ==>
   V INTER  {EL 0 ul,EL 1 ul, EL 2 ul,mxi V (cc_uh V ul)} = set_of_list ul`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  MATCH_MP_TAC SUBSET_ANTISYM;
  CONJ2_TAC;
    REWRITE_TAC[SUBSET_INTER];
    CONJ_TAC;
      MATCH_MP_TAC Packing3.BARV_SUBSET;
      EXISTS_TAC `2`;
      BY(ASM_MESON_TAC[leaf;IN]);
    GMATCH_SIMP_TAC set_of_list3;
    ASM_REWRITE_TAC[];
    BY(SET_TAC[]);
  GMATCH_SIMP_TAC set_of_list3;
  ASM_REWRITE_TAC[];
  INTRO_TAC MXI_NOT_IN_V [`V`;`ul`];
  ASM_REWRITE_TAC[];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let MCELL_EXTREME_DIFF_V = 
prove_by_refinement(
 `!V ul .
         saturated V /\ packing V /\ leaf V ul /\ (cc_ke V ul = 3) 
   ==>
     {EL 0 ul,EL 1 ul, EL 2 ul,mxi V (cc_uh V ul)} DIFF V = {mxi V (cc_uh V ul)}`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  MATCH_MP_TAC SUBSET_ANTISYM;
  CONJ2_TAC;
    INTRO_TAC MXI_NOT_IN_V [`V`;`ul`];
    ASM_REWRITE_TAC[];
    BY(SET_TAC[]);
  INTRO_TAC MCELL_V_INTER_EXTREME [`V`;`ul`];
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC set_of_list3;
  ASM_REWRITE_TAC[];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let FUEIMOV_3 = 
prove_by_refinement(
  `!V ul vl.   saturated V /\ packing V /\ leaf V ul /\ leaf V vl /\ (cc_ke V ul = 3) /\
   {EL 0 ul,EL 1 ul} = {EL 0 vl,EL 1 vl} /\ cc_cell V ul = cc_cell V vl ==> (ul = vl)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `LENGTH ul = 3 /\ LENGTH vl = 3` (C SUBGOAL_THEN MP_TAC);
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `cc_ke V vl = 3` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC CC_KE_34 [`V`;`vl`];
    DISCH_THEN DISJ_CASES_TAC;
      BY(ASM_REWRITE_TAC[]);
    INTRO_TAC FUEIMOV_K [`V`;`vl`;`ul`];
    BY(ASM_REWRITE_TAC[]);
  INTRO_TAC CC_CELL_CONVEX_HULL_INJ [`V`;`ul`;`vl`;`mxi V (cc_uh V ul)`;`mxi V (cc_uh V vl)`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `mxi V (cc_uh V ul) = mxi V (cc_uh V vl)` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC MCELL_EXTREME_DIFF_V [`V`;`ul`];
    INTRO_TAC MCELL_EXTREME_DIFF_V [`V`;`vl`];
    FIRST_X_ASSUM MP_TAC;
    ASM_REWRITE_TAC[];
    BY(SET_TAC[]);
  TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul} =       {EL 0 vl, EL 1 vl, EL 2 vl}` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC MCELL_V_INTER_EXTREME [`V`;`ul`];
    INTRO_TAC MCELL_V_INTER_EXTREME [`V`;`vl`];
    ASM_REWRITE_TAC[];
    REPEAT (GMATCH_SIMP_TAC set_of_list3);
    CONJ_TAC;
      BY(ASM_REWRITE_TAC[]);
    CONJ_TAC;
      BY(ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM_ST `EL` MP_TAC;
    BY(SET_TAC[]);
  TYPIFY `~(EL 0 ul = EL 1 ul)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT;
    GEXISTL_TAC [`EL 2 ul`;`mxi V (cc_uh V ul)`];
    MATCH_MP_TAC CC_CELL_EXTREME_CARD;
    TYPIFY `V` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~(EL 1 ul = EL 2 ul)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT;
    GEXISTL_TAC [`EL 0 ul`;`mxi V (cc_uh V ul)`];
    TYPIFY `{EL 1 ul, EL 2 ul, EL 0 ul, mxi V (cc_uh V ul)} = {EL 0 ul, EL 1 ul, EL 2 ul, mxi V (cc_uh V ul)}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    MATCH_MP_TAC CC_CELL_EXTREME_CARD;
    TYPIFY `V` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~(EL 0 ul = EL 2 ul)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT;
    GEXISTL_TAC [`EL 1 ul`;`mxi V (cc_uh V ul)`];
    TYPIFY `{EL 0 ul, EL 2 ul, EL 1 ul, mxi V (cc_uh V ul)} = {EL 0 ul, EL 1 ul, EL 2 ul, mxi V (cc_uh V ul)}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    MATCH_MP_TAC CC_CELL_EXTREME_CARD;
    TYPIFY `V` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `((EL 0 vl = EL 0 ul) /\ (EL 1 vl = EL 1 ul)) \/ ((EL 0 vl = EL 1 ul) /\ (EL 1 vl = EL 0 ul))` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `{a,b}={c,d}` MP_TAC;
    REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND];
    DISCH_THEN DISJ_CASES_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(ASM_REWRITE_TAC[]);
  COMMENT "1. next match EL 2";
  TYPIFY `EL 2 vl = EL 2 ul` (C SUBGOAL_THEN ASSUME_TAC);
    (FIRST_X_ASSUM_ST `x INSERT y =  x' INSERT y'` MP_TAC);
    REWRITE_TAC[EXTENSION;IN_INSERT;NOT_IN_EMPTY];
    DISCH_TAC;
    FIRST_ASSUM (C INTRO_TAC [`EL 0 ul`]);
    FIRST_ASSUM (C INTRO_TAC [`EL 1 ul`]);
    FIRST_X_ASSUM (C INTRO_TAC [`EL 2 ul`]);
    REPEAT (FIRST_X_ASSUM_ST `~` MP_TAC);
    REWRITE_TAC[];
    FIRST_X_ASSUM DISJ_CASES_TAC;
      ASM_REWRITE_TAC[];
      BY(MESON_TAC[]);
    ASM_REWRITE_TAC[];
    BY(MESON_TAC[]);
  COMMENT "1. now use chi_msb to eliminate the second case";
  FIRST_X_ASSUM DISJ_CASES_TAC;
    ONCE_REWRITE_TAC[EQ_SYM_EQ];
    GMATCH_SIMP_TAC LENGTH3;
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[LENGTH3]);
  INTRO_TAC CELL3_NONDEG [`V`;`ul`];
  ASM_REWRITE_TAC[];
  INTRO_TAC CELL3_NONDEG [`V`;`vl`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  ABBREV_TAC `xi = mxi V (cc_uh V vl)`;
  TYPIFY `chi_msb vl xi = chi_msb [EL 1 ul;EL 0 ul;EL 2 ul] xi` (C SUBGOAL_THEN MP_TAC);
    REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
    REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH3)));
    DISCH_TAC;
    DISCH_THEN SUBST1_TAC;
    BY(ASM_REWRITE_TAC[]);
  ONCE_REWRITE_TAC[chi_msb_swap_01];
  REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH3)));
  DISCH_THEN (SUBST1_TAC o GSYM);
  REPEAT (FIRST_X_ASSUM_ST `chi_msb` MP_TAC);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let TWO_REARRANGEMENT_LEMMA_ALT  = 
prove_by_refinement(
  `!V ul  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)`,

  (* {{{ proof *)
  [
  BY(MESON_TAC[Qzksykg.TWO_REARRANGEMENT_LEMMA])
  ]);;
  (* }}} *)

let MCELL2_EDGE_FIRST = 
prove_by_refinement(
  `!V ul u v. saturated V /\ packing V /\ ul IN barV V 3 /\
    {u,v} IN edgeX V (mcell2 V ul) ==>
    (?vl. vl IN barV V 3 /\ u = EL 0 vl /\ v = EL 1 vl /\ mcell2 V ul = mcell2 V vl)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `barV V 3 ul` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[IN]);
  INTRO_TAC MCELL2_EDGE [`V`;`ul`;`{u,v}`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[IN]);
  REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
  REPEAT WEAK_STRIP_TAC;
    TYPIFY `ul` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  COMMENT "second case";
  INTRO_TAC TWO_REARRANGEMENT_LEMMA_ALT [`V`;`ul`;`v`;`u`;`EL 2 ul`;`EL 3 ul`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC LENGTH4;
    BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Rvfxzbu.RVFXZBU [`V`;`ul`;`2`;`p`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[IN_INSERT;arith `2 -1 = 1`]);
  DISCH_TAC;
  INTRO_TAC Qzksykg.QZKSYKG1 [`V`;`ul`;`left_action_list p ul`;`2`;`p`];
  ANTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;arith `2 - 1 = 1`];
    DISCH_TAC;
    BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL2;NEGLIGIBLE_EMPTY]);
  DISCH_TAC;
  TYPIFY `left_action_list p ul` EXISTS_TAC;
  ASM_REWRITE_TAC[IN;MCELL2];
  FIRST_X_ASSUM_ST `EL 3` (SUBST1_TAC o SYM);
  REPEAT (FIRST_X_ASSUM_ST `EL` MP_TAC);
  REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let FINITE_CARD1_IMP_SINGLETON = 
prove_by_refinement(
  `!(S:A->bool). FINITE S /\ CARD S = 1 ==> (?x. S = {x})`,

  (* {{{ proof *)
  [
  ASM_MESON_TAC[ Local_lemmas.FINITE_CARD1_IMP_SINGLETON]
  ]);;
  (* }}} *)

let SET2_INSERT1 = 
prove_by_refinement(
  `!(a:A) b x y z. {a,b} SUBSET {x,y,z} /\ ~(a = b) ==> (?c. {a,b,c} = {x,y,z})`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `FINITE ({x, y, z} DIFF {a, b})` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC FINITE_DIFF;
    BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
  TYPIFY `CARD {x,y,z} <= 3` (C SUBGOAL_THEN ASSUME_TAC);
    BY(MESON_TAC[Geomdetail.CARD3]);
  INTRO_TAC Hypermap.LEMMA_CARD_DIFF [`{x,y,z}`;`{a,b}`];
  ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
  TYPIFY `CARD {a,b} = 2` (C SUBGOAL_THEN SUBST1_TAC);
    BY(ASM_REWRITE_TAC[Geomdetail.CARD_SET2]);
  DISCH_TAC;
  TYPIFY `CARD ({x,y,z} DIFF {a,b}) = 0 \/ CARD({x,y,z} DIFF {a,b}) = 1` (C SUBGOAL_THEN MP_TAC);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  REPEAT WEAK_STRIP_TAC;
    INTRO_TAC CARD_EQ_0 [`{x, y, z} DIFF {a, b}`];
    ASM_REWRITE_TAC[];
    REPEAT WEAK_STRIP_TAC;
    TYPIFY `a` EXISTS_TAC;
    FIRST_X_ASSUM MP_TAC;
    FIRST_X_ASSUM_ST `SUBSET` MP_TAC;
    BY(SET_TAC[]);
  INTRO_TAC FINITE_CARD1_IMP_SINGLETON [`{x, y, z} DIFF {a, b}`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `x'` EXISTS_TAC;
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
  ]);;
  (* }}} *)

let MCELL3_EDGE_FIRST = 
prove_by_refinement(
  `!V ul u v. saturated V /\ packing V /\ ul IN barV V 3 /\
    {u,v} IN edgeX V (mcell3 V ul) ==>
    (?vl. vl IN barV V 3 /\ u = EL 0 vl /\ v = EL 1 vl /\ mcell3 V ul = mcell3 V vl)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `barV V 3 ul` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[IN]);
  TYPIFY `~NULLSET(mcell3 V ul)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL3;NEGLIGIBLE_EMPTY]);
  INTRO_TAC MCELL3_EDGE [`V`;`ul`;`u`;`v`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[IN]);
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC SET_OF_LIST_TRUNCATE_2 [`ul`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[arith `3 <= 3 + 1`;IN;Sphere.BARV]);
  DISCH_TAC;
  INTRO_TAC SET2_INSERT1 [`u`;`v`;`EL 0 ul`;`EL 1 ul`;`EL 2 ul`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul} = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
    ONCE_REWRITE_TAC[EQ_SYM_EQ];
    MATCH_MP_TAC set_of_list4;
    BY(ASM_MESON_TAC[arith `3+1 = 4`;IN;Sphere.BARV]);
  INTRO_TAC Marchal_cells_3.LEFT_ACTION_LIST_2_EXISTS [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`u`;`v`;`c`;`EL 3 ul`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`];
    ANTS_TAC;
      BY(ASM_MESON_TAC[IN]);
    MATCH_MP_TAC (arith `(x = y) ==> (x = 3 +1 ==> y = 4)`);
    BY(REWRITE_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `left_action_list p ul` EXISTS_TAC;
  INTRO_TAC Rvfxzbu.RVFXZBU [`V`;`ul`;`3`;`p`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[IN_INSERT;arith `3 -1 = 2`]);
  DISCH_TAC;
  INTRO_TAC Qzksykg.QZKSYKG1 [`V`;`ul`;`left_action_list p ul`;`3`;`p`];
  ANTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;arith `3 - 1 = 2`];
    DISCH_TAC;
    BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL3;NEGLIGIBLE_EMPTY]);
  DISCH_TAC;
  ASM_REWRITE_TAC[IN;MCELL3];
  INTRO_TAC LENGTH4 [`ul`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[arith `3 + 1 = 4`;IN;Sphere.BARV]);
  DISCH_THEN (ASSUME_TAC o SYM);
  FIRST_X_ASSUM_ST `CONS x y = left_action_list p q` MP_TAC;
  ASM_REWRITE_TAC[];
  DISCH_THEN (SUBST1_TAC o SYM);
  BY(REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`])
  ]);;
  (* }}} *)

let SET2_INSERT2 = 
prove_by_refinement(
  `!(a:A) b w x y z. {a,b} SUBSET {w,x,y,z} /\ ~(a = b) /\ CARD {w,x,y,z} = 4 ==>
     (?c d. {w,x,y,z} = {a,b,c,d})`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Hypermap.LEMMA_CARD_DIFF [`{w,x,y,z}`;`{a,b}`];
  ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
  INTRO_TAC Hypermap.CARD_TWO_ELEMENTS [`a`;`b`];
  ASM_REWRITE_TAC[];
  DISCH_THEN SUBST1_TAC;
  REWRITE_TAC [arith `4 = x + 2 <=> x = 2`];
  DISCH_TAC;
  INTRO_TAC Rogers.CARD_2_IMP_DOUBLE [`{w, x, y, z} DIFF {a, b}`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    MATCH_MP_TAC FINITE_DIFF;
    BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
  REPEAT WEAK_STRIP_TAC;
  GEXISTL_TAC [`a'`;`b'`];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
  ]);;
  (* }}} *)

let MCELL4_EDGE_FIRST = 
prove_by_refinement(
  `!V ul u v. saturated V /\ packing V /\ ul IN barV V 3 /\
    {u,v} IN edgeX V (mcell4 V ul) ==>
    (?vl. vl IN barV V 3 /\ u = EL 0 vl /\ v = EL 1 vl /\ mcell4 V ul = mcell4 V vl)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `barV V 3 ul` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[IN]);
  TYPIFY `~NULLSET(mcell4 V ul)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL4;NEGLIGIBLE_EMPTY]);
  INTRO_TAC MCELL4_EDGE [`V`;`ul`;`u`;`v`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul} = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
    ONCE_REWRITE_TAC[EQ_SYM_EQ];
    MATCH_MP_TAC set_of_list4;
    BY(ASM_MESON_TAC[arith `3+1 = 4`;IN;Sphere.BARV]);
  INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`];
  ASM_REWRITE_TAC[arith `3 + 1 = 4`];
  DISCH_TAC;
  INTRO_TAC SET2_INSERT2 [`u`;`v`;`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Marchal_cells_3.LEFT_ACTION_LIST_3_EXISTS [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 ul`;`u`;`v`;`c`;`d`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `left_action_list p ul` EXISTS_TAC;
  INTRO_TAC Rvfxzbu.RVFXZBU [`V`;`ul`;`4`;`p`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[IN_INSERT;arith `4 -1 = 3`]);
  DISCH_TAC;
  INTRO_TAC Qzksykg.QZKSYKG1 [`V`;`ul`;`left_action_list p ul`;`4`;`p`];
  ANTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;arith `4 - 1 = 3`];
    DISCH_TAC;
    BY(ASM_MESON_TAC[MCELL4;NEGLIGIBLE_EMPTY]);
  DISCH_TAC;
  ASM_REWRITE_TAC[IN;MCELL4];
  INTRO_TAC LENGTH4 [`ul`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[arith `3 + 1 = 4`;IN;Sphere.BARV]);
  DISCH_THEN (ASSUME_TAC o SYM);
  FIRST_X_ASSUM_ST `CONS x y = left_action_list p q` MP_TAC;
  ASM_REWRITE_TAC[];
  DISCH_THEN (SUBST1_TAC o SYM);
  BY(REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`])
  ]);;
  (* }}} *)


(* MCELL_EDGE_FIRST is YSAKKTX in the notes *)

let MCELL_EDGE_FIRST = 
prove_by_refinement(
  `!V ul k u v. saturated V /\ packing V /\ ul IN barV V 3 /\
    {u,v} IN edgeX V (mcell k V ul) ==>  
    (?vl. vl IN barV V 3 /\ mcell k V vl = mcell k V ul /\ u = EL 0 vl /\ v = EL 1 vl)
     `,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  MP_TAC (arith `k <= 1 \/ k = 2 \/ k = 3 \/ 4 <= k`);
  REPEAT WEAK_STRIP_TAC;
        BY(ASM_MESON_TAC[EDGE_IMP_K2;NOT_IN_EMPTY;IN]);
      INTRO_TAC MCELL2_EDGE_FIRST [`V`;`ul`;`u`;`v`];
      REWRITE_TAC[MCELL2];
      BY(ASM_MESON_TAC[]);
    INTRO_TAC MCELL3_EDGE_FIRST [`V`;`ul`;`u`;`v`];
    REWRITE_TAC[MCELL3];
    BY(ASM_MESON_TAC[]);
  INTRO_TAC MCELL4_EDGE_FIRST [`V`;`ul`;`u`;`v`];
  FIRST_X_ASSUM_ST `mcell` MP_TAC;
  ASM_REWRITE_TAC[Pack_defs.mcell];
  ASM_SIMP_TAC [arith `4 <= k ==> ~(k=0) /\ ~(k = 1) /\ ~(k=2) /\ ~(k = 3)`];
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let BARV3_TRUNC2 = 
prove_by_refinement(
  `!V ul. ul IN barV V 3 ==> truncate_simplex 2 ul = [EL 0 ul;EL 1 ul;EL 2 ul]`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `ul = [EL 0 ul;EL 1 ul; EL 2 ul; EL 3 ul]` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC LENGTH4;
    BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3+1 = 4`]);
  BY(ASM_MESON_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_2])
  ]);;
  (* }}} *)

let RBUTTCS = 
prove_by_refinement(
  `!V vl u v. saturated V /\ packing V /\  {u,v} IN edgeX V (mcell4  V vl) /\ vl IN barV V 3 ==>
    (?ul. leaf V ul /\ stem ul = {u,v} /\ (mcell4 V vl = cc_cell V ul))`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC MCELL_EDGE_FIRST [`V`;`vl`;`4`;`u`;`v`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(ASM_MESON_TAC[MCELL4]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(mcell 4 V vl' = {})` (C SUBGOAL_THEN MP_TAC);
    BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL4;NEGLIGIBLE_EMPTY]);
  DISCH_TAC;
  FIRST_X_ASSUM_ST `mcell 4 V vl' = mcell 4 V vl` (fun t -> REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[MCELL4] THEN SUBST1_TAC (SYM t));
  REWRITE_TAC[MCELL4] THEN REPEAT WEAK_STRIP_TAC;
  TYPED_ABBREV_TAC `(wl:(real^3) list) = truncate_simplex 2 (vl')` ;
  TYPIFY `hl vl' < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `mcell` MP_TAC;
    REWRITE_TAC[GSYM MCELL4;Pack_defs.mcell4];
    BY(MESON_TAC[]);
  INTRO_TAC Rogers.XNHPWAB4 [`V`;`vl'`;`3`];
  ASM_REWRITE_TAC[];
  DISCH_THEN (C INTRO_TAC [`2`;`3`]);
  ANTS_TAC;
    BY(ARITH_TAC);
  TYPIFY `truncate_simplex 3 vl' = vl'` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_REFL;
    BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 =4`]);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `hl wl < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  TYPIFY `leaf V wl` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[leaf];
    ASM_REWRITE_TAC[Sphere.sqrt2];
    REWRITE_TAC[IN];
    EXPAND_TAC "wl";
    MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
    BY(ASM_MESON_TAC[IN;arith `2 <= 3`]);
  TYPIFY `EL 0 wl = u /\ EL 1 wl = v /\ EL 2 wl = EL 2 vl'` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "wl";
    REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
    ASM_REWRITE_TAC[arith `1 <= 2 /\ 0 <= 2 /\ 2 <= 2`];
    BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `2 + 1 <= 3 + 1`]);
  ASM_CASES_TAC `mcell 4 V vl' = cc_cell V wl`;
    TYPIFY `wl` EXISTS_TAC;
    GMATCH_SIMP_TAC STEM_OF_LEAF;
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  INTRO_TAC CFFONNL [`V`;`wl`;`mcell 4 V vl'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    REWRITE_TAC[Pack_defs.mcell_set;IN_ELIM_THM];
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[GSYM MEMBER_NOT_EMPTY];
    TYPIFY `EL 2 wl` EXISTS_TAC;
    REWRITE_TAC[IN_INTER];
    CONJ_TAC;
      INTRO_TAC Lepjbdj.LEPJBDJ [`V`;`vl'`;`4`];
      ASM_REWRITE_TAC[arith `1 <= 4 /\ 4 <= 4 /\ 4 - 1 = 3`];
      ANTS_TAC;
        BY(ASM_MESON_TAC[IN]);
      TYPIFY `EL 2 vl' IN set_of_list vl'` ENOUGH_TO_SHOW_TAC;
        BY(SET_TAC[]);
      GMATCH_SIMP_TAC set_of_list4;
      CONJ_TAC;
        BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3+1 = 4`]);
      BY(SET_TAC[]);
    BY(REWRITE_TAC[cc_A0;Local_lemmas.X_IN_AFF_GT_X]);
  DISCH_THEN SUBST1_TAC;
  TYPIFY `[EL 1 vl';EL 0 vl';EL 2 vl']` EXISTS_TAC;
  REWRITE_TAC[];
  TYPIFY `wl = [EL 0 vl';EL 1 vl'; EL 2 vl']` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "wl";
    GMATCH_SIMP_TAC BARV3_TRUNC2;
    BY(ASM_MESON_TAC[]);
  INTRO_TAC ZASUVOR [`V`;`EL 0 vl'`;`EL 1 vl'`;`EL 2 vl'`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC STEM_OF_LEAF;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let STEM_EDGEX = 
prove_by_refinement(
  `!V ul. packing V /\ saturated V /\ leaf V ul ==>
    {EL 0 ul,EL 1 ul} IN edgeX V (cc_cell V ul)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC CC_CELL_NOT_NULLSET [`V`;`ul`];
  ASM_REWRITE_TAC[cc_cell];
  DISCH_TAC;
  INTRO_TAC CC_KE_34 [`V`;`ul`];
  DISCH_TAC;
  INTRO_TAC LIST_OF_CC_UH [`V`;`ul`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`cc_uh V ul`;`3`];
  INTRO_TAC EL_CC_UH [`V`;`ul`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC cc_uh [`V`;`ul`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  ANTS_TAC;
    BY(ASM_MESON_TAC[IN]);
  REWRITE_TAC[arith `3 + 1 = 4`];
  DISCH_TAC;
  INTRO_TAC set_of_list4 [`cc_uh V ul`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 =4`]);
  DISCH_TAC;
  INTRO_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 (cc_uh V ul)`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  COMMENT "do cases";
  FIRST_X_ASSUM DISJ_CASES_TAC;
    ASM_REWRITE_TAC[GSYM MCELL3];
    GMATCH_SIMP_TAC Bump.MCELL3_EDGE;
    ASM_REWRITE_TAC[];
    SUBCONJ_TAC;
      BY(ASM_MESON_TAC[IN;MCELL3]);
    DISCH_TAC;
    GMATCH_SIMP_TAC set_of_list3;
    CONJ_TAC;
      BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `3 = 2 + 1`]);
    BY(SET_TAC[]);
  COMMENT "do case 4";
  ASM_REWRITE_TAC[GSYM MCELL4];
  GMATCH_SIMP_TAC Bump.MCELL4_EDGE;
  ASM_REWRITE_TAC[];
  SUBCONJ_TAC;
    BY(ASM_MESON_TAC[IN;MCELL4]);
  DISCH_TAC;
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let FCHKUGT = 
prove_by_refinement(
  `!V u0 u1 u2 u2'. saturated V /\ packing V /\ cc_A0 [u0;u1;u2] = cc_A0 [u0;u1;u2'] /\
   leaf V [u0;u1;u2] /\ leaf V [u0;u1;u2'] ==> (u2 = u2')`,

  (* {{{ proof *)
  [
  REWRITE_TAC[cc_A0;EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC STEM_EDGEX [`V`;`[u0;u1;u2]`];
    ASM_REWRITE_TAC[];
    ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;CONS_11];
    REWRITE_TAC[IN_ELIM_THM;Pack_defs.edgeX;Geomdetail.PAIR_EQ_EXPAND];
    BY(MESON_TAC[]);
  INTRO_TAC ZASUVOR [`V`;`u0`;`u1`;`u2`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC CFFONNL [`V`;`[u0;u1;u2]`;`cc_cell V [u0;u1;u2']`];
  ASM_SIMP_TAC[CC_CELL_IN_MCELL_SET];
  REWRITE_TAC[TAUT `(a /\ b /\ ~c ==> d) <=> (a /\ b ==> c \/ d)`];
  ANTS_TAC;
    REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`];
    CONJ_TAC;
      TYPIFY `{u0,u1} = {EL 0 [u0;u1;u2'],EL 1 [u0;u1;u2']}` (C SUBGOAL_THEN SUBST1_TAC);
        BY(REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`]);
      MATCH_MP_TAC STEM_EDGEX;
      BY(ASM_REWRITE_TAC[]);
    INTRO_TAC NUNRRDS_0 [`V`;`[u0;u1;u2']`];
    ASM_REWRITE_TAC[cc_A0];
    REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
  DISCH_TAC;
  INTRO_TAC CC_KE_34 [`V`;`[u0;u1;u2']`];
  COMMENT "case k=3";
  DISCH_THEN DISJ_CASES_TAC;
    FIRST_X_ASSUM DISJ_CASES_TAC;
      INTRO_TAC FUEIMOV_3 [`V`;`[u0;u1;u2']`;`[u0;u1;u2]`];
      ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;CONS_11];
      BY(MESON_TAC[]);
    INTRO_TAC FUEIMOV_3 [`V`;`[u0;u1;u2']`;`[u1;u0;u2]`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;CONS_11;Geomdetail.PAIR_EQ_EXPAND]);
    BY(ASM_REWRITE_TAC[CONS_11]);
  COMMENT "case k=4";
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM DISJ_CASES_TAC;
    INTRO_TAC FUEIMOV_4 [`V`;`[u0;u1;u2']`;`[u0;u1;u2]`];
    REWRITE_TAC[CONS_11];
    ASM_REWRITE_TAC[];
    DISCH_THEN MP_TAC THEN ANTS_TAC;
      REPEAT (GMATCH_SIMP_TAC STEM_OF_LEAF);
      REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;Geomdetail.PAIR_EQ_EXPAND];
      BY(ASM_MESON_TAC[]);
    ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`];
    INTRO_TAC LIST_OF_CC_UH [`V`;`[u0;u1;u2]`];
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    BY(ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;CONS_11]);
  COMMENT "case k=4 a";
  INTRO_TAC FUEIMOV_4 [`V`;`[u0;u1;u2']`;`[u1;u0;u2]`];
  REWRITE_TAC[CONS_11];
  ASM_REWRITE_TAC[];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    REPEAT (GMATCH_SIMP_TAC STEM_OF_LEAF);
    REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;Geomdetail.PAIR_EQ_EXPAND];
    BY(ASM_MESON_TAC[]);
  INTRO_TAC LIST_OF_CC_UH [`V`;`[u1;u0;u2]`];
  ASM_REWRITE_TAC[];
  DISCH_THEN SUBST1_TAC;
  REWRITE_TAC[CONS_11];
  TYPIFY `EL 2 [u1;u0;u2] = u2` (C SUBGOAL_THEN SUBST1_TAC);
    BY(ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;CONS_11]);
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC CC_CELL_NOT_COPLANAR_EXTREME [`V`;`[u0;u1;u2']`;`u2`];
  ASM_REWRITE_TAC[arith `~(4=3)`];
  FIRST_X_ASSUM kill;
  FIRST_X_ASSUM (SUBST1_TAC o SYM);
  ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;CONS_11];
  REPLICATE_TAC 8 (FIRST_X_ASSUM kill);
  REWRITE_TAC[coplanar];
  GEXISTL_TAC [`u0`;`u1`;`u2`];
  TYPIFY `{u0,u1,u2} SUBSET affine hull {u0,u1,u2}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[HULL_SUBSET]);
  TYPIFY `u2' IN affine hull {u0,u1,u2}` ENOUGH_TO_SHOW_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
  MATCH_MP_TAC Packing3.IN_TRANS;
  TYPIFY `aff_gt {u0,u1} {u2}` EXISTS_TAC;
  CONJ2_TAC;
    INTRO_TAC AFF_GT_SUBSET_AFFINE_HULL [`{u0,u1}`;`{u2}`];
    TYPIFY `{u0,u1} UNION {u2} = {u0,u1,u2}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  BY(REWRITE_TAC[Local_lemmas.X_IN_AFF_GT_X])
  ]);;
  (* }}} *)

let AZIM_BASE_SHIFT_LE = 
prove_by_refinement(
  `!x y b1 b2 w1 w2.
    ~(collinear {x,y,b1}) /\ ~(collinear {x,y,b2}) /\ ~(collinear {x,y,w1}) /\
    ~(collinear {x,y,w2}) /\ 
    azim x y b1 b2 <= azim x y b1 w1 /\
    azim x y b1 b2 <= azim x y b1 w2  ==>
    azim x y b1 w2 - azim x y b1 w1 = azim x y b2 w2 - azim x y b2 w1`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Fan.sum4_azim_fan [`x`;`y`;`b1`;`b2`;`w1`];
  DISCH_THEN GMATCH_SIMP_TAC;
  INTRO_TAC Fan.sum4_azim_fan [`x`;`y`;`b1`;`b2`;`w2`];
  DISCH_THEN GMATCH_SIMP_TAC;
  ASM_REWRITE_TAC[];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let WEDGE_GE_SPLIT = 
prove_by_refinement(
  `!u0 u1 u2 u3 w.
    ~(collinear {u0,u1,u2}) /\
    ~(collinear {u0,u1,u3}) /\
    w IN wedge u0 u1 u2 u3 ==>
   (     ~(collinear {u0,u1,w}) /\
	   wedge_ge u0 u1 u2 u3 = wedge_ge u0 u1 u2 w UNION wedge_ge u0 u1 w u3)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[wedge;IN_ELIM_THM];
  REWRITE_TAC[EXTENSION;IN_UNION;Local_lemmas.WEDGE_GE_AZIM_LE];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  ASM_CASES_TAC `azim u0 u1 u2 x <= azim u0 u1 u2 w`;
    ASM_REWRITE_TAC[];
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  TYPIFY `collinear {u0,u1,x}` ASM_CASES_TAC;
    INTRO_TAC (CONJUNCT2 (CONJUNCT2 AZIM_DEGENERATE)) [`u0`;`u1`;`u2`;`x`];
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    INTRO_TAC (CONJUNCT2 (CONJUNCT2 AZIM_DEGENERATE)) [`u0`;`u1`;`w`;`x`];
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    BY(REWRITE_TAC[Local_lemmas.AZIM_RANGE]);
  ONCE_REWRITE_TAC[arith `x <= y <=> &0 <= y - x`];
  INTRO_TAC AZIM_BASE_SHIFT_LE [`u0`;`u1`;`u2`;`w`;`u3`;`x`];
  ASM_REWRITE_TAC[];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let IN_CONV0_IMP_AZIM_PI_ALT = 
prove_by_refinement(
  `!x e a b.  ~collinear {x, a, e} /\ x IN conv0 {a, b} ==> azim x e a b = pi`,

  (* {{{ proof *)
  [
  MESON_TAC[Local_lemmas.IN_CONV0_IMP_AZIM_PI]
  ]);;
  (* }}} *)

let AFF_GT_0_2 = 
prove
 (`!(v:real^A) w.
         aff_gt {} {v,w} =
             {y | ?t2 t3.
                     &0 < t2 /\
		     &0 < t3 /\
                     t2 + t3 = &1 /\
                     y = t2 % v + t3 % w}`,

  AFF_TAC
);;
let MIDPOINT_IN_CONV0 = 
prove_by_refinement(
  `!(p:real^A) q.  (#0.5) % (p + q) IN conv0 {p,q}`,

  (* {{{ proof *)
  [
  REWRITE_TAC[conv0;SYM Sphere.aff_gt_def;AFF_GT_0_2];
  REWRITE_TAC[conv0;SYM Sphere.aff_gt_def;AFF_GT_0_2;IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  GEXISTL_TAC [`#0.5`;`#0.5`];
  BY(REPEAT CONJ_TAC THENL [REAL_ARITH_TAC;REAL_ARITH_TAC;REAL_ARITH_TAC;VECTOR_ARITH_TAC])
  ]);;
  (* }}} *)

let AZIM_SPLIT_POINT = 
prove_by_refinement(
  `!u0 u1 u2 u3.
   ~collinear {u0,u1,u2} /\
   ~collinear {u0,u1,u3} /\
   pi < azim u0 u1 u2 u3 ==>
  (?w.
     w IN wedge u0 u1 u2 u3 /\
     azim u0 u1 u2 w = pi /\
     azim u0 u1 w u3 < pi)
`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ABBREV_TAC `(w:real^3) = &2 % u0 - u2`;
  TYPIFY `w` EXISTS_TAC;
  INTRO_TAC IN_CONV0_IMP_AZIM_PI_ALT [`u0`;`u1`;`u2`;`w`];
  ANTS_TAC;
    CONJ_TAC;
      TYPIFY `{u0,u2,u1} = {u0,u1,u2}` ENOUGH_TO_SHOW_TAC;
        BY(DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]);
      BY(SET_TAC[]);
    INTRO_TAC MIDPOINT_IN_CONV0 [`u2`;`w`];
    MATCH_MP_TAC (TAUT `(a = b) ==> (a ==> b)`);
    AP_THM_TAC THEN AP_TERM_TAC;
    EXPAND_TAC "w";
    BY(VECTOR_ARITH_TAC);
  DISCH_TAC;
  ASM_REWRITE_TAC[];
  ASM_REWRITE_TAC[wedge;IN_ELIM_THM];
  REWRITE_TAC[PI_POS];
  SUBCONJ_TAC;
    DISCH_TAC;
    INTRO_TAC (CONJUNCT2 (CONJUNCT2 AZIM_DEGENERATE)) [`u0`;`u1`;`u2`;`w`];
    ASM_REWRITE_TAC[];
    MP_TAC PI_POS;
    BY(REAL_ARITH_TAC);
  DISCH_TAC;
  INTRO_TAC Fan.sum4_azim_fan [`u0`;`u1`;`u2`;`w`;`u3`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(FIRST_X_ASSUM_ST `pi < x` MP_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `x = pi + y <=> y = x - pi`];
  DISCH_THEN SUBST1_TAC;
  BY(REWRITE_TAC[Local_lemmas.AZIM_RANGE;arith `x - pi < pi <=> x < &2 * pi`])
  ]);;
  (* }}} *)

let CLOSED_WEDGE_LT_PI = 
prove_by_refinement(
  `!u0 u1 u2 u3. ~collinear {u0,u1,u2} /\ ~ collinear {u0,u1,u3} /\
    azim u0 u1 u2 u3 < pi ==> closed (wedge_ge u0 u1 u2 u3)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ASM_SIMP_TAC[Local_lemmas.WEDGE_GE_EQ_AFF_GE];
  MATCH_MP_TAC CLOSED_AFF_GE;
  BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY])
  ]);;
  (* }}} *)

let CLOSED_WEDGE_EQ_PI = 
prove_by_refinement(
  `!u0 u1 u2 u3. ~collinear {u0,u1,u2} /\ ~ collinear {u0,u1,u3} /\
    azim u0 u1 u2 u3 = pi ==> closed (wedge_ge u0 u1 u2 u3)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ASM_SIMP_TAC[Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT];
  ABBREV_TAC `e = ((u1 - u0) cross (u2 - u0))`;
  TYPIFY `!x. e dot (x - u0) = e dot x - e dot u0` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    BY(VECTOR_ARITH_TAC);
  ONCE_REWRITE_TAC[arith `&0 <= x - y <=>  x >= y`];
  BY(REWRITE_TAC[CLOSED_HALFSPACE_GE])
  ]);;
  (* }}} *)

let CLOSED_WEDGE = 
prove_by_refinement(
  `!u0 u1 u2 u3. ~collinear {u0,u1,u2} /\ ~ collinear {u0,u1,u3}  ==> closed (wedge_ge u0 u1 u2 u3)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `azim u0 u1 u2 u3 < pi \/ azim u0 u1 u2 u3 = pi \/ pi < azim u0 u1 u2 u3` (C SUBGOAL_THEN MP_TAC);
    BY(REAL_ARITH_TAC);
  REPEAT WEAK_STRIP_TAC;
      BY(ASM_MESON_TAC[CLOSED_WEDGE_LT_PI]);
    BY(ASM_MESON_TAC[CLOSED_WEDGE_EQ_PI]);
  INTRO_TAC AZIM_SPLIT_POINT [`u0`;`u1`;`u2`;`u3`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC WEDGE_GE_SPLIT [`u0`;`u1`;`u2`;`u3`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC CLOSED_UNION;
  CONJ_TAC;
    BY(ASM_MESON_TAC[CLOSED_WEDGE_EQ_PI]);
  BY(ASM_MESON_TAC[CLOSED_WEDGE_LT_PI])
  ]);;
  (* }}} *)

let WEDGE_INTER_AFF_GE = 
prove_by_refinement(
  `!u0 u1 v1 v2. 
    wedge u0 u1 v1 v2 INTER aff_ge {u0,u1} {v1} = {} /\
    wedge u0 u1 v1 v2 INTER aff_ge {u0,u1} {v2} = {}
 `,

  (* {{{ proof *)
  [
  REWRITE_TAC[wedge;EXTENSION;NOT_IN_EMPTY;IN_INTER;IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  CONJ_TAC;
    REPEAT WEAK_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
    CONJ2_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    DISCH_TAC;
    BY(ASM_MESON_TAC[AZIM_DEGENERATE;arith `~(&0 < &0)`]);
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
  SUBCONJ_TAC;
    DISCH_TAC;
    BY(ASM_MESON_TAC[AZIM_DEGENERATE;arith `~(&0 < x /\ x < &0)`]);
  DISCH_TAC;
  TYPIFY `~collinear {u0,u1,v1}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[AZIM_DEGENERATE;arith `~(&0 < &0)`]);
  DISCH_TAC;
  INTRO_TAC Fan.sum5_azim_fan [`u0`;`u1`;`v1`;`v2`;`x`];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[Local_lemmas.AZIM_RANGE];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let AFF_GE_SUBSET_WEDGE_GE = 
prove_by_refinement(
  `!u0 u1 v1 v2.
    ~collinear {u0,u1,v1} /\
    ~collinear {u0,u1,v2} ==>
    aff_ge {u0,u1} {v1} SUBSET wedge_ge u0 u1 v1 v2 /\
    aff_ge {u0,u1} {v2} SUBSET wedge_ge u0 u1 v1 v2
    `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE;EXTENSION;NOT_IN_EMPTY;SUBSET;IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[AND_FORALL_THM];
  GEN_TAC;
  ASM_SIMP_TAC[GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2;Local_lemmas.AZIM_RANGE];
  DISCH_TAC;
  TYPIFY `collinear {u0,u1,x}` ASM_CASES_TAC;
    BY(ASM_MESON_TAC[AZIM_DEGENERATE;Local_lemmas.AZIM_RANGE]);
  INTRO_TAC Fan.sum5_azim_fan [`u0`;`u1`;`v1`;`v2`;`x`];
  ASM_REWRITE_TAC[Local_lemmas.AZIM_RANGE];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let BDXKHTW_PREP_LEMMA = 
prove_by_refinement(
  `!u0 u1 v1 v2 V X. saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\
    X IN mcell_set V /\
    {u0,u1} IN edgeX V X /\
    ~(azim u0 u1 v1 v2 = &0) /\ (?y. y IN X INTER wedge u0 u1 v1 v2) /\
    (?x. x IN X /\ ~(x IN wedge_ge u0 u1 v1 v2)) ==>
    (convex X /\ ~(u0=u1) /\ ~collinear {u0,u1,v1} /\ ~collinear {u0,u1,v2} /\
    (?p q. p IN X INTER wedge u0 u1 v1 v2 /\ q IN X DIFF wedge_ge u0 u1 v1 v2 /\ ~coplanar {p,q,u0,u1} /\
      ~(p IN aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}) /\ 
      ~(q IN aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2})))
`,

  (* {{{ proof *)
  [
  COMMENT "initialize";
  REWRITE_TAC[SUBSET;Pack_defs.mcell_set;IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC GBEWYFX [`V`;`[u0;u1;v1]`];
  INTRO_TAC GBEWYFX [`V`;`[u0;u1;v2]`];
  ASM_REWRITE_TAC[Bump.set_of_list3_explicit];
  REPEAT WEAK_STRIP_TAC;
  ASM_CASES_TAC `NULLSET X`;
    INTRO_TAC Bump.RIJRIED [`V`;`ul`;`i`];
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    DISCH_TAC;
    BY(ASM_MESON_TAC[NOT_IN_EMPTY]);
  TYPIFY `2 <= i` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[arith `2 <= i <=> ~(i <= 1)`];
    DISCH_TAC;
    INTRO_TAC Bump.EDGE_IMP_K2 [`V`;`ul`;`i`];
    ANTS_TAC;
      ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[IN]);
    BY(ASM_MESON_TAC[NOT_IN_EMPTY]);
  TYPIFY `convex X` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[MCELL_CONVEX;IN]);
  PROOF_BY_CONTR_TAC;
  ABBREV_TAC `(s:real^3->bool) = aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}`;
  TYPIFY `NULLSET s` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "s";
    MATCH_MP_TAC (CONJUNCT2 NULLSET_RULES);
    BY(ASM_SIMP_TAC[Conforming.NEGLIGIBLE_AFF_GE_2_1]);
  ABBREV_TAC `(X':real^3->bool) = X DIFF s`;
  COMMENT "X' not planar";
  TYPIFY `~(coplanar X')` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "X'";
    DISCH_TAC;
    TYPIFY `~(coplanar X)` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[COPLANAR_IMP_NEGLIGIBLE]);
    TYPIFY `X SUBSET X' UNION s` (C SUBGOAL_THEN ASSUME_TAC);
      EXPAND_TAC "X'";
      BY(SET_TAC[]);
    FIRST_X_ASSUM_ST `~NULLSET X` MP_TAC;
    REWRITE_TAC[];
    MATCH_MP_TAC NEGLIGIBLE_SUBSET;
    TYPIFY `X' UNION s` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC (CONJUNCT2 NULLSET_RULES);
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[COPLANAR_IMP_NEGLIGIBLE]);
  COMMENT "X'' not planar";
  INTRO_TAC COPLANAR_UNION [`X' INTER wedge u0 u1 v1 v2`;`X' INTER ((:real^3) DIFF wedge_ge u0 u1 v1 v2)`;`u0`;`u1`];
  ABBREV_TAC `X'' =  (X' INTER wedge u0 u1 v1 v2 UNION        X' INTER ((:real^3) DIFF wedge_ge u0 u1 v1 v2) UNION       {u0, u1})`;
  TYPIFY `X' SUBSET X''` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "X''";
    REWRITE_TAC[SUBSET;IN_UNION;IN_INTER;IN_DIFF;IN_UNIV];
    REPEAT WEAK_STRIP_TAC;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC (TAUT `(~a ==> b)    ==> (a \/ b \/ c)`);
    DISCH_TAC;
    INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v1`;`v2`];
    ASM_REWRITE_TAC[];
    REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
    EXPAND_TAC "X'";
    BY(SET_TAC[]);
  TYPIFY `~(coplanar X'')` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
    BY(MESON_TAC[COPLANAR_SUBSET]);
  COMMENT "start on conjuncts";
  CONJ_TAC;
    REWRITE_TAC[GSYM MEMBER_NOT_EMPTY];
    TYPIFY `y` EXISTS_TAC;
    EXPAND_TAC "X'";
    REWRITE_TAC[IN_INTER;IN_DIFF];
    TYPIFY `~(y IN s)` ENOUGH_TO_SHOW_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `INTER` MP_TAC) THEN SET_TAC[]);
    EXPAND_TAC "s";
    INTRO_TAC WEDGE_INTER_AFF_GE [`u0`;`u1`;`v1`;`v2`];
    BY(REPEAT (FIRST_X_ASSUM_ST `INTER` MP_TAC) THEN SET_TAC[]);
  CONJ_TAC;
    REWRITE_TAC[GSYM MEMBER_NOT_EMPTY];
    TYPIFY `x` EXISTS_TAC;
    EXPAND_TAC "X'";
    TYPIFY `s SUBSET wedge_ge u0 u1 v1 v2` ENOUGH_TO_SHOW_TAC;
      REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC);
      BY(SET_TAC[]);
    EXPAND_TAC "s";
    REWRITE_TAC[UNION_SUBSET];
    BY(ASM_SIMP_TAC[AFF_GE_SUBSET_WEDGE_GE]);
  COMMENT "next conjunct A";
  TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `~collinear t` kill;
    FIRST_X_ASSUM_ST `~collinear t` MP_TAC;
    BY(MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
  REWRITE_TAC[TAUT `(a /\ b /\ c) = ((a /\ b) /\ c)`];
  CONJ_TAC;
    REWRITE_TAC[AND_FORALL_THM];
    GEN_TAC;
    EXPAND_TAC "X'";
    EXPAND_TAC "s";
    REWRITE_TAC[IN_INTER;IN_UNION;IN_DIFF];
    TYPIFY `collinear {p,u0,u1} ==> p IN aff_ge {u0,u1} {v1}` ENOUGH_TO_SHOW_TAC;
      BY(MESON_TAC[]);
    TYPIFY `{p,u0,u1} = {u0,u1,p}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    ASM_SIMP_TAC[COLLINEAR_3_IN_AFFINE_HULL];
    TYPIFY `affine hull {u0,u1} SUBSET aff_ge {u0,u1} {v1}` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    MATCH_MP_TAC AFFINE_HULL_SUBSET_AFF_GE;
    BY(ASM_SIMP_TAC[Fan.th3a]);
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM_ST `mcell` MP_TAC;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[NOT_FORALL_THM];
  REPEAT WEAK_STRIP_TAC;
  GEXISTL_TAC [`p`;`q`];
  FIRST_X_ASSUM MP_TAC;
  EXPAND_TAC "X'";
  FIRST_X_ASSUM_ST `X = mcell i V ul` SUBST1_TAC;
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let WEDGE_SUBSET_WEDGE_GE = 
prove_by_refinement(
  `!u0 u1 u2 u3. wedge u0 u1 u2 u3 SUBSET wedge_ge u0 u1 u2 u3`,

  (* {{{ proof *)
  [
  REWRITE_TAC[wedge;SUBSET;Local_lemmas.WEDGE_GE_AZIM_LE;IN_ELIM_THM];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let AFF_INTER_IMP_COPLANAR = 
prove_by_refinement(
  `!a b c (d:real^3).  ~(affine hull {a,b} INTER affine hull {c,d} ={}) ==>
    coplanar {a,b,c,d}`,

  (* {{{ proof *)
  [
  REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY];
  REWRITE_TAC[AFFINE_HULL_2_ALT;IN_ELIM_THM;IN_UNIV;NOT_FORALL_THM];
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[coplanar];
  ASM_CASES_TAC `u = &0`;
    GEXISTL_TAC [`b`;`c`;`d`];
    TYPIFY `{b,c,d} SUBSET affine hull {b,c,d} /\  a IN affine hull {b,c,d}` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    REWRITE_TAC[HULL_SUBSET];
    REWRITE_TAC[AFFINE_HULL_3;IN_ELIM_THM];
    GEXISTL_TAC [`&0`;`&1 - u'`;`u'`];
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    BY(REPEAT (FIRST_X_ASSUM_ST `%` MP_TAC) THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
  GEXISTL_TAC [`a`;`c`;`d`];
  TYPIFY `{a,c,d} SUBSET affine hull {a,c,d} /\  b IN affine hull {a,c,d}` ENOUGH_TO_SHOW_TAC;
    BY(SET_TAC[]);
  REWRITE_TAC[HULL_SUBSET];
  REWRITE_TAC[AFFINE_HULL_3;IN_ELIM_THM];
  GEXISTL_TAC [`(u - &1)/ u`;`(&1 - u')/ u`;`u' / u`];
  CONJ_TAC;
    Calc_derivative.CALC_ID_TAC;
    BY(ASM_REWRITE_TAC[]);
  MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP;
  TYPIFY `u` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC];
  TYPIFY `!x. u * x  / u = x` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    GEN_TAC;
    Calc_derivative.CALC_ID_TAC;
    BY(ASM_REWRITE_TAC[]);
  BY(REPEAT (FIRST_X_ASSUM_ST `%` MP_TAC) THEN VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let NOT_COLLINEAR_AFF_DIM2 = 
prove_by_refinement(
  `!(a:real^A) b c. ~collinear {a,b,c} ==> aff_dim {a,b,c} = &2`,

  (* {{{ proof *)
  [
  REWRITE_TAC[COLLINEAR_AFF_DIM];
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC AFF_DIM_3 [`a`;`b`;`c`];
  BY(FIRST_X_ASSUM MP_TAC THEN INT_ARITH_TAC)
  ]);;
  (* }}} *)

let ADD_NN_ZERO = 
prove_by_refinement(
  `!a b x y.  &0 < a /\ &0 < b /\ &0 <= x /\ &0 <= y /\ a * x + b * y = &0 ==> (x = &0 /\ y = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM_ST `+` (MP_TAC o (MATCH_MP (arith `x + y = &0 ==> (~(&0 <= x) \/ ~(&0 <= y) \/ (x = &0 /\ y = &0))`)));
  REPEAT WEAK_STRIP_TAC;
      FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[];
      GMATCH_SIMP_TAC REAL_LE_MUL;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[];
    GMATCH_SIMP_TAC REAL_LE_MUL;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
  REWRITE_TAC[REAL_ENTIRE];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let BDXKHTW = 
prove_by_refinement(
  `!u0 u1 v1 v2 V X. saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\
    X IN mcell_set V /\
    {u0,u1} IN edgeX V X /\
    ~(azim u0 u1 v1 v2 = &0) /\ (?y. y IN X INTER wedge u0 u1 v1 v2) ==>
    (X SUBSET wedge_ge u0 u1 v1 v2)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  PROOF_BY_CONTR_TAC;
  INTRO_TAC BDXKHTW_PREP_LEMMA [`u0`;`u1`;`v1`;`v2`;`V`;`X`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[SUBSET]);
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC CONNECTED_SEGMENT_NOT_COVERED [`wedge u0 u1 v1 v2`;`(:real^3) DIFF wedge_ge u0 u1 v1 v2`;`p`;`q`];
  ANTS_TAC;
    ASM_SIMP_TAC[OPEN_WEDGE;CLOSED_WEDGE;GSYM closed];
    REWRITE_TAC[TAUT `(a /\ b /\ c) = ((a /\ b) /\ c)`];
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
    BY(SET_TAC[WEDGE_SUBSET_WEDGE_GE]);
  REWRITE_TAC[IN_DIFF;IN_UNIV];
  REPEAT WEAK_STRIP_TAC;
  COMMENT "x IN X";
  TYPIFY `x IN X` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `segment [p,q] SUBSET X` ENOUGH_TO_SHOW_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
    FIRST_X_ASSUM_ST `convex` MP_TAC;
    REWRITE_TAC[ CONVEX_CONTAINS_SEGMENT];
    BY(REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC) THEN SET_TAC[]);
  COMMENT "x IN aff_ge";
  TYPIFY `?v. leaf V [u0;u1;v] /\ ~collinear {u0,u1,v} /\ x IN aff_ge {u0,u1} {v} /\ ~(p IN aff_ge {u0,u1} {v}) /\ ~(q IN aff_ge {u0,u1} {v})` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v1`;`v2`];
    ASM_REWRITE_TAC[];
    REPEAT (FIRST_X_ASSUM_ST `UNION` MP_TAC);
    REWRITE_TAC[SUBSET;IN_UNION];
    BY(ASM_MESON_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  COMMENT "non degeneracies";
  TYPIFY `~(x = p) /\ ~(x = q)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
  FIRST_X_ASSUM_ST `segment` MP_TAC;
  REWRITE_TAC[closed_segment;IN_ELIM_THM];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(p = q)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `DIFF` MP_TAC;
    FIRST_X_ASSUM_ST `INTER` MP_TAC;
    BY(SET_TAC[WEDGE_SUBSET_WEDGE_GE]);
  TYPIFY `&0 < u` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_SIMP_TAC[arith `&0 <= u ==> (&0 < u <=> ~(u= &0))`];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `%` MP_TAC;
    BY(ASM_REWRITE_TAC[varith `(&1 - &0) % p + &0 % q = (p:real^3)`]);
  TYPIFY `u < &1` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_SIMP_TAC[arith `u <= &1 ==> (u < &1 <=> ~(u= &1))`];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `%` MP_TAC;
    BY(ASM_REWRITE_TAC[varith `(&1 - &1) % p + &1 % q = (q:real^3)`]);
  COMMENT "x not in aff {u0,u1}";
  TYPIFY `~(x IN affine hull {u0,u1})` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM_ST `coplanar` MP_TAC;
    REWRITE_TAC[];
    MATCH_MP_TAC AFF_INTER_IMP_COPLANAR;
    ASM_REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;NOT_FORALL_THM];
    TYPIFY `x` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[AFFINE_HULL_2_ALT;IN_ELIM_THM;IN_UNIV];
    TYPIFY `u` EXISTS_TAC;
    BY(VECTOR_ARITH_TAC);
  COMMENT "x in aff_gt";
  TYPIFY `x IN aff_gt {u0,u1} {v}` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `DISJOINT {u0,u1} {v}` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_SIMP_TAC[Fan.th3a]);
    REPLICATE_TAC 5 (FIRST_X_ASSUM_ST `IN` MP_TAC);
    ASM_SIMP_TAC[Collect_geom.IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF];
    BY(MESON_TAC[Sphere.aff]);
  COMMENT "introduce cc";
  TYPIFY `?ul. leaf V ul /\ X = cc_cell V ul /\ stem ul = {u0,u1} /\ cc_A0 ul = aff_gt {u0,u1} {v} /\ set_of_list ul = {u0,u1,v} ` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC CFFONNL [`V`;`[u0;u1;v]`;`X`];
    ASM_REWRITE_TAC[];
    REWRITE_TAC[TAUT `(a /\ b /\ ~c ==> d) <=> (a /\ b ==> (c \/ d))`];
    ANTS_TAC;
      ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;cc_A0];
      REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY;NOT_FORALL_THM];
      TYPIFY `x` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
    DISCH_THEN DISJ_CASES_TAC;
      TYPIFY `[u0;u1;v]` EXISTS_TAC;
      ASM_REWRITE_TAC[cc_A0;EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;set_of_list3_explicit];
      GMATCH_SIMP_TAC STEM_OF_LEAF;
      REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
      BY(ASM_MESON_TAC[]);
    TYPIFY `[u1;u0;v]` EXISTS_TAC;
    ASM_REWRITE_TAC[cc_A0;EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;set_of_list3_explicit];
    INTRO_TAC ZASUVOR [`V`;`u0`;`u1`;`v`];
    ASM_REWRITE_TAC[];
    REPEAT WEAK_STRIP_TAC;
    ASM_REWRITE_TAC[];
    CONJ2_TAC;
      CONJ2_TAC;
        BY(SET_TAC[]);
      AP_THM_TAC THEN AP_TERM_TAC;
      BY(SET_TAC[]);
    GMATCH_SIMP_TAC STEM_OF_LEAF;
    ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
    CONJ2_TAC;
      BY(SET_TAC[]);
    BY(ASM_MESON_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  COMMENT "introduce chi_msb";
  INTRO_TAC CELL_NN [`V`;`ul`;`p`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `INTER` MP_TAC;
    ASM_REWRITE_TAC[];
    BY(SET_TAC[]);
  DISCH_TAC;
  INTRO_TAC CELL_NN [`V`;`ul`;`q`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `DIFF` MP_TAC;
    ASM_REWRITE_TAC[];
    BY(SET_TAC[]);
  DISCH_TAC;
  COMMENT "chi x = 0";
  INTRO_TAC AFFINE_IMP_CHI_MSB_0 [`ul`;`x`];
  ANTS_TAC;
    CONJ_TAC;
      BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
    REPEAT (FIRST_X_ASSUM_ST `aff_gt` MP_TAC);
    ASM_REWRITE_TAC[];
    TYPIFY ` {u0,u1,v} = {u0,u1} UNION {v} ` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    TYPIFY `aff_gt {u0, u1} {v} SUBSET affine hull ({u0, u1} UNION {v})` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    BY(MESON_TAC[AFF_GT_SUBSET_AFFINE_HULL]);
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC CHI_MSB_ADDITIVE;
  CONJ_TAC;
    BY(REAL_ARITH_TAC);
  DISCH_TAC;
  FIRST_X_ASSUM_ST `coplanar` MP_TAC;
  REWRITE_TAC[coplanar];
  GEXISTL_TAC [`u0`;`u1`;`v`];
  TYPIFY `p IN affine hull {u0,u1,v} /\ q IN affine hull {u0,u1,v} /\  {u0,u1,v} SUBSET affine hull {u0,u1,v}` ENOUGH_TO_SHOW_TAC;
    BY(SET_TAC[]);
  REWRITE_TAC[HULL_SUBSET];
  FIRST_X_ASSUM_ST `x = {a,b,c}` (SUBST1_TAC o SYM);
  REPEAT (GMATCH_SIMP_TAC COPLANAR_INSERT);
  COMMENT "fresh start";
  REPEAT (GMATCH_SIMP_TAC set_of_list3);
  TYPIFY `!p. {p,EL 0 ul, EL 1 ul, EL 2 ul} = {EL 0 ul, EL 1 ul, EL 2 ul,p}` (C SUBGOAL_THEN (unlist ONCE_REWRITE_TAC));
    BY(SET_TAC[]);
  REWRITE_TAC[CHI_MSB_COPLANAR];
  REPEAT (GMATCH_SIMP_TAC NOT_COLLINEAR_AFF_DIM2);
  TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  TYPIFY `set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_SIMP_TAC[set_of_list3]);
  CONJ_TAC;
    BY(ASM_MESON_TAC[GBEWYFX]);
  ASM_REWRITE_TAC[];
  TYPIFY ` [EL 0 ul;EL 1 ul;EL 2 ul] = ul` ((C SUBGOAL_THEN SUBST1_TAC));
    BY(ASM_SIMP_TAC[ GSYM LENGTH3]);
  MATCH_MP_TAC (TAUT `a /\ b  ==> b /\ a`);
  MATCH_MP_TAC ADD_NN_ZERO;
  GEXISTL_TAC [`(&1 - u)`;`u`];
  BY(ASM_SIMP_TAC[arith `u < &1 ==> &0 < &1 - u`])
  ]);;
  (* }}} *)

let AZIM_POS_IMP_SUM_2PI_ALT = 
prove_by_refinement(
  `!a b c d. 
    &0 < azim a b c d ==> azim a b c d + azim a b d c = &2 * pi
  `,

  (* {{{ proof *)
  [
    MESON_TAC[Local_lemmas1.AZIM_POS_IMP_SUM_2PI]
  ]);;
  (* }}} *)

let WEDGE_GE_COMPLEMENT = 
prove_by_refinement(
  `!u0 u1 v1 v2. 
    ~(azim u0 u1 v1 v2 = &0) ==>
    (:real^3) DIFF wedge_ge u0 u1 v1 v2 = wedge u0 u1 v2 v1`,

  (* {{{ proof *)
  [
  REWRITE_TAC[EXTENSION;wedge;Local_lemmas.WEDGE_GE_AZIM_LE;IN_DIFF;IN_UNIV;IN_ELIM_THM];
  REWRITE_TAC[arith `~(x <= y) <=> (y < x)`];
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(collinear {u0,u1,v1}) /\ ~collinear {u0,u1,v2}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[AZIM_DEGENERATE]);
  TYPIFY `collinear {u0,u1,x}` ASM_CASES_TAC;
    ASM_REWRITE_TAC[];
    ASM_SIMP_TAC[AZIM_DEGENERATE;arith `~(x < &0) <=> &0 <= x`];
    BY(REWRITE_TAC[Local_lemmas.AZIM_RANGE]);
  ASM_REWRITE_TAC[];
  TYPIFY `&0 < azim u0 u1 v1 v2` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_SIMP_TAC[arith `~(x = &0) ==> (&0 < x <=> &0 <= x)`;Local_lemmas.AZIM_RANGE]);
  REWRITE_TAC[TAUT `(a <=> b) <=> ((a ==> b) /\ (b ==> a))`];
  CONJ_TAC;
    REPEAT WEAK_STRIP_TAC;
    INTRO_TAC Fan.sum4_azim_fan [`u0`;`u1`;`v1`;`v2`;`x`];
    ASM_SIMP_TAC[arith `x < y ==> x <= y`];
    INTRO_TAC AZIM_POS_IMP_SUM_2PI_ALT [`u0`;`u1`;`v1`;`v2`];
    INTRO_TAC Local_lemmas.AZIM_RANGE [`u0`;`u1`;`v1`;`x`];
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  REPEAT WEAK_STRIP_TAC;
  INTRO_TAC Fan.sum4_azim_fan [`u0`;`u1`;`v2`;`x`;`v1`];
  ASM_SIMP_TAC[arith `x < y ==> x <= y`];
  INTRO_TAC AZIM_POS_IMP_SUM_2PI_ALT [`u0`;`u1`;`v2`;`v1`];
  INTRO_TAC AZIM_POS_IMP_SUM_2PI_ALT [`u0`;`u1`;`x`;`v1`];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let WEDGE_COMPLEMENT = 
prove_by_refinement(
  `!u0 u1 v1 v2. ~(azim u0 u1 v1 v2 = &0) ==>
    (:real^3) DIFF wedge u0 u1 v1 v2 = wedge_ge u0 u1 v2 v1`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(azim u0 u1 v2 v1 = &0)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.AZIM_EQ_0_SYM2]);
  INTRO_TAC WEDGE_GE_COMPLEMENT [`u0`;`u1`;`v2`;`v1`];
  ASM_REWRITE_TAC[];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let EWYBJUA = 
prove_by_refinement(
  `!u0 u1 v1 v2 V X. saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\
    X IN mcell_set V /\
    {u0,u1} IN edgeX V X /\
    ~(azim u0 u1 v1 v2 = &0)  ==>
    (X SUBSET wedge_ge u0 u1 v1 v2) \/ (X SUBSET wedge_ge u0 u1 v2 v1)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(X INTER wedge u0 u1 v1 v2 = {})` ASM_CASES_TAC;
    DISJ1_TAC;
    MATCH_MP_TAC BDXKHTW;
    TYPIFY `V` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
  TYPIFY `~(X INTER  wedge u0 u1 v2 v1 = {})` ASM_CASES_TAC;
    DISJ2_TAC;
    MATCH_MP_TAC BDXKHTW;
    TYPIFY `V` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      BY(ASM_MESON_TAC[Local_lemmas.AZIM_EQ_0_SYM2]);
    BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
  DISJ1_TAC;
  TYPIFY `~collinear {u0,u1,v1}` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC GBEWYFX [`V`;`[u0;u1;v1]`];
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC set_of_list3;
    ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  TYPIFY `~collinear {u0,u1,v2}` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC GBEWYFX [`V`;`[u0;u1;v2]`];
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC set_of_list3;
    ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
    BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
  TYPIFY `NULLSET X` ASM_CASES_TAC;
    FIRST_X_ASSUM_ST `mcell_set` MP_TAC;
    REWRITE_TAC[Pack_defs.mcell_set;IN_ELIM_THM];
    REPEAT WEAK_STRIP_TAC;
    INTRO_TAC Bump.RIJRIED [`V`;`ul`;`i`];
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    DISCH_TAC;
    BY(ASM_MESON_TAC[NOT_IN_EMPTY]);
  ABBREV_TAC `(s:real^3->bool) = aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}`;
  TYPIFY `NULLSET s` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "s";
    MATCH_MP_TAC (CONJUNCT2 NULLSET_RULES);
    BY(ASM_SIMP_TAC[Conforming.NEGLIGIBLE_AFF_GE_2_1]);
  TYPIFY `X SUBSET aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}` ASM_CASES_TAC;
    BY(ASM_MESON_TAC[NEGLIGIBLE_SUBSET]);
  TYPIFY `?x. x IN X DIFF s` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM MP_TAC;
    EXPAND_TAC "s";
    BY(SET_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `~collinear t` MP_TAC;
    BY(MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
  TYPIFY `collinear {u0,u1,x}` ASM_CASES_TAC;
    INTRO_TAC COLLINEAR_3_IN_AFFINE_HULL [`u0`;`u1`;`x`];
    ASM_REWRITE_TAC[];
    TYPIFY `affine hull {u0,u1} SUBSET aff_ge {u0,u1} {v1}` ENOUGH_TO_SHOW_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
    MATCH_MP_TAC AFFINE_HULL_SUBSET_AFF_GE;
    MATCH_MP_TAC Fan.th3a;
    BY(ASM_REWRITE_TAC[]);
  REPEAT (FIRST_X_ASSUM_ST `INTER` MP_TAC);
  REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY];
  (DISCH_THEN (C INTRO_TAC [`x`]));
  FIRST_X_ASSUM_ST `DIFF` MP_TAC;
  REWRITE_TAC[IN_DIFF];
  DISCH_TAC;
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `x IN wedge_ge u0 u1 v2 v1` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC WEDGE_COMPLEMENT [`u0`;`u1`;`v1`;`v2`];
    ASM_REWRITE_TAC[EXTENSION;IN_DIFF;IN_UNIV];
    BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
  (DISCH_THEN (C INTRO_TAC [`x`]));
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v2`;`v1`];
  ASM_REWRITE_TAC[];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
  ]);;
  (* }}} *)

end;;