(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Conclusions                                                       *)
(* Chapter: Local Fan                                                         *)
(* Lemma: ZLZTHIC                                                             *)
(* Author: Thomas Hales                                                       *)
(* Date: 2013-07-10                                                           *)
(* ========================================================================== *)



module Zlzthic = struct

  open Hales_tactic;;


let FOR_ASM th =
  let th1 = REWRITE_RULE[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] th in
  let th2 = SPEC_ALL th1 in 
    UNDISCH_ALL th2;;

let ASSUME_TAC2 = ASSUME_TAC o FOR_ASM;;
let DOWN = FIRST_X_ASSUM MP_TAC;;
let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;
let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (SPEC_ALL ( tm ))];;
let SWITCH_TAC tm = UNDISCH_TAC tm THEN DISCH_THEN (ASSUME_TAC o GSYM);;
let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `; MESON[]` a ==> b ==> c <=> a /\ b ==> c `];;



let NONCOLLINEAR_OPEN = Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR;;

let NONPLANAR_OPEN = 
prove_by_refinement(
  `!(v1:real->real^3) v2 v3 v4 t. ~coplanar {v1 t,v2 t,v3 t, v4 t} /\
    v1 continuous atreal t /\ v2 continuous atreal t /\ v3 continuous atreal t /\ 
    v4 continuous atreal t
    ==>
       (?e. &0 < e /\ !t'. abs(t - t') < e ==>  ~coplanar {v1 t', v2 t' ,v3 t',v4 t'})`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Oxlzlez.coplanar_delta_y];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `(\t. delta_y (dist (v1 t,v2 t)) (dist (v1 t,v3 t))               (dist (v1 t,v4 t))               (dist (v3 t,v4 t))               (dist (v2 t,v4 t))               (dist (v2 t,v3 t))) real_continuous atreal t` ENOUGH_TO_SHOW_TAC;
    REWRITE_TAC[real_continuous_atreal];
    DISCH_THEN (C INTRO_TAC [`delta_y (dist (v1 t,v2 t)) (dist (v1 t,v3 t)) (dist (v1 t,v4 t))      (dist (v3 t,v4 t))      (dist (v2 t,v4 t))      (dist (v2 t,v3 t))`]);
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `d` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`t'`]);
    ASM_REWRITE_TAC[];
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[Sphere.delta_y;Sphere.delta_x];
  BY((REPEAT ( (MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE MATCH_MP_TAC REAL_CONTINUOUS_SUB ORELSE MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE MATCH_MP_TAC REAL_CONTINUOUS_NEG ORELSE MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON2_REDO) THEN (REPEAT CONJ_TAC))) THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let COLL_IFF_COLL_CROSS2 = 
prove_by_refinement(
  `!v w. collinear {vec 0, v, w} <=> collinear {vec 0, w, v cross w}`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `s = {vec 0,v,w}`;
  (ONCE_REWRITE_TAC[CROSS_SKEW]);
  ONCE_REWRITE_TAC[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`];
  (REWRITE_TAC[arith `-- (u:real^3) = (-- &1) % u`]);
  GMATCH_SIMP_TAC COLLINEAR_SPECIAL_SCALE;
  (ONCE_REWRITE_TAC[SET_RULE `{vec 0,a,(b:real^3)} = {vec 0,b,a}`]);
  RULE_ASSUM_TAC( ONCE_REWRITE_RULE[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`]);
  REWRITE_TAC[arith` ~( -- &1 = &0)`];
  BY(ASM_MESON_TAC([Local_lemmas.COLL_IFF_COLL_CROSS]))
  ]);;
  (* }}} *)

let azim_cross_0 = 
prove_by_refinement(
  `!v w. ~(collinear {vec 0,v,w}) ==> ~(azim (vec 0) (v cross w) v w = &0)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;Local_lemmas.NOT_COLL_IMP_COPL;SET_RULE `{vec 0,v,w,v cross w} = {vec 0,v cross w,v,(w:real^3)}`])
  ]);;
  (* }}} *)

let wedge_ge_cross = 
prove_by_refinement(
  `!v w. ~collinear {vec 0,v,w} ==> wedge_ge (vec 0) (v cross w) v w = aff_ge {vec 0, v cross w} {v, w}`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  GMATCH_SIMP_TAC Local_lemmas.WEDGE_GE_EQ_AFF_GE;
  CONJ_TAC;
    TYPIFY `&0 < sin(azim (vec 0) (v cross w) v w)` ENOUGH_TO_SHOW_TAC;
      REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`];
      STRIP_TAC;
      CONJ_TAC;
        REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT];
        BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
      BY(ASM_MESON_TAC[SIN_PI;arith `~(&0 < &0)`]);
    REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS];
    ONCE_REWRITE_TAC[CROSS_TRIPLE];
    BY(ASM_REWRITE_TAC[DOT_POS_LT;CROSS_EQ_0]);
  ONCE_REWRITE_TAC[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`];
  BY(ASM_MESON_TAC[COLL_IFF_COLL_CROSS2;Local_lemmas.COLL_IFF_COLL_CROSS])
  ]);;
  (* }}} *)

let azim_lt_pi_cross = 
prove_by_refinement(
  `!u1 u2 u3. (&0 < azim (vec 0) u1 u2 u3 /\ azim(vec 0) u1 u2 u3 < pi) <=> &0 < (u1 cross u2) dot u3`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Trigonometry.JBDNJJB [`u1`;`u2`;`u3`];
  ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
  REWRITE_TAC[Trigonometry2.re_eqvl];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  ASM_CASES_TAC `&0 < sin(azim(vec 0) u1 u2 u3)`;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`];
    REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT];
    ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
    CONJ2_TAC;
      DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
      BY(ASM_MESON_TAC[SIN_PI;arith `~(&0 < &0)`]);
    BY(ASM_MESON_TAC[Counting_spheres.AZIM_NN;SIN_0;arith `&0 < x <=> &0 <= x /\ ~(x = &0)`;arith `~(&0 < &0)`]);
  COMMENT "other direction";
  TYPED_ABBREV_TAC `s = sin (azim (vec 0) u1 u2 u3)`;
  REWRITE_TAC[arith `&0 < t * s <=> ~(&0 <= t* (-- s))`];
  GMATCH_SIMP_TAC REAL_LE_MUL;
  CONJ_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `~` MP_TAC;
  EXPAND_TAC "s";
  REWRITE_TAC[];
  BY(ASM_MESON_TAC[SIN_POS_PI])
  ]);;
  (* }}} *)

let generic_alt = 
prove_by_refinement(
  `!u v w. ~collinear {vec 0,v,w} /\ ~(u = vec 0) ==>
     (aff_ge {vec 0} {v,w} INTER aff_lt {vec 0} {u} = {} <=> 
      ~coplanar {vec 0,u,v,w} \/ ((-- u) IN wedge (vec 0) (v cross w) w v))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a = b)`);
  CONJ_TAC THEN STRIP_TAC;
      MATCH_MP_TAC (TAUT `(a ==> b ) ==> (~a \/ b)`);
      DISCH_TAC;
      GMATCH_SIMP_TAC (GSYM Leaf_cell.WEDGE_GE_COMPLEMENT);
      REWRITE_TAC[IN_DIFF;IN_UNIV];
      ASM_SIMP_TAC[azim_cross_0];
      ASM_SIMP_TAC[wedge_ge_cross];
      COMMENT "down to three";
      GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2;
      REWRITE_TAC[IN_ELIM_THM;arith `t1 % (vec 0):real^3 = vec 0`];
      CONJ_TAC;
        TYPIFY `DISJOINT  {v, w} {vec 0} /\ ~(v cross w = v) /\ ~(v cross w = w)` ENOUGH_TO_SHOW_TAC;
          REWRITE_TAC[DISJOINT];
          BY(SET_TAC[]);
        CONJ_TAC;
          MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
          BY(ASM_REWRITE_TAC[]);
        REWRITE_TAC[CROSS_EQ_SELF];
        BY(CONJ_TAC THEN ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,(v:real^3),vec 0} = {vec 0,v} /\ {vec 0,vec 0,(w:real^3)} = {vec 0,w}`]);
      REPEAT WEAKER_STRIP_TAC;
      RULE_ASSUM_TAC( REWRITE_RULE[arith `-- (u:real^3) = w <=> u = -- w`] );
      FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
      REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;NOT_FORALL_THM];
      TYPIFY `-- (u:real^3)` EXISTS_TAC;
      CONJ2_TAC;
        GMATCH_SIMP_TAC AFF_LT_1_1;
        REWRITE_TAC[IN_ELIM_THM;DISJOINT];
        CONJ_TAC;
          BY(ASM_TAC THEN SET_TAC[]);
        GEXISTL_TAC [`&2`;`-- &1`];
        BY(REPEAT CONJ_TAC THEN TRY REAL_ARITH_TAC THEN VECTOR_ARITH_TAC);
      RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas.CROSS_DOT_COPLANAR]);
      RULE_ASSUM_TAC(ONCE_REWRITE_RULE[CROSS_TRIPLE]);
      FIRST_X_ASSUM_ST `x = &0` MP_TAC;
      ASM_REWRITE_TAC[];
      REWRITE_TAC[DOT_RNEG;DOT_RADD;DOT_RMUL];
      REWRITE_TAC[DOT_RZERO];
      REWRITE_TAC[DOT_CROSS_SELF];
      (REWRITE_TAC[arith `--(&0 + t2 * a + t3 * &0 + t4 * &0) = &0 <=> t2 * a = &0`]);
      REWRITE_TAC[REAL_ENTIRE];
      ASM_SIMP_TAC[DOT_POS_LT;CROSS_EQ_0;arith `&0 < x ==> ~(x = &0)`];
      DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
      REWRITE_TAC[arith `-- --(vec 0 + &0 % a + b + (c:real^3)) = b + c`];
      GMATCH_SIMP_TAC AFF_GE_1_2;
      CONJ_TAC;
        ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
        BY(ASM_REWRITE_TAC[]);
      REWRITE_TAC[IN_ELIM_THM];
      GEXISTL_TAC [`t1`;`t3`;`t4`];
      ASM_REWRITE_TAC[];
      CONJ_TAC;
        BY(ASM_TAC THEN REAL_ARITH_TAC);
      BY(VECTOR_ARITH_TAC);
    COMMENT "second case";
    REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER];
    GMATCH_SIMP_TAC AFF_GE_1_2;
    CONJ_TAC;
      ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
      BY(ASM_REWRITE_TAC[]);
    REWRITE_TAC[IN_ELIM_THM];
    GMATCH_SIMP_TAC Nkezbfc_local.AFF_LT_1_1;
    ASM_REWRITE_TAC[IN_ELIM_THM];
    REPEAT WEAKER_STRIP_TAC;
    RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas.CROSS_DOT_COPLANAR]);
    RULE_ASSUM_TAC(ONCE_REWRITE_RULE[CROSS_TRIPLE]);
    TYPIFY `(v cross w) dot (t1 % vec 0 + t2 % v + t3 % w) = (v cross w) dot (t1' % vec 0 + t2' % u)` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[DOT_RNEG;DOT_RADD;DOT_RMUL;DOT_RZERO;DOT_CROSS_SELF];
    TYPIFY `~(t2' * ((v cross w) dot u) = &0)` ENOUGH_TO_SHOW_TAC;
      BY(REAL_ARITH_TAC);
    ASM_REWRITE_TAC[REAL_ENTIRE];
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "third and final case";
  REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER];
  GMATCH_SIMP_TAC AFF_GE_1_2;
  CONJ_TAC;
    ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
    BY(ASM_REWRITE_TAC[]);
  REWRITE_TAC[IN_ELIM_THM];
  GMATCH_SIMP_TAC Nkezbfc_local.AFF_LT_1_1;
  ASM_REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `x IN wedge (vec 0) (v cross w) w v` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `wedge` MP_TAC;
    REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM];
    FIRST_X_ASSUM SUBST1_TAC;
    TYPIFY `t1' % vec 0 + t2' % u = (-- t2') % (-- u)` (C SUBGOAL_THEN SUBST1_TAC);
      BY(VECTOR_ARITH_TAC);
    FIRST_X_ASSUM_ST `t < &0` MP_TAC;
    BY(MESON_TAC[AZIM_SCALE_ALL;arith `&0 < &1`;arith `t < &0 ==> &0 < -- t`;arith `&1 % (v:real^3) = v`]);
  FIRST_X_ASSUM_ST `x = y` kill;
  TYPIFY `~(x IN wedge (vec 0) (v cross w) w v)` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC (GSYM Leaf_cell.WEDGE_GE_COMPLEMENT);
    (REWRITE_TAC[IN_DIFF;IN_UNIV]);
    ASM_SIMP_TAC[azim_cross_0];
    ASM_SIMP_TAC[wedge_ge_cross];
    GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2;
    REWRITE_TAC[IN_ELIM_THM];
    CONJ_TAC;
      TYPIFY `DISJOINT  {v, w} {vec 0} /\ ~(v cross w = v) /\ ~(v cross w = w)` ENOUGH_TO_SHOW_TAC;
        REWRITE_TAC[DISJOINT];
        BY(SET_TAC[]);
      CONJ_TAC;
        MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
        BY(ASM_REWRITE_TAC[]);
      REWRITE_TAC[CROSS_EQ_SELF];
      BY(CONJ_TAC THEN ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,(v:real^3),vec 0} = {vec 0,v} /\ {vec 0,vec 0,(w:real^3)} = {vec 0,w}`]);
    GEXISTL_TAC [`t1`;`&0`;`t2`;`t3`];
    REPEAT CONJ_TAC THEN ASM_TAC THEN TRY REAL_ARITH_TAC;
    BY(REPEAT WEAKER_STRIP_TAC THEN VECTOR_ARITH_TAC);
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let vuy1 = 
prove_by_refinement(
  `!v u0 u1.
        ~collinear {vec 0,u0,v} /\ ~collinear {vec 0,u0,u1} /\ v IN aff_ge {vec 0,u0} {u1} ==> 
    (?t0 t1. &0 < t1 /\ v = t0 % u0 + t1 % u1)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
  GMATCH_SIMP_TAC AFF_GE_2_1;
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  ASM_SIMP_TAC[Fan.th3a];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  GEXISTL_TAC [`t2`;`t3`];
  CONJ_TAC;
    PROOF_BY_CONTR_TAC;
    TYPIFY `t3 = &0` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    TYPIFY `v = t2 % u0` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
    DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]);
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let DISJOINT_PAIR = 
prove_by_refinement(
  `!a b c. DISJOINT a {b,c} <=> DISJOINT a {b} /\ DISJOINT a {c}`,

  (* {{{ proof *)
  [
  REWRITE_TAC[DISJOINT];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let vuy2 = 
prove_by_refinement(
  `!v u0 u1.
         ~collinear {vec 0, u0, v} /\
         ~collinear {vec 0, u0, u1} /\
         v IN aff_ge {vec 0, u0} {u1} ==>
       (u0 cross u1) dot v = &0`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC vuy1 [`v`;`u0`;`u1`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_CROSS_SELF];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let vuy3 = 
prove_by_refinement(
  `!v u0 u1. ~collinear {vec 0, u0, v} /\
         ~collinear {vec 0, u0, u1} /\
         v IN aff_ge {vec 0, u0} {u1} ==>
    ~collinear {vec 0,u0 cross u1, v}`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  DISCH_TAC;
  REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM];
  SUBCONJ_TAC;
    BY(ASM_REWRITE_TAC[CROSS_EQ_0]);
  ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC vuy1 [`v`;`u0`;`u1`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `v dot v = c % (u0 cross u1) dot (t0 % u0 + t1 % u1)` (C SUBGOAL_THEN MP_TAC);
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[DOT_RMUL;DOT_LMUL;DOT_RADD;DOT_CROSS_SELF];
  TYPIFY ` c * (t0 * &0 + t1 * &0) = &0` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[DOT_EQ_0];
  DISCH_TAC;
  BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,u0,vec 0} = {vec 0,(u0:real^3)}`])
  ]);;
  (* }}} *)

let vuy4 = 
prove_by_refinement(
  `!v u0 u1. ~collinear {vec 0, u0, v} /\
         ~collinear {vec 0, u0, u1} /\
         v IN aff_ge {vec 0, u0} {u1} ==>
    azim (vec 0) (u0 cross u1) u0 v < pi`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `&0 < ((u0 cross u1) cross u0) dot v` ENOUGH_TO_SHOW_TAC;
    BY(MESON_TAC[azim_lt_pi_cross]);
  INTRO_TAC vuy1 [`v`;`u0`;`u1`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  ONCE_REWRITE_TAC[CROSS_TRIPLE];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[CROSS_RMUL;DOT_LMUL;CROSS_RADD;DOT_CROSS_SELF;CROSS_REFL;arith `t % vec 0 + (a:real^3) = a`];
  GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
  BY(ASM_REWRITE_TAC[DOT_POS_LT;CROSS_EQ_0])
  ]);;
  (* }}} *)

let vuy5 = 
prove_by_refinement(
  `!v u0 u1. 
         ~collinear {vec 0, u0, u1} ==>
    u0 IN aff_ge {vec 0,u0} {u1}`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  GMATCH_SIMP_TAC AFF_GE_2_1;
  ASM_SIMP_TAC[Fan.th3a];
  REWRITE_TAC[IN_ELIM_THM];
  GEXISTL_TAC [`&0`;`&1`;`&0`];
  REPEAT CONJ_TAC THEN TRY REAL_ARITH_TAC;
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let cross_independent = 
prove_by_refinement(
  `!u0 u1 a b c. ~collinear {vec 0,u0,u1} /\
    a % (u0 cross u1) + b % u0 + c % u1 = vec 0 ==> a = &0`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY ` (u0 cross  u1) dot ( (--b) % u0 + (--c) % u1 ) = a * ((u0 cross u1) dot (u0 cross u1))` (C SUBGOAL_THEN MP_TAC);
    REWRITE_TAC[GSYM DOT_RMUL];
    TYPIFY `a % (u0 cross u1)  = -- b % u0 + -- c % u1` ENOUGH_TO_SHOW_TAC;
      BY(MESON_TAC[]);
    BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
  REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_RZERO;DOT_CROSS_SELF];
  REWRITE_TAC[arith `-- b * &0 + -- c * &0 = x <=> x = &0`];
  REWRITE_TAC[REAL_ENTIRE;DOT_EQ_0];
  BY(ASM_REWRITE_TAC[CROSS_EQ_0])
  ]);;
  (* }}} *)

let ybt_inj = 
prove_by_refinement(
  `!u0 u1 v1 v2 .   ~collinear {vec 0, u0, v1} /\ 
    ~collinear {vec 0, u0, v2} /\
         ~collinear {vec 0, u0, u1} /\ ~collinear {vec 0,v1,v2} /\
         v1 IN aff_ge {vec 0, u0} {u1} /\          v2 IN aff_ge {vec 0, u0} {u1} ==>
~(    azim (vec 0) (u0 cross u1) u0 v1 = azim (vec 0) (u0 cross u1) u0 v2)
     `,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Topology.th [`(vec 0):real^3`;`u0 cross u1`;`u0`;`v2`];
  REWRITE_TAC[EXTENSION;IN_ELIM_THM];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    ASM_SIMP_TAC[vuy3];
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`];
    BY(ASM_MESON_TAC[Local_lemmas.COLL_IFF_COLL_CROSS]);
  DISCH_THEN (C INTRO_TAC [`v1`]);
  ASM_SIMP_TAC[vuy3];
  DISCH_TAC;
  INTRO_TAC vuy1 [`v1`;`u0`;`u1`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `aff_gt` MP_TAC;
  REWRITE_TAC[];
  GMATCH_SIMP_TAC AFF_GT_2_1;
  CONJ_TAC;
    REWRITE_TAC[DISJOINT;EXTENSION;IN_INTER;IN_SING;IN_INSERT;NOT_IN_EMPTY];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    FIRST_X_ASSUM DISJ_CASES_TAC;
      FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
      BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,a}= {a,(b:real^3)}`]);
    FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
    REWRITE_TAC[];
    GMATCH_SIMP_TAC AFF_GE_2_1;
    ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `(-- &1) % (u0 cross u1) + t2 % u0 + t3 % u1 = vec 0` (C SUBGOAL_THEN MP_TAC);
      BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
    BY(ASM_MESON_TAC[cross_independent;arith `~(-- &1 = &0)`]);
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `v1 = t3 % v2` ENOUGH_TO_SHOW_TAC;
    DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    BY(ASM_MESON_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`;COLLINEAR_LEMMA_ALT]);
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
  REWRITE_TAC[];
  GMATCH_SIMP_TAC AFF_GE_2_1;
  ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `x:real^3` (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
  FIRST_X_ASSUM_ST `v1 = t1' % ((vec 0):real^3) + c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
  RULE_ASSUM_TAC(REWRITE_RULE[VECTOR_MUL_ASSOC;VECTOR_ADD_LDISTRIB]);
  TYPIFY `t2 % (u0 cross u1) + (t3 * t2' - t0) % u0 + (t3*t3' - t1) % u1 = vec 0` (C SUBGOAL_THEN MP_TAC);
    REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `x:real^3` MP_TAC);
    ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
    DISCH_TAC;
    BY(VECTOR_ARITH_TAC);
  DISCH_TAC;
  TYPIFY `t2 = &0` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[cross_independent]);
  FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
  FIRST_X_ASSUM kill;
  FIRST_X_ASSUM_ST `x:real^3` MP_TAC;
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

let ybt_inj_0 = 
prove_by_refinement(
  `!u0 u1 v2 .   
    ~collinear {vec 0, u0, v2} /\
         ~collinear {vec 0, u0, u1} /\ 
         v2 IN aff_ge {vec 0, u0} {u1} ==>
~(      azim (vec 0) (u0 cross u1) u0 v2 = &0)
     `,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  GMATCH_SIMP_TAC Local_lemmas.AZIM_EQ_0_GE_ALT2;
  CONJ_TAC;
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`];
    BY(ASM_MESON_TAC[Local_lemmas.COLL_IFF_COLL_CROSS]);
  GMATCH_SIMP_TAC AFF_GE_2_1;
  CONJ_TAC;
    REWRITE_TAC[DISJOINT;EXTENSION;IN_INTER;IN_SING;IN_INSERT;NOT_IN_EMPTY];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    FIRST_X_ASSUM DISJ_CASES_TAC;
      FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
      BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b}= {a,(b:real^3)}`]);
    TYPIFY `u0 dot u0 = (u0 cross u1) dot u0` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[DOT_CROSS_SELF];
    REWRITE_TAC[DOT_EQ_0];
    DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b}= {a,(b:real^3)}`]);
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
  REWRITE_TAC[];
  GMATCH_SIMP_TAC AFF_GE_2_1;
  ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `t2 % (u0 cross u1) + (t3 - t2') % u0 + (-- t3') % u1 = vec 0` (C SUBGOAL_THEN MP_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
  DISCH_TAC;
  TYPIFY `t2 = &0` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[cross_independent]);
  FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
  REPLICATE_TAC 4 (FIRST_X_ASSUM kill);
  TYPIFY `v2 = t3 % u0` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
  FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
  BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT])
  ]);;
  (* }}} *)

let ECAU_aff_ge = 
prove_by_refinement(
  `!(u:num->real^3) r. (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\
     (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} )  ==> 
  (!i. 1 <= i /\ i <= r ==> u i IN aff_ge {vec 0,u 0 } {u 1} )  `,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `u i IN aff_gt {vec 0,u 0} {u 1}` (C SUBGOAL_THEN MP_TAC);
    ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
    BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  INTRO_TAC AFF_GT_SUBSET_AFF_GE [`{vec 0,u 0}`;`{u 1}`];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let collinear_cross = 
prove_by_refinement(
  `!u i r. i <= r /\ 1 <= r /\ (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\
     (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) 
  ==> ~collinear {vec 0,u 0 cross u 1,u i}`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[];
  TYPIFY `i = 0` ASM_CASES_TAC;
    ASM_REWRITE_TAC[];
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
    REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_TAC THEN ARITH_TAC);
  INTRO_TAC ECAU_aff_ge [`u`;`r`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  MATCH_MP_TAC vuy3;
  BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN TRY ARITH_TAC)
  ]);;
  (* }}} *)

let YBTASCZ1 = 
prove_by_refinement(
  `!u r j.
    (j <= r) /\ (1<= r) /\
    (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\
    (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\
    cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\
    (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==>
    (!i. i < j ==> azim (vec 0) ((u 0) cross (u 1)) (u 0) (u i) < azim (vec 0) (u 0 cross (u 1)) (u 0) (u j))
    `,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  DISCH_TAC;
  INTRO_TAC ECAU_aff_ge [`u`;`r`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INDUCT_TAC;
    DISCH_TAC;
    REWRITE_TAC[arith `a < b <=> (a <= b /\ ~(a = b))`];
    CONJ_TAC;
      BY(REWRITE_TAC[AZIM_REFL;Local_lemmas.AZIM_RANGE]);
    REWRITE_TAC[AZIM_REFL];
    ONCE_REWRITE_TAC[EQ_SYM_EQ];
    MATCH_MP_TAC ybt_inj_0;
    ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
    BY(REPEAT CONJ_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_TAC THEN TRY ARITH_TAC);
  COMMENT "induction step";
  ONCE_REWRITE_TAC[arith `a < b <=> ~(b < a) /\ ~(a = b)`];
  REPEAT WEAKER_STRIP_TAC;
  CONJ2_TAC;
    MATCH_MP_TAC ybt_inj;
    ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
    BY(REPEAT CONJ_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_TAC THEN TRY ARITH_TAC);
  DISCH_TAC;
  TYPIFY `i < (j:num)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) = u (i+1)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_TAC THEN ARITH_TAC);
  INTRO_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`{u i | (i:num) <= r}`;`u i`;`u 0 cross u 1`;`(vec 0):real^3`];
  ANTS_TAC;
    CONJ_TAC;
      REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_SING];
      TYPIFY `1 <= r` (C SUBGOAL_THEN MP_TAC);
        BY(ASM_REWRITE_TAC[]);
      TYPIFY (`~(u 0 = u 1)`) ENOUGH_TO_SHOW_TAC;
        BY(MESON_TAC[arith `1 <= r ==> 0 <= r /\ 1 <= r`]);
      DISCH_TAC;
      FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]);
      ANTS_TAC;
        BY(ASM_TAC THEN ARITH_TAC);
      ASM_REWRITE_TAC[];
      BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}= {a,(b:real^3)}`]);
    TYPIFY `{u i | i <= r } = IMAGE u {i | i <= (r:num)}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    MATCH_MP_TAC FINITE_IMAGE;
    BY(REWRITE_TAC[FINITE_NUMSEG_LE]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`u j`]);
  ANTS_TAC;
    CONJ_TAC;
      DISCH_TAC;
      FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`j`;`i`]);
      ANTS_TAC;
        BY(ASM_TAC THEN ARITH_TAC);
      ASM_REWRITE_TAC[];
      BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}= {a,(b:real^3)}`]);
    TYPIFY_GOAL_THEN `(j:num) <=r ==> {u i | i <= r} (u j)` MATCH_MP_TAC;
      TYPIFY `{u i | i <= r } = IMAGE u {i | i <= (r:num)}` (C SUBGOAL_THEN SUBST1_TAC);
        BY(SET_TAC[]);
      REWRITE_TAC[IMAGE;IN_ELIM_THM];
      BY(MESON_TAC[]);
    BY(ASM_TAC THEN ARITH_TAC);
  REWRITE_TAC[arith `i+1 = SUC i`];
  REWRITE_TAC[DE_MORGAN_THM];
  PROOF_BY_CONTR_TAC;
  COMMENT "shift";
  FIRST_X_ASSUM_ST `(i:num) < j ==> b` MP_TAC;
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  FIRST_ASSUM MP_TAC;
  REWRITE_TAC[];
  ONCE_REWRITE_TAC[arith `a < b <=> &0 < b - a`];
  GMATCH_SIMP_TAC Leaf_cell.AZIM_BASE_SHIFT_LE;
  TYPIFY `u i` EXISTS_TAC;
  (ASM_SIMP_TAC[arith `x <= x` ;arith `x < y ==> x <= y`]);
  CONJ_TAC;
    BY(REPEAT (GMATCH_SIMP_TAC collinear_cross) THEN REPEAT CONJ_TAC THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC);
  REWRITE_TAC[arith `&0 < a - b <=> b < a`];
  DISCH_TAC;
  COMMENT "second shift";
  TYPIFY `azim (vec 0) (u 0 cross u 1) (u i) (u j) <      azim (vec 0) (u 0 cross u 1) (u i) (u (SUC i))` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `SUC` kill;
    FIRST_ASSUM_ST `SUC` MP_TAC;
    ONCE_REWRITE_TAC[arith `a < b <=> &0 < b - a`];
    MATCH_MP_TAC (arith `a = b ==> &0 < a ==> &0 < b`);
    MATCH_MP_TAC Leaf_cell.AZIM_BASE_SHIFT_LE;
    (ASM_SIMP_TAC[arith `x <= x` ;arith `x < y ==> x <= y`]);
    REWRITE_TAC[TAUT `(a /\ b /\ c) <=> ((a /\ b) /\ c)`];
    CONJ2_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    BY(REPEAT (GMATCH_SIMP_TAC collinear_cross) THEN REPEAT CONJ_TAC THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let YBTASCZ2 = 
prove_by_refinement(
  `!u r i j.
    (i < j) /\ (j <= r) /\ (1<= r) /\
    (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\
    (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\
    cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\
    (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==>
    (azim (vec 0) ((u 0) cross (u 1)) (u i) (u j) < pi)
    `,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC YBTASCZ1 [`u`;`r`;`j`];
  ASM_REWRITE_TAC[];
  DISCH_THEN (C INTRO_TAC [`i`]);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC Fan.sum4_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`;`u j`];
  ANTS_TAC;
    ASM_SIMP_TAC[arith `x < y ==> x <= y`];
    BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC collinear_cross THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC);
  INTRO_TAC vuy4 [`u j`;`u 0`;`u 1`];
  ANTS_TAC;
    INTRO_TAC ECAU_aff_ge [`u`;`r`];
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN ARITH_TAC);
  INTRO_TAC Counting_spheres.AZIM_NN [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let YBTASCZ3 = 
prove_by_refinement(
  `!u r i j.
    (i < j) /\ (j <= r) /\ (1<= r) /\
    (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\
    (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\
    cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\
    (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==>
    (&0 < azim (vec 0) ((u 0) cross (u 1)) (u i) (u j))
    `,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC YBTASCZ1 [`u`;`r`;`j`];
  ASM_REWRITE_TAC[];
  DISCH_THEN (C INTRO_TAC [`i`]);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC Fan.sum4_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`;`u j`];
  ANTS_TAC;
    ASM_SIMP_TAC[arith `x < y ==> x <= y`];
    BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC collinear_cross THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC);
  BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let KCZXLLE = 
prove_by_refinement(
  `!u r i j k.
    (j < k) /\ (k <= r) /\ (1<= r) /\ (i <= r) /\ ((i < j \/ k < i)) /\
    (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\
    (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\
    cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\
    (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==>
    (azim (vec 0) (u i) (u j) (u k) = &0)
    `,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?r. j < k /\     k <= r /\     1 <= r /\     (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\     (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0, u 0} {u 1}) /\     cyclic_set {u i | i <= r} (vec 0) (u 0 cross u 1) /\     (!i. i < r          ==> azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) =              u (i + 1))` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `r` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  INTRO_TAC ECAU_aff_ge [`u`;`r`] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC;
  COMMENT "planarity";
  TYPIFY `!i. i <= r ==> u i IN affine hull {vec 0,u 0,u 1}` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    ASM_CASES_TAC `i' = 0`;
      MATCH_MP_TAC HULL_INC;
      ASM_REWRITE_TAC[];
      BY(SET_TAC[]);
    RULE_ASSUM_TAC(REWRITE_RULE[arith `~(i=0) <=> 1<= i`]);
    REWRITE_TAC[GSYM Trigonometry.UIVNNRR2];
    INTRO_TAC (GEN_ALL Local_lemmas.AFF_GT_MONO) [`{vec 0,u 0}`;`{u 1}`;`{u 1}`];
    ANTS_TAC;
      BY(SET_TAC[]);
    TYPIFY_GOAL_THEN `{vec 0,u 0} UNION {u 1} = {vec 0,u 0,u 1} /\ {u 1} DIFF {u 1} = {}` (unlist REWRITE_TAC);
      BY(SET_TAC[]);
    TYPIFY `u i' IN aff_gt {vec 0, u 0} {u 1}` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  COMMENT "ARITH GOES HERE";
  TYPIFY `j <= (r:num)` (C SUBGOAL_THEN ASSUME_TAC);
    REPLICATE_TAC 10 (FIRST_X_ASSUM kill);
    BY(ASM_TAC THEN ARITH_TAC);
  TYPIFY `~(i = j) /\ ~(i = k) /\ 0 <= r` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPLICATE_TAC 6 (FIRST_X_ASSUM kill) THEN ASM_TAC THEN ARITH_TAC);
  TYPIFY `~(0 = k) /\ (1 <= k) /\ ~(0=1)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM kill) THEN ASM_TAC THEN ARITH_TAC);
  COMMENT "other prelims here";
  TYPIFY `~collinear {vec 0, u 0, u 1} /\ ~collinear {vec 0,u i,u j} /\ ~collinear {vec 0,u i,u k}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[arith `~(0=1)`]);
  TYPIFY `DISJOINT {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC Fan.th3a;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~collinear {vec 0, u 0, u k} /\ ~collinear {vec 0, u 0, u 1} /\ u k IN aff_ge {vec 0, u 0} {u 1} /\ u k IN aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC);
    BY((REPEAT CONJ_TAC) THEN (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
  TYPIFY `!i. i <= r ==> ~collinear {vec 0,u 0 cross u 1, u i}` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    ASM_CASES_TAC `i' = 0`;
      FIRST_X_ASSUM_ST `collinear` MP_TAC;
      ASM_REWRITE_TAC[];
      ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
      REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS];
      BY(ASM_REWRITE_TAC[]);
    RULE_ASSUM_TAC (ONCE_REWRITE_RULE[arith `~(i'=0) <=> (1 <= i' /\ ~(i' = 0))`]);
    FIRST_X_ASSUM_ST `collinear` MP_TAC;
    REWRITE_TAC[];
    MATCH_MP_TAC vuy3;
    BY((REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]));
  COMMENT "standard";
  TYPIFY `coplanar {vec 0, u i, u j, u k}` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[coplanar];
    GEXISTL_TAC [`(vec 0):real^3`;`u 0`;`u 1`];
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN (FIRST_X_ASSUM MATCH_MP_TAC ORELSE MATCH_MP_TAC HULL_INC) THEN ASM_REWRITE_TAC[];
    BY(REPEAT WEAKER_STRIP_TAC THEN SET_TAC[]);
  RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR]);
  FIRST_X_ASSUM DISJ_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  PROOF_BY_CONTR_TAC THEN FIRST_X_ASSUM kill;
  INTRO_TAC (GEN_ALL Ldurdpn.LDURDPN) [`u i`;`u j`;`u k`];
  ANTS_TAC;
    BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  REWRITE_TAC[DE_MORGAN_THM];
  DISJ2_TAC;
  TYPIFY `conv0 {u j,u k} SUBSET aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_CASES_TAC `j=0`;
      ASM_REWRITE_TAC[Geomdetail.CONV0_SET2;SUBSET;IN_ELIM_THM];
      REPEAT WEAKER_STRIP_TAC;
      GMATCH_SIMP_TAC AFF_GT_2_1;
      ASM_REWRITE_TAC[IN_ELIM_THM];
      INTRO_TAC vuy1 [`u k`;`u 0`;`u 1`];
      ANTS_TAC;
        BY(ASM_REWRITE_TAC[]);
      REPEAT WEAKER_STRIP_TAC;
      ASM_REWRITE_TAC[];
      GEXISTL_TAC [`&1 - a - b * (t0 + t1)`;`a + b * t0`;`b*t1`];
      GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
      ASM_REWRITE_TAC[];
      CONJ_TAC;
        BY(REAL_ARITH_TAC);
      BY(VECTOR_ARITH_TAC);
    COMMENT "~(j=0)";
    MATCH_MP_TAC SUBSET_TRANS;
    TYPIFY `conv {u j,u k}` EXISTS_TAC;
    REWRITE_TAC[Geomdetail.CONV02_SU_CONV2];
    MATCH_MP_TAC Geomdetail.CONVEX_IM_CONV2_SU;
    ASM_REWRITE_TAC[CONVEX_AFF_GT];
    RULE_ASSUM_TAC(REWRITE_RULE[arith `~(j=0) <=> 1<=j`]);
    BY( FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INTER;NOT_IN_EMPTY];
  REWRITE_TAC[TAUT `~(a /\ b) <=> (b ==> ~a)`];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `aff` MP_TAC;
  REWRITE_TAC[Trigonometry2.AFF2_VEC0;IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `k' % u i IN aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN MP_TAC);
    BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  REWRITE_TAC[];
  GMATCH_SIMP_TAC AFF_GT_2_1;
  ASM_REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(i = 0)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM_ST `%` MP_TAC;
    ASM_REWRITE_TAC[];
    TYPIFY `~collinear {vec 0, u 0, u 1}` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_REWRITE_TAC[]);
    REWRITE_TAC[COLLINEAR_LEMMA_ALT];
    REWRITE_TAC[DE_MORGAN_THM;NOT_EXISTS_THM];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`(inv t3 * (k' - t2))`]);
    REWRITE_TAC[];
    TYPIFY `t3 % u 1 = t3 % (inv t3 * (k' - t2)) % u 0` ENOUGH_TO_SHOW_TAC;
      REWRITE_TAC[VECTOR_MUL_LCANCEL];
      DISCH_THEN DISJ_CASES_TAC;
        BY(FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)) THEN FIRST_X_ASSUM_ST `&0 < &0` MP_TAC THEN REAL_ARITH_TAC);
      BY(FIRST_X_ASSUM ACCEPT_TAC);
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[VECTOR_MUL_ASSOC];
    TYPIFY `(t3 * inv t3 * (k' - t2)) = k' - t2` (C SUBGOAL_THEN SUBST1_TAC);
      Calc_derivative.CALC_ID_TAC;
      BY(FIRST_X_ASSUM_ST `&0 < t3` MP_TAC THEN REAL_ARITH_TAC);
    BY(VECTOR_ARITH_TAC);
  TYPIFY `?t. &0 < t /\ x = t % u i` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM_ST `aff_gt` (C INTRO_TAC [`i`]);
    (ANTS_TAC);
      BY(RULE_ASSUM_TAC(REWRITE_RULE[arith `~(i=0) <=> 1 <= i`]) THEN ASM_REWRITE_TAC[]);
    GMATCH_SIMP_TAC AFF_GT_2_1;
    ASM_REWRITE_TAC[IN_ELIM_THM];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `k'` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    TYPIFY `k' = t3/ t3'` ENOUGH_TO_SHOW_TAC;
      DISCH_THEN SUBST1_TAC;
      GMATCH_SIMP_TAC REAL_LT_DIV;
      BY(ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    TYPIFY `t3 = k' * t3'` ENOUGH_TO_SHOW_TAC;
      DISCH_THEN SUBST1_TAC;
      Calc_derivative.CALC_ID_TAC;
      BY((FIRST_X_ASSUM_ST `&0 < t` MP_TAC) THEN REAL_ARITH_TAC);
    PROOF_BY_CONTR_TAC;
    TYPIFY `(k'*t2' - t2) % u 0 + (k'*t3' - t3) % u 1 = vec 0` (C SUBGOAL_THEN MP_TAC);
      BY(FIRST_X_ASSUM_ST `%` MP_TAC THEN VECTOR_ARITH_TAC);
    DISCH_TAC;
    TYPIFY `inv (k' * t3' - t3) % (k' * t3' - t3) % u 1 = inv(k' * t3' - t3) % (t2 - k' * t2') % u 0` (C SUBGOAL_THEN ASSUME_TAC);
      REWRITE_TAC[VECTOR_MUL_LCANCEL];
      DISJ2_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[VECTOR_MUL_ASSOC];
    TYPIFY `inv (k' * t3' - t3) * (k' * t3' - t3) = &1` (C SUBGOAL_THEN SUBST1_TAC);
      Calc_derivative.CALC_ID_TAC;
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    REWRITE_TAC[VECTOR_MUL_LID];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]);
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]);
  REPEAT WEAKER_STRIP_TAC;
  (COMMENT "wedge");
  TYPIFY `conv0 {u j,u k}  SUBSET wedge (vec 0) (u 0 cross u 1) (u j) (u k)` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `wedge (vec 0) (u 0 cross u 1) (u j) (u k) = aff_gt {vec 0,u 0 cross u 1} {u j,u k}` ENOUGH_TO_SHOW_TAC;
      DISCH_THEN SUBST1_TAC;
      REWRITE_TAC[CONV0_AFF_GT];
      MATCH_MP_TAC AFF_GT_MONO_LEFT;
      BY(SET_TAC[]);
    MATCH_MP_TAC WEDGE_LUNE_GT;
    TYPIFY_GOAL_THEN `~collinear {vec 0, u 0 cross u 1, u j}` (unlist REWRITE_TAC);
      ASM_CASES_TAC `j= 0`;
        ASM_REWRITE_TAC[];
        ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
        REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS];
        FIRST_X_ASSUM MATCH_MP_TAC;
        BY(ASM_REWRITE_TAC[]);
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[]);
    CONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[]);
    GMATCH_SIMP_TAC YBTASCZ3;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC YBTASCZ2;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `x IN wedge (vec 0) (u 0 cross u 1) (u j) (u k)` (C SUBGOAL_THEN MP_TAC);
    BY(REPEAT (FIRST_X_ASSUM_ST `conv0` MP_TAC) THEN SET_TAC[]);
  REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM];
  FIRST_X_ASSUM_ST `x = (y:real^3)` SUBST1_TAC;
  TYPIFY `azim (vec 0) (u 0 cross u 1) (u j) (t % u i) = azim (vec 0) (u 0 cross u 1) (u j) (u i)` (C SUBGOAL_THEN SUBST1_TAC);
    FIRST_X_ASSUM_ST `&0 < t` MP_TAC;
    BY(MESON_TAC[AZIM_SCALE_ALL;arith `&0 < &1`;arith `&1 % v = v`]);
  COMMENT "two cases";
  REWRITE_TAC[DE_MORGAN_THM];
  DISJ2_TAC;
  FIRST_X_ASSUM DISJ_CASES_TAC;
    REWRITE_TAC[arith `~(a < b) <=> b <= a`];
    MATCH_MP_TAC REAL_LE_TRANS;
    TYPIFY `pi` EXISTS_TAC;
    SUBCONJ_TAC;
      MATCH_MP_TAC (arith `x < pi ==> x <= pi`);
      MATCH_MP_TAC YBTASCZ2;
      EXISTS_TAC `r:num`;
      BY(ASM_REWRITE_TAC[]);
    DISCH_TAC;
    ONCE_REWRITE_TAC[Rogers.AZIM_COMPL_EXT];
    COND_CASES_TAC;
      TYPIFY `&0 < azim  (vec 0) (u 0 cross u 1) (u i) (u j)` ENOUGH_TO_SHOW_TAC;
        BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
      MATCH_MP_TAC YBTASCZ3;
      TYPIFY `r` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    MATCH_MP_TAC (arith `x < pi ==> pi <= &2 * pi - x`);
    MATCH_MP_TAC YBTASCZ2;
    EXISTS_TAC `r:num`;
    BY(ASM_REWRITE_TAC[]);
  COMMENT "last case";
  REWRITE_TAC[arith `~(a < b) <=> b <= a`];
  INTRO_TAC Fan.sum3_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u j`;`u k`;`u i`];
  ANTS_TAC;
    CONJ_TAC;
      MATCH_MP_TAC (arith `x < pi /\ y < pi ==> x + y < &2 * pi`);
      CONJ_TAC THEN (MATCH_MP_TAC YBTASCZ2);
        TYPIFY `r` EXISTS_TAC;
        BY(ASM_REWRITE_TAC[]);
      TYPIFY `r` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `&0 <=  azim (vec 0) (u 0 cross u 1) (u k) (u i)` ENOUGH_TO_SHOW_TAC;
    BY(REAL_ARITH_TAC);
  BY(REWRITE_TAC[Counting_spheres.AZIM_NN])
  ]);;
  (* }}} *)

let KCZXLLE_SYM = 
prove_by_refinement(
  `!u r i j k.
         k <= r /\
         j <= r /\
         1 <= r /\
         i <= r /\
         ((j < k /\ (i < j \/ k < i)) \/ (k < j /\ (i < k \/ j < i))) /\
         (!i j.
              i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\
         (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0, u 0} {u 1}) /\
         cyclic_set {u i | i <= r} (vec 0) (u 0 cross u 1) /\
         (!i. i < r
              ==> azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) =
                  u (i + 1))
         ==> azim (vec 0) (u i) (u j) (u k) = &0`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM DISJ_CASES_TAC;
    MATCH_MP_TAC KCZXLLE;
    TYPIFY `r` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  ONCE_REWRITE_TAC[Local_lemmas.AZIM_EQ_0_SYM2];
  MATCH_MP_TAC KCZXLLE;
  TYPIFY `r` EXISTS_TAC;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let open_continuous_eps = 
prove_by_refinement(
  `!U f t a b. (t IN real_interval (a,b)) /\ f t IN U /\
		(!x. x IN real_interval (a,b) ==> f real_continuous atreal x) /\ real_open U ==> 
   (?e. &0 < e /\ (!x. abs (x-t) < e ==> f x IN U))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Pent_hex.continuous_preimage_open [`f`;`real_interval (a,b)`;`U`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(ASM_SIMP_TAC[ Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT ]);
  REWRITE_TAC[real_open;IN_ELIM_THM];
  DISCH_THEN (C INTRO_TAC [`t`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let coplanar_in_affine_hull = 
prove_by_refinement(
  `!(u:real^A) v w x. ~collinear {u,v,w} /\ coplanar {x,u,v,w} ==> x IN affine hull {u,v,w}`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Counting_spheres.NOT_COLLINEAR_AFF_DIM_2 [`u`;`v`;`w`];
  ASM_REWRITE_TAC[] THEN DISCH_TAC;
  MATCH_MP_TAC Leaf_cell.COPLANAR_INSERT;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let azim_0_as_closed = 
prove_by_refinement(
  `!(v2:real^3) v3 v4. ~collinear {vec 0, v2,v3} /\ ~collinear {vec 0,v2,v4} ==>
    (azim (vec 0) v2 v3 v4 = &0 <=> (coplanar {vec 0,v2,v3,v4} /\ &0 <= ((v2 cross v3) cross v2) dot v4))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~coplanar {vec 0,v2,v3,v4}` ASM_CASES_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[]) THEN ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[AZIM_EQ_0_PI_IMP_COPLANAR]);
  INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`v2`;`v3`;`v4`];
  ANTS_TAC;
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,c,d,a}`];
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`v2`;`v3`;`v4`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `&0 <= ((v2 cross v3) cross v2) dot v4 <=> &0 <= t2` (C SUBGOAL_THEN SUBST1_TAC);
    ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL];
    ONCE_REWRITE_TAC[CROSS_TRIPLE];
    REWRITE_TAC[CROSS_REFL;DOT_LZERO];
    REWRITE_TAC[arith `t1 * &0 + c = c`];
    GMATCH_SIMP_TAC (CONJUNCT2 REAL_LE_MUL_EQ);
    REWRITE_TAC[DOT_POS_LT];
    BY(ASM_REWRITE_TAC[CROSS_EQ_0]);
  TYPIFY `azim (vec 0) v2 v3 v4 = &0 <=> ~(azim (vec 0) v2 v3 v4 = pi)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(ASM_MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;PI_POS;arith `&0 < pi ==> ~(&0 = pi)`]);
  GMATCH_SIMP_TAC Ldurdpn.LDURDPN;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  TYPIFY_GOAL_THEN `(?A. plane A /\ {vec 0, v2, v3, v4} SUBSET A)` (unlist REWRITE_TAC);
    FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `affine hull {vec 0,v2,v3}` EXISTS_TAC;
    CONJ2_TAC;
      TYPIFY `v4 IN affine hull {vec 0,v2,v3} /\ {vec 0 ,v2,v3} SUBSET affine hull {vec 0,v2,v3}` ENOUGH_TO_SHOW_TAC;
        BY(SET_TAC[]);
      BY(CONJ_TAC THEN ASM_MESON_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL]);
    REWRITE_TAC[plane];
    BY(ASM_MESON_TAC[]);
  ASM_REWRITE_TAC[];
  REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY];
  REWRITE_TAC[Trigonometry2.AFF2_VEC0;IN_ELIM_THM;Geomdetail.CONV0_SET2;DE_MORGAN_THM;NOT_EXISTS_THM];
  TYPIFY `(!x. (!k. ~(x = k % v2)) \/      (!a b.           ~(&0 < a) \/           ~(&0 < b) \/           ~(a + b = &1) \/           ~(x = a % v3 + b % (t1 % v2 + t2 % v3)))) <=> (!k a b. &0 < a /\ &0 < b /\ a + b = &1 ==> ~(k % v2 = a % v3 + b % (t1 % v2 + t2 % v3)))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(MESON_TAC[]);
  COMMENT "first case";
  ASM_CASES_TAC `&0 <= t2`;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `v3 = (inv (b * t2  + a) * (-- (b * t1 - k))) % v2` ENOUGH_TO_SHOW_TAC;
      BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]);
    MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP;
    TYPIFY `(b * t2 + a)` EXISTS_TAC;
    SUBCONJ_TAC;
      MATCH_MP_TAC (arith `&0 <= b' /\ &0 < a ==> ~(b' + a = &0)`);
      GMATCH_SIMP_TAC REAL_LE_MUL;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[VECTOR_MUL_ASSOC];
    DISCH_TAC;
    TYPIFY `((b * t2 + a) * inv (b * t2 + a) * --(b * t1 - k))  = -- (b * t1 - k)` (C SUBGOAL_THEN SUBST1_TAC);
      Calc_derivative.CALC_ID_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
    BY(FIRST_X_ASSUM_ST `%` MP_TAC THEN VECTOR_ARITH_TAC);
  ASM_REWRITE_TAC[NOT_FORALL_THM];
  TYPIFY `~(t2 = &1)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  GEXISTL_TAC [`t1 / (&1 - t2)`;`-- t2 / (&1 - t2)`;`&1 / (&1 - t2)`;];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    GMATCH_SIMP_TAC REAL_LT_DIV;
    GMATCH_SIMP_TAC REAL_LT_DIV;
    TYPIFY `--t2 / (&1 - t2) + &1 / (&1 - t2) = &1` (C SUBGOAL_THEN SUBST1_TAC);
      Calc_derivative.CALC_ID_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[];
  TYPIFY `&1 / (&1 - t2) % (t1 % v2 + t2 % v3) = t1 / (&1 - t2) % v2 - --t2 / (&1 - t2) % v3` ENOUGH_TO_SHOW_TAC;
    DISCH_THEN SUBST1_TAC;
    BY(VECTOR_ARITH_TAC);
  REWRITE_TAC[VECTOR_ADD_LDISTRIB];
  REWRITE_TAC[VECTOR_MUL_ASSOC];
  TYPIFY `(&1 / (&1 - t2) * t1) = t1 / (&1 - t2)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REAL_ARITH_TAC);
  BY(VECTOR_ARITH_TAC)
  ]);;
  (* }}} *)

(*
let CONTINUOUS_LIFT_DOT2 = prove
 (`!net f:A->real^N g.                                                     
        f continuous net /\ g continuous net
        ==> (\x. lift(f x dot g x)) continuous net`,
  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (MATCH_MP (REWRITE_RULE
   [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`]
  BILINEAR_CONTINUOUS_COMPOSE) BILINEAR_DOT)) THEN REWRITE_TAC[]);;

let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
  `!(f:real->real^A) g x.  f continuous atreal x /\ g continuous atreal x
            ==> (\x. (f x dot g x)) real_continuous atreal x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
  INTRO_TAC CONTINUOUS_AT_LIFT_DOT2 [`f o drop`;`g o drop`;`lift x`];
  TYPIFY `(\x. lift ((f o drop) x dot (g o drop) x)) = (\x. lift (f x dot g x)) o drop` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
  BY(ASM_REWRITE_TAC[GSYM (* Xbjrphc. *) CONTINUOUS_CONTINUOUS_ATREAL])
  ]);;
  (* }}} *)
*)

let REAL_CONTINUOUS_AT_DOT2 = 
prove_by_refinement(
  `!(f:real->real^A) g x.  f continuous atreal x /\ g continuous atreal x
            ==> (\x. (f x dot g x)) real_continuous atreal x`,

  (* {{{ proof *)
  [
  REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
  MATCH_MP_TAC CONTINUOUS_LIFT_DOT2;
  ASM_REWRITE_TAC[];
  ]);;
  (* }}} *)

let azim_pos_open = 
prove_by_refinement(
  `!v2 v3 v4 t a b.     (!x. x IN real_interval (a,b) ==> v2 continuous (atreal x)) /\
    (!x. x IN real_interval (a,b) ==> v3 continuous (atreal x)) /\
    (!x. x IN real_interval (a,b) ==> v4 continuous (atreal x)) /\
    t IN real_interval(a,b) /\
    ~collinear {(vec 0) ,(v2 t) ,(v3 t)}  /\ ~collinear {(vec 0), (v2 t), (v4 t)} /\
    ~(azim (vec 0) (v2 t) (v3 t) (v4 t) = &0) ==>
  (?e. &0 < e /\ (!t'. abs(t' - t) < e ==> ~(azim (vec 0) (v2 t') (v3 t') (v4 t') = &0)))
 `,

  (* {{{ proof *)
  [
  REWRITE_TAC[real_open;IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN ) [`t`;`(vec 0):real^3`;`v2`;`v3`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN ) [`t`;`(vec 0):real^3`;`v2`;`v4`];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC azim_0_as_closed [`v2 t`;`v3 t`;`v4 t`];
  ASM_REWRITE_TAC[DE_MORGAN_THM];
  DISCH_TAC;
  TYPIFY `?e. &0 < e /\ (!t'. abs(t - t') < e ==> (~coplanar {vec 0, v2 t', v3 t', v4 t'} \/ ~(&0 <= ((v2 t' cross v3 t') cross v2 t') dot v4 t')))` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM DISJ_CASES_TAC;
      INTRO_TAC NONPLANAR_OPEN [`\(t:real). ((vec 0):real^3)`;`v2`;`v3`;`v4`;`t`];
      ANTS_TAC;
        ASM_REWRITE_TAC[CONTINUOUS_CONST];
        BY(ASM_MESON_TAC[]);
      REWRITE_TAC[];
      BY(MESON_TAC[]);
    TYPIFY `(\t. ((v2 t cross v3 t) cross v2 t) dot -- (v4 t)) real_continuous_on ( real_interval(a,b) )` (C SUBGOAL_THEN ASSUME_TAC);
      GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
      REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC REAL_CONTINUOUS_AT_DOT2;
      CONJ2_TAC;
        MATCH_MP_TAC CONTINUOUS_NEG;
        BY(ASM_MESON_TAC[]);
      MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS;
      CONJ2_TAC;
        BY(ASM_MESON_TAC[]);
      MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS;
      BY(ASM_MESON_TAC[]);
    INTRO_TAC Pent_hex.continuous_preimage_open [`(\x. ((v2 x cross v3 x) cross v2 x) dot -- v4 x)`;`real_interval(a,b)`;`{u | &0 < u}`];
    ANTS_TAC;
      ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
      BY(REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`]);
    REWRITE_TAC[IN_ELIM_THM];
    REWRITE_TAC[real_open;DOT_RNEG;arith `&0 < -- x <=> ~(&0 <= x)`;IN_ELIM_THM];
    DISCH_THEN (C INTRO_TAC [`t`]);
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(MESON_TAC[arith `abs (x' - t) < e <=> abs (t - x') < e`]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?e'''. e''' <= e /\ e''' <= e' /\ e''' <= e'' /\ &0 < e'''` (C SUBGOAL_THEN MP_TAC);
    TYPIFY `if (e'' <= e' /\ e'' <= e) then e'' else (if (e' <= e'' /\ e' <= e) then e' else e)` EXISTS_TAC;
    BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e'''` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  GEN_TAC;
  DISCH_TAC;
  GMATCH_SIMP_TAC azim_0_as_closed;
  REWRITE_TAC[DE_MORGAN_THM];
  BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN TRY REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let azim_real_continuous_on = 
prove_by_refinement(
  `!v2 v3 v4 t a b.
    (!x. x IN real_interval (a,b) ==> v2 continuous (atreal x)) /\
    (!x. x IN real_interval (a,b) ==> v3 continuous (atreal x)) /\
    (!x. x IN real_interval (a,b) ==> v4 continuous (atreal x)) /\
    t IN real_interval(a,b) /\
    ~collinear {(vec 0) ,(v2 t) ,(v3 t)}  /\ ~collinear {(vec 0), (v2 t), (v4 t)} /\
    ~(azim (vec 0) (v2 t) (v3 t) (v4 t)  = &0) ==>
    (?e. &0 < e /\ (\q. azim (vec 0) (v2 q) (v3 q) (v4 q)) real_continuous_on (real_interval (t - e, t+ e)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`t`;`(vec 0):real^3`;`v2`;`v3`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`t`;`(vec 0):real^3`;`v2`;`v4`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC azim_pos_open [`v2`;`v3`;`v4`;`t`;`a`;`b`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?e'''.  &0 < e''' /\ (!x. t - e''' < x /\ x < t + e''' ==> x IN real_interval (a,b))` (C SUBGOAL_THEN MP_TAC);
    TYPIFY `if (b-t <= t -a) then b -  t else t - a` EXISTS_TAC;
    FIRST_X_ASSUM_ST `IN` MP_TAC;
    REWRITE_TAC[IN_REAL_INTERVAL];
    BY(REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?e''''. e'''' <= e /\ e'''' <= e' /\ e'''' <= e'' /\ e'''' <= e''' /\ &0 < e''''` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e,e',e'',e'''}`];
    ANTS_TAC;
      CONJ_TAC;
        BY(MESON_TAC[FINITE_RULES]);
      BY(SET_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `m` EXISTS_TAC;
    RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT;NOT_IN_EMPTY]);
    REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN (REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC));
    BY(MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e''''` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
  REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;IN_REAL_INTERVAL];
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE;
  ASM_REWRITE_TAC[CONTINUOUS_CONST];
  GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
  TYPIFY `x IN real_interval (a,b)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN (REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC)) THEN TRY REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let azim_pos_iff_nz = 
prove_by_refinement(
  `!v1 v2 v3 v4.
    &0 < azim v1 v2 v3 v4 <=> ~(azim v1 v2 v3 v4 = &0)`,

  (* {{{ proof *)
  [
  BY(MESON_TAC[Counting_spheres.AZIM_NN;arith `&0 < x <=> (&0 <= x /\ ~(x = &0))`])
  ]);;
  (* }}} *)

(* was NHCXLRV_PREP *)

let NHCXLRV = 
prove_by_refinement(
  `!v w0 w1 w2 f a b.    
    deformation f {w0,w1,w2,v} (a,b) /\
    ~collinear {vec 0, f w1 (&0), f w2 (&0)} /\
    ~collinear {vec 0, f w1 (&0), f w0 (&0)} /\
    ~collinear {vec 0, f w1 (&0), f v (&0)} /\
    v IN wedge (vec 0) w1 w2 w0 ==>
    (?e. &0 < e /\ 
       (!t. abs t < e ==> (f v t) IN wedge (vec 0) (f w1 t) (f w2 t) (f w0 t)))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM;IN_INSERT;NOT_IN_EMPTY;Localization.deformation];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?c. azim (vec 0) w1 w2 v < c /\ c < azim (vec 0) w1 w2 w0` (C SUBGOAL_THEN MP_TAC);
    TYPIFY `(azim (vec 0) w1 w2 v + azim (vec 0) w1 w2 w0)/ &2` EXISTS_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `(?e1. &0 < e1 /\ (!t. abs t < e1 ==> &0 < azim (vec 0) (f w1 t) (f w2 t) (f v t))) /\(?e2. &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f w1 t) (f w2 t) (f v t) < c)) /\ (?e3. &0 < e3 /\ (!t. abs t < e3 ==> c < azim (vec 0) (f w1 t) (f w2 t) (f w0 t)))` ENOUGH_TO_SHOW_TAC;
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `if (e1 <= e2 /\ e1 <= e3) then e1 else if (e2 <= e3 /\ e2 <= e1) then e2 else e3` EXISTS_TAC;
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    CONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
    MATCH_MP_TAC REAL_LT_TRANS;
    TYPIFY `c` EXISTS_TAC;
    BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f w0`;`&0`;`a`;`b`];
  ANTS_TAC;
    ASM_REWRITE_TAC[GSYM azim_pos_iff_nz];
    FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC);
    TYPIFY_GOAL_THEN `&0 < azim (vec 0) w1 w2 w0` (unlist REWRITE_TAC);
      BY(ASM_MESON_TAC[Counting_spheres.AZIM_NN;arith `&0 <= x /\ x < y ==> &0 < y`]);
    BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f v`;`&0`;`a`;`b`];
  ANTS_TAC;
    ASM_REWRITE_TAC[GSYM azim_pos_iff_nz];
    FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC);
    ASM_REWRITE_TAC[];
    BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  RULE_ASSUM_TAC (REWRITE_RULE[arith `&0 - e = -- e /\ &0 + e  = e`]);
  INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f v q))`;`real_interval (-- e',e')`;`{x | &0 < x}`];
  ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`];
  INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f v q))`;`real_interval (-- e',e')`;`{x | x < c }`];
  ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_LT];
  INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f w0 q))`;`real_interval (-- e,e)`;`{x | c < x}`];
  ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_GT;arith ` c < x <=> x > c`];
  REWRITE_TAC[IN_REAL_INTERVAL;IN_ELIM_THM;real_open];
  REWRITE_TAC[arith `x > c <=> c < x`];
  REPEAT (DISCH_THEN (C INTRO_TAC [`&0`]) THEN (FIRST_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC)) THEN ASM_SIMP_TAC[arith `&0 < e ==> -- e < &0`] THEN DISCH_TAC);
  RULE_ASSUM_TAC (REWRITE_RULE[arith `x - &0 = x`]);
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let NHCXLRV_ALT = 
prove_by_refinement(
  `!v w0 w1 w2 f a b.
         deformation f {w0, w1, w2, v} (a,b) /\
         ~collinear {vec 0, w1, w2} /\
         ~collinear {vec 0, w1, w0} /\
         ~collinear {vec 0, w1, v} /\
         v IN wedge (vec 0) w1 w2 w0
         ==> (?e. &0 < e /\
                  (!t. abs t < e
                       ==> f v t IN wedge (vec 0) (f w1 t) (f w2 t) (f w0 t)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC NHCXLRV;
  GEXISTL_TAC [`a`;`b`];
  ASM_REWRITE_TAC[];
  TYPIFY `!u. u  IN {w0,w1,w2,v} ==> f u (&0) = u` (C SUBGOAL_THEN ASSUME_TAC);
    RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]);
    ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC);
  ASM_REWRITE_TAC[];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let WNWSHJT = 
prove_by_refinement(
  `!w0 w1 w2 f a b.    
    deformation f {w0,w1,w2} (a,b) /\
    ~collinear {vec 0, f w1 (&0), f w2 (&0)} /\
    ~collinear {vec 0, f w1 (&0), f w0 (&0)} /\
    &0 < azim (vec 0) w1 w2 w0   /\
    azim (vec 0) w1 w2 w0 < pi ==> 
    (?e. &0 < e /\ 
       (!t. abs t < e ==> azim (vec 0) (f w1 t) (f w2 t) (f w0 t) < pi))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[IN_ELIM_THM;IN_INSERT;NOT_IN_EMPTY;Localization.deformation];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f w0`;`&0`;`a`;`b`];
  ANTS_TAC;
    ASM_REWRITE_TAC[GSYM azim_pos_iff_nz];
    FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC);
    ASM_REWRITE_TAC[];
    BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  RULE_ASSUM_TAC (REWRITE_RULE[arith `&0 - e = -- e /\ &0 + e  = e`]);
  INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f w0 q))`;`real_interval (-- e,e)`;`{x | x < pi}`];
  ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_LT];
  REWRITE_TAC[IN_REAL_INTERVAL;IN_ELIM_THM;real_open];
  REPEAT (DISCH_THEN (C INTRO_TAC [`&0`]) THEN (FIRST_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC)) THEN ASM_SIMP_TAC[arith `&0 < e ==> -- e < &0`] THEN DISCH_TAC);
  RULE_ASSUM_TAC (REWRITE_RULE[arith `x - &0 = x`]);
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let LOFA_IMP_INANGLE_EQ_AZIM = 
prove_by_refinement
(`!V E FF v. local_fan (V,E,FF) /\ v IN V ==> interior_angle1 (vec 0) FF v = azim_in_fan (v, rho_node1 FF v) E `,

[
  REWRITE_TAC[Localization.convex_local_fan; Local_lemmas.azim_in_fan2];
  REPEAT STRIP_TAC;
  ASSUME_TAC2 Local_lemmas.EXISTS_INVERSE_OF_V;
  DOWN THEN STRIP_TAC;
  ASSUME_TAC2 Local_lemmas.LOFA_IMP_EE_TWO_ELMS;
  ASSUME_TAC2 Local_lemmas.LOFA_CARD_EE_V_1;
  ASSUME_TAC2 Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2;
  DOWN THEN STRIP_TAC;
  UNDISCH_TAC` v:real^3 IN V `;
  FIRST_ASSUM NHANH;
  LET_TAC;
  SWITCH_TAC` EE v E = {rho_node1 FF v, vv} `;
  ASM_SIMP_TAC[ARITH_RULE` a = 2 ==> a > 1 `];
  STRIP_TAC;
  DOWN THEN DOWN THEN PHA;
  ASSUME_TAC2 (SPEC `vv:real^3 ` (GEN` v:real^3 ` Local_lemmas.IVS_RHO_IDD));
  EXPAND_TAC "d";
  SIMP_TAC[];
  UNDISCH_TAC` {rho_node1 FF v, vv} = EE v E `;
  DISCH_THEN (SUBST1_TAC o SYM);
  EXPAND_TAC "v";
  DOWN;
  BY(SIMP_TAC[Local_lemmas.interior_angle1; GSYM Local_lemmas.ivs_rho_node1; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET])
]);;

let deformation_rho_node1_equivariant1 = 
prove_by_refinement(
  `!f V E FF a b v t. 
    deformation f V (a,b) /\
    local_fan (V,E,FF) /\
    local_fan
                    (IMAGE (\v. f v t) V,
                     IMAGE (\s. IMAGE (\v. f v t) s) E,
                     IMAGE (\ (u,v). f u t,f v t) FF) /\
    v IN V ==>
    f (rho_node1 FF v) t = rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC EQ_SYM;
  MATCH_MP_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE);
  GEXISTL_TAC [`IMAGE (\v. f v t) V`;`       IMAGE (\s. IMAGE (\v. f v t) s) E`];
  CONJ_TAC;
    TYPIFY `IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` ENOUGH_TO_SHOW_TAC;
      DISCH_THEN (SUBST1_TAC o GSYM);
      BY(ASM_REWRITE_TAC[]);
    BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
  REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
  GEXISTL_TAC [`v`;`rho_node1 FF v`];
  REWRITE_TAC[];
  BY(ASM_MESON_TAC[Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2])
  ]);;
  (* }}} *)

let deformation_ivs_rho_node1_equivariant1 = 
prove_by_refinement(
  `!f V E FF a b v t. 
    deformation f V (a,b) /\
    local_fan (V,E,FF) /\
    local_fan
                    (IMAGE (\v. f v t) V,
                     IMAGE (\s. IMAGE (\v. f v t) s) E,
                     IMAGE (\ (u,v). f u t,f v t) FF) /\
    v IN V ==>
    f (ivs_rho_node1 FF v) t = ivs_rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC EQ_SYM;
  MATCH_MP_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE);
  GEXISTL_TAC [`IMAGE (\v. f v t) V`;`       IMAGE (\s. IMAGE (\v. f v t) s) E`];
  CONJ_TAC;
    TYPIFY `IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` ENOUGH_TO_SHOW_TAC;
      DISCH_THEN (SUBST1_TAC o GSYM);
      BY(ASM_REWRITE_TAC[]);
    BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
  REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
  GEXISTL_TAC [`ivs_rho_node1 FF v`;`v`];
  REWRITE_TAC[];
  BY(ASM_MESON_TAC[Lunar_deform.IVS_RHO_NODE_V_IN_FF])
  ]);;
  (* }}} *)

let deformation_rho_node1_equivariant = 
prove_by_refinement(
  `!f V E FF a b v . 
    deformation f V (a,b) /\
    local_fan (V,E,FF) /\
    v IN V ==>
    (?e. &0 < e /\ 
       (!t. abs t < e ==> f (rho_node1 FF v) t = rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`t`]);
  ASM_REWRITE_TAC[];
  BY(ASM_MESON_TAC[deformation_rho_node1_equivariant1])
  ]);;
  (* }}} *)

let deformation_subset = 
prove_by_refinement(
  `!f U V a b. U SUBSET V /\ deformation f V (a,b) ==> deformation f U (a,b)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Localization.deformation;SUBSET];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let EXISTS_TRIPLE_THM = 
prove_by_refinement(
  `!P. (?p1 p2 p3. P p1 p2 p3) <=> (?x. P (FST x) (FST (SND x)) (SND (SND x)))`,

  (* {{{ proof *)
  [
  BY(REWRITE_TAC[EXISTS_PAIR_THM])
  ]);;
  (* }}} *)

let zlz_reduction = 
prove_by_refinement(
  `!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) /\
     (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
	 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) /\
  (!u v w.
      ?e4. v,w IN FF /\ u IN V
           ==> &0 < e4 /\
               (!t. --e4 < t /\ t < e4
                    ==> aff_ge {vec 0} {f v t, f w t} INTER
                        aff_lt {vec 0} {f u t} =
                        {})) /\
 (!x. ?e3. x IN FF
           ==> &0 < e3 /\
               (!t. --e3 < t /\ t < e3
                    ==> IMAGE (\v. f v t) V SUBSET
                        wedge_in_fan_ge (f (FST x) t,f (SND x) t)
                        (IMAGE (IMAGE (\v. f v t)) E))) /\
 (!x. ?e2. x IN FF
           ==> &0 < e2 /\
               (!t. --e2 < t /\ t < e2
                    ==> azim_in_fan (f (FST x) t,f (SND x) t)
                        (IMAGE (IMAGE (\v. f v t)) E) <=
                        pi)) 
   ==> (?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> convex_local_fan
                       (IMAGE (\v. f v t) V,
                        IMAGE (IMAGE (\v. f v t)) E,
                        IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
                       generic (IMAGE (\v. f v t) V)
                       (IMAGE (IMAGE (\v. f v t)) E)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Localization.convex_local_fan];
  REWRITE_TAC[Localization.generic];
  COMMENT "preliminaries";
  TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
  INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `FINITE FF` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~(FF = {})` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Polar_fan.LOCAL_FAN_NOT_EMPTY_FF;
    BY(ASM_MESON_TAC[]);
  TYPIFY `(?e1. &0 < e1 /\ (!t. --e1 < t /\ t < e1 ==>       (local_fan               (IMAGE (\v. f v t) V,                IMAGE (IMAGE (\v. f v t)) E,                IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF)))) /\     (?e2. &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> 			 ((!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF                    ==> azim_in_fan x (IMAGE (IMAGE (\v. f v t)) E) <= pi)))) /\     (?e3. &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> 			 (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF                    ==>                         IMAGE (\v. f v t) V SUBSET                        wedge_in_fan_ge x (IMAGE (IMAGE (\v. f v t)) E)))) /\    (?e4. &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> 			(!v w u.                   {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\                   u IN IMAGE (\v. f v t) V                   ==> aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})))` ENOUGH_TO_SHOW_TAC;
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `?e. e <= e1 /\ e <= e2 /\ e <= e3 /\ e <= e4 /\ &0 < e` (C SUBGOAL_THEN MP_TAC);
      INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e1,e2,e3,e4}`];
      ANTS_TAC;
        CONJ_TAC;
          BY(MESON_TAC[FINITE_RULES]);
        BY(SET_TAC[]);
      REPEAT WEAKER_STRIP_TAC;
      TYPIFY `m` EXISTS_TAC;
      RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT;NOT_IN_EMPTY]);
      REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN (REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC));
      BY(MESON_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e` EXISTS_TAC;
    BY(ASM_MESON_TAC[arith `-- e < t /\ t < e /\ e <= e' ==> (-- e' < t /\ t < e')`]);
  COMMENT "local_fan";
  SUBCONJ_TAC;
    INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`t`]);
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  COMMENT "skolemize all variables";
  COMMENT "angle <= pi";
  TYPIFY_GOAL_THEN `(!x. ?e2. x IN FF ==> ( &0 < e2 /\   (!t.  --e2 < t /\ t < e2 ==> azim_in_fan ( (\uv. f (FST uv) t,f (SND uv) t) x) (IMAGE (IMAGE (\v. f v t)) E) <= pi))) ==> (?e2. &0 < e2 /\       (!t. --e2 < t /\ t < e2            ==> (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF                     ==> azim_in_fan x (IMAGE (IMAGE (\v. f v t)) E) <= pi)))` GMATCH_SIMP_TAC;
    REWRITE_TAC[SKOLEM_THM];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `?e. &0 < e /\ (!x. x IN FF ==> e <= e2 x)` (C SUBGOAL_THEN MP_TAC);
      INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e2 FF`];
      ANTS_TAC;
        CONJ_TAC;
          (MATCH_MP_TAC FINITE_IMAGE);
          BY(ASM_REWRITE_TAC[]);
        (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
        BY(ASM_REWRITE_TAC[]);
      REPEAT WEAKER_STRIP_TAC;
      TYPIFY `m` EXISTS_TAC;
      REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC);
      REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
      REWRITE_TAC[IN_IMAGE];
      BY(MESON_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
    REPEAT WEAKER_STRIP_TAC;
    REPEAT (FIRST_X_ASSUM (C INTRO_TAC [`p1,p2`]));
    DISCH_TAC;
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `IMAGE` MP_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`t`]);
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[]);
  COMMENT "skolemize wedge_in_fan";
  TYPIFY_GOAL_THEN `(!x. ?e3. x IN FF ==>  &0 < e3 /\       (!t. --e3 < t /\ t < e3            ==> (IMAGE (\v. f v t) V SUBSET                         wedge_in_fan_ge (f (FST x) t, f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E)))) ==> ( (?e3. &0 < e3 /\       (!t. --e3 < t /\ t < e3            ==> (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF                     ==> IMAGE (\v. f v t) V SUBSET                         wedge_in_fan_ge x (IMAGE (IMAGE (\v. f v t)) E)))))` GMATCH_SIMP_TAC;
    REWRITE_TAC[SKOLEM_THM];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `?e. &0 < e /\ (!x. x IN FF ==> e <= e3 x)` (C SUBGOAL_THEN MP_TAC);
      INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e3 FF`];
      ANTS_TAC;
        CONJ_TAC;
          (MATCH_MP_TAC FINITE_IMAGE);
          BY(ASM_REWRITE_TAC[]);
        (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
        BY(ASM_REWRITE_TAC[]);
      REPEAT WEAKER_STRIP_TAC;
      TYPIFY `m` EXISTS_TAC;
      REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC);
      REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
      REWRITE_TAC[IN_IMAGE];
      BY(MESON_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
    REPEAT WEAKER_STRIP_TAC;
    REPEAT (FIRST_X_ASSUM (C INTRO_TAC [`p1,p2`]));
    DISCH_TAC;
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `IMAGE` MP_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`t`]);
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[]);
  TYPIFY_GOAL_THEN `(!u v w. ?e4. (v,w) IN FF /\ u IN V ==> &0 < e4 /\ (!t. --e4 < t /\ t < e4  ==> aff_ge {vec 0} {f v t, f w t} INTER aff_lt {vec 0} {f u t} = {})) ==> (?e4. &0 < e4 /\       (!t. --e4 < t /\ t < e4            ==> (!v w u.                     {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\                     u IN IMAGE (\v. f v t) V                     ==> aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {}))) ` GMATCH_SIMP_TAC;
    REWRITE_TAC[SKOLEM_THM];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `?e. &0 < e /\ (!u v w. (u,(v,w)) IN V CROSS FF ==> e <= e4 u v w)` (C SUBGOAL_THEN MP_TAC);
      INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE (\ x. e4 (FST x) (FST (SND x)) (SND(SND x))) (V CROSS FF)`];
      ANTS_TAC;
        CONJ_TAC;
          (MATCH_MP_TAC FINITE_IMAGE);
          MATCH_MP_TAC FINITE_CROSS;
          ASM_REWRITE_TAC[];
          BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]);
        (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
        REWRITE_TAC[CROSS_EQ_EMPTY];
        ASM_REWRITE_TAC[];
        BY(ASM_MESON_TAC[Local_lemmas.LOFA_V_NOT_EMP]);
      REPEAT WEAKER_STRIP_TAC;
      TYPIFY `m` EXISTS_TAC;
      REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
      REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
      REWRITE_TAC[IN_IMAGE];
      REWRITE_TAC[EXISTS_PAIR_THM];
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`p1`;`p1'`;`p2`]);
      ANTS_TAC;
        RULE_ASSUM_TAC(REWRITE_RULE[IN_CROSS]);
        BY(ASM_REWRITE_TAC[]);
      (REPEAT WEAKER_STRIP_TAC);
      ASM_REWRITE_TAC[];
      TYPIFY `m = e4 p1 p1' p2` UNDISCH_TAC;
      DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_MESON_TAC[IN_CROSS]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `IMAGE` MP_TAC;
    REWRITE_TAC[IN_IMAGE];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `?v' w'. x' = {v',w'}` (C SUBGOAL_THEN MP_TAC);
      TYPIFY `graph E` (C SUBGOAL_THEN ASSUME_TAC);
        BY(ASM_MESON_TAC[Fan_defs.FAN;Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN]);
      RULE_ASSUM_TAC(REWRITE_RULE[Fan_defs.graph]);
      TYPIFY`x' HAS_SIZE 2` (C SUBGOAL_THEN ASSUME_TAC);
        BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[IN]);
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[Local_lemmas1.HAS_SIZE_2_EXISTS2]);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    FIRST_X_ASSUM_ST `IMAGE` MP_TAC;
    REWRITE_TAC[SET_RULE `IMAGE f {u,v} = {f u,f v}`];
    DISCH_THEN ( SUBST1_TAC );
    ASM_REWRITE_TAC[];
    TYPIFY `?v'' w''. {v',w'} = {v'',w''} /\ (v'',w'') IN FF` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_MESON_TAC[Local_lemmas.LOFA_IN_E_IMP_IN_FF;SET_RULE `{a,b} = {b,a}`]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `{f v' t,f w' t} = {f v'' t,f w'' t}` (C SUBGOAL_THEN SUBST1_TAC);
      FIRST_X_ASSUM_ST `{a,b}` MP_TAC;
      REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND];
      BY(MESON_TAC[]);
    FIRST_X_ASSUM (C INTRO_TAC [`x`;`v''`;`w''`]);
    REWRITE_TAC[IN_CROSS];
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`x`;`v''`;`w''`]);
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let real_interval_contains_0_ball = 
prove_by_refinement(
`!a b e1. a < &0 /\ &0 < b /\ &0 < e1  ==> (?e. &0 < e /\ e <= e1 /\ (!t. abs t < e ==> t IN real_interval (a,b)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `if (b <= -- a) /\ b <= e1 then b else (if e1 <= b /\ e1 <= --a then e1 else -- a)` EXISTS_TAC;
  REWRITE_TAC[IN_REAL_INTERVAL];
  ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
  CONJ_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  CONJ_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  GEN_TAC;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let zlz_azim = 
prove_by_refinement(
  `!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) /\
     (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
	 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==>
 (!x. ?e2. x IN FF
           ==> &0 < e2 /\
               (!t. --e2 < t /\ t < e2
                    ==> azim_in_fan (f (FST x) t,f (SND x) t)
                        (IMAGE (IMAGE (\v. f v t)) E) <=
                        pi)) `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Localization.convex_local_fan];
  REWRITE_TAC[Localization.generic];
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "preliminaries";
  TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
  INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`];
  ASM_REWRITE_TAC[];
  TYPIFY `FINITE FF` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~(FF = {})` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Polar_fan.LOCAL_FAN_NOT_EMPTY_FF;
    BY(ASM_MESON_TAC[]);
  COMMENT "local_fan";
  INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
  ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "restart here";
  TYPIFY `?p1 p2. (x = p1,p2)` (C SUBGOAL_THEN MP_TAC);
    BY(REWRITE_TAC[PAIR_SURJECTIVE]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[FST;SND];
  FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
  REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
  DISCH_TAC;
  TYPIFY `p1 IN V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]);
  TYPIFY `p2 = rho_node1 FF p1` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC EQ_SYM;
    MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `interior_angle1 (vec 0) FF p1 = azim_in_fan (p1,p2) E` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC LOFA_IMP_INANGLE_EQ_AZIM [`V`;`E`;`FF`;`p1`];
    BY(ASM_MESON_TAC[]);
  TYPIFY `?e2. &0 < e2 /\ e2 <= e /\ (!t. abs t < e2 ==> t IN real_interval (a,b))` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC real_interval_contains_0_ball;
    RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_REAL_INTERVAL]);
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "first case";
  TYPIFY `interior_angle1 (vec 0) FF p1 = pi` ASM_CASES_TAC;
    TYPIFY `e2` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    COMMENT "new insert";
    TYPIFY `local_fan (IMAGE (\v. f v t) V,  IMAGE (IMAGE (\v. f v t)) E,  IMAGE (\uv. f (FST uv) (t),f (SND uv) (t)) FF) /\ f p1 (t) IN IMAGE (\v. f v t) V` (C SUBGOAL_THEN ASSUME_TAC);
      CONJ_TAC;
        ASM_REWRITE_TAC[];
        FIRST_X_ASSUM MATCH_MP_TAC;
        BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
      REWRITE_TAC[IN_IMAGE];
      TYPIFY `p1` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    GMATCH_SIMP_TAC deformation_rho_node1_equivariant1;
    CONJ_TAC;
      GEXISTL_TAC [`a`;`b`;`E`;`V`];
      BY(ASM_REWRITE_TAC[]);
    INTRO_TAC (GSYM LOFA_IMP_INANGLE_EQ_AZIM) [`IMAGE (\v. f v t) V`;`IMAGE (IMAGE (\v. f v t)) E`;`IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF`;`f p1 t`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    DISCH_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    BY(ASM_MESON_TAC[]);
  COMMENT "second case here";
  COMMENT "case azim < pi";
  TYPIFY `interior_angle1 (vec 0) FF p1 < pi` (C SUBGOAL_THEN ASSUME_TAC);
    RULE_ASSUM_TAC (REWRITE_RULE[Localization.convex_local_fan]);
    FIRST_X_ASSUM_ST `wedge_in_fan_ge` MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `interior_angle1 (vec 0) FF p1 <= pi` ENOUGH_TO_SHOW_TAC;
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[]);
  INTRO_TAC WNWSHJT [`ivs_rho_node1 FF p1`;`p1`;`p2`;`f`;`a`;`b`];
  ASM_REWRITE_TAC[];
  REPEAT (GMATCH_SIMP_TAC (GSYM Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND));
  TYPIFY `E` EXISTS_TAC;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  ANTS_TAC;
    CONJ_TAC;
      MATCH_MP_TAC deformation_subset;
      TYPIFY `V` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
      BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_IVS_IN_V;Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]);
    (GMATCH_SIMP_TAC deformation_rho_node1_equivariant1);
    GMATCH_SIMP_TAC deformation_ivs_rho_node1_equivariant1;
    CONJ_TAC;
      GEXISTL_TAC [`a`;`b`;`E`;`V`];
      ASM_REWRITE_TAC[];
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e1` MP_TAC) THEN REAL_ARITH_TAC);
    CONJ_TAC;
      GEXISTL_TAC [`a`;`b`;`E`;`V`];
      ASM_REWRITE_TAC[];
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e1` MP_TAC) THEN REAL_ARITH_TAC);
    TYPIFY `!v. v IN V ==> f v (&0) = v` (C SUBGOAL_THEN ASSUME_TAC);
      RULE_ASSUM_TAC (REWRITE_RULE[Localization.deformation]);
      BY(ASM_REWRITE_TAC[]);
    TYPIFY `f p1 (&0) = p1` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_SIMP_TAC[]);
    ASM_REWRITE_TAC[];
    TYPIFY `IMAGE (\uv. f (FST uv) (&0),f (SND uv) (&0)) FF = FF` (C SUBGOAL_THEN SUBST1_TAC);
      REWRITE_TAC[IN_IMAGE;EXTENSION;EXISTS_PAIR_THM];
      GEN_TAC;
      INTRO_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V) [`E`;`FF`;`FST x`;`SND x`;`V`];
      ASM_REWRITE_TAC[];
      DISCH_TAC;
      TYPIFY `x IN FF` ASM_CASES_TAC;
        ASM_REWRITE_TAC[];
        GEXISTL_TAC [ `FST x`;`SND x`];
        BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[PAIR;FST;SND]);
      ASM_REWRITE_TAC[];
      REWRITE_TAC[NOT_EXISTS_THM];
      REPEAT WEAKER_STRIP_TAC;
      INTRO_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V) [`E`;`FF`;`p1'`;`p2'`;`V`];
      ASM_REWRITE_TAC[];
      BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[PAIR;FST;SND]);
    TYPIFY `p1 IN V` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]);
    CONJ_TAC;
      INTRO_TAC (GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS) [`E`;`V`;`FF`;`p1`];
      BY(ASM_REWRITE_TAC[]);
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `(!t. abs t < e ==> azim_in_fan (f p1 t,f (rho_node1 FF p1) t)               (IMAGE (IMAGE (\v. f v t)) E) = azim (vec 0) (f p1 t) (f (rho_node1 FF p1) t)              (f (ivs_rho_node1 FF p1) t))` (C SUBGOAL_THEN MP_TAC);
    REPEAT WEAKER_STRIP_TAC;
    GMATCH_SIMP_TAC deformation_rho_node1_equivariant1;
    CONJ_TAC;
      GEXISTL_TAC [`a`;`b`;`E`;`V`];
      (ASM_REWRITE_TAC[]);
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(ASM_REWRITE_TAC[]);
    GMATCH_SIMP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND;
    CONJ_TAC;
      TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
      CONJ_TAC;
        FIRST_X_ASSUM MATCH_MP_TAC;
        BY(ASM_REWRITE_TAC[]);
      REWRITE_TAC[IN_IMAGE];
      TYPIFY `p1` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    GMATCH_SIMP_TAC deformation_ivs_rho_node1_equivariant1;
    GEXISTL_TAC [`a`;`b`;`E`;`V`];
    (ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  TYPIFY `if (e2 <= e') then e2 else e'` EXISTS_TAC;
  CONJ_TAC;
    BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`t`]);
  ANTS_TAC;
    BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  DISCH_THEN SUBST1_TAC;
  MATCH_MP_TAC (arith `x < pi ==> x <= pi`);
  FIRST_X_ASSUM MATCH_MP_TAC;
  BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let zlz_generic = 
prove_by_refinement(
  `!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) ==>
  (!u v w.
      ?e4. v,w IN FF /\ u IN V
           ==> &0 < e4 /\
               (!t. --e4 < t /\ t < e4
                    ==> aff_ge {vec 0} {f v t, f w t} INTER
                        aff_lt {vec 0} {f u t} =
                        {}))`,

  (* {{{ proof *)
  [
  COMMENT "prelims";
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `v IN V /\ w IN V` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~(u = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_V_DIFF]);
  TYPIFY `rho_node1 FF v = w` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~collinear {vec 0,v, rho_node1 FF v}` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  COMMENT "expand generic";
  RULE_ASSUM_TAC(REWRITE_RULE[Localization.generic]);
  FIRST_X_ASSUM (C INTRO_TAC [`v`;`rho_node1 FF v`;`u`]);
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC Local_lemmas.LOCAL_FAN_IN_FF_IN_ORD_PAIRS2;
    BY(ASM_REWRITE_TAC[]);
  (GMATCH_SIMP_TAC generic_alt);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `?e. &0 < e /\ (!t. -- e < t /\ t < e ==> ~(f u t = vec 0) /\ ~collinear {vec 0,f v t,f w t} /\ (~coplanar {vec 0,f u t,f v t,f w t} \/ -- (f u t) IN wedge (vec 0) (f v t cross f w t) (f w t) (f v t)))` ENOUGH_TO_SHOW_TAC;
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    GMATCH_SIMP_TAC generic_alt;
    FIRST_X_ASSUM (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `?e1. &0 < e1 /\ (!t. abs t < e1 ==> ~(f u t = vec 0))` (C SUBGOAL_THEN MP_TAC);
    REWRITE_TAC[GSYM NORM_POS_LT];
    INTRO_TAC Pent_hex.continuous_preimage_open [`norm o (f u)`;`real_interval (a,b)`;`{x | &0 < x}`];
    REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
    REWRITE_TAC[IN_ELIM_THM;o_THM];
    ANTS_TAC;
      REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`];
      GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
      REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC REAL_CONTINUOUS_CONTINUOUS_ATREAL_COMPOSE;
      CONJ_TAC;
        RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]);
        BY(ASM_MESON_TAC[]);
      BY(REWRITE_TAC[REAL_CONTINUOUS_NORM_WITHIN]);
    REWRITE_TAC[real_open;IN_ELIM_THM];
    DISCH_THEN (C INTRO_TAC [`&0`]);
    ANTS_TAC;
      RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]);
      ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[NORM_POS_LT]);
    BY(MESON_TAC[arith `abs (x - &0) = abs x`]);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "collinearity";
  TYPIFY `f v (&0) = v /\ f w (&0) = w /\ f u (&0) = u /\ f v continuous atreal (&0) /\ f w continuous atreal (&0) /\ f u continuous atreal (&0)` (C SUBGOAL_THEN ASSUME_TAC);
    RULE_ASSUM_TAC (REWRITE_RULE[Localization.deformation]);
    BY(ASM_MESON_TAC[]);
  TYPIFY `?e2. &0 < e2 /\ (!t. abs t < e2 ==> ~collinear {vec 0,f v t, f w t})` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`&0`;`(vec 0):real^3`;`f v`;`f w`];
    ASM_REWRITE_TAC[];
    BY(MESON_TAC[arith `abs(&0 - r') = abs(r')`]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?e3. &0 < e3 /\ (!t. abs t < e3 ==> ((~coplanar {vec 0, f u t, f v t, f w t} \/               --f u t IN wedge (vec 0) (f v t cross f w t) (f w t) (f v t))))` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM DISJ_CASES_TAC;
      INTRO_TAC NONPLANAR_OPEN [`\ (t:real). (vec 0):real^3`;`f u`;`f v`;`f w`;`&0`];
      ASM_REWRITE_TAC[CONTINUOUS_CONST;arith `abs(&0  - t') = abs(t')`];
      BY(MESON_TAC[]);
    COMMENT "disjointness";
    TYPIFY `~(v cross w = v) /\ ~(v cross w = w) ` (C SUBGOAL_THEN ASSUME_TAC);
      REWRITE_TAC[CROSS_EQ_SELF];
      BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b} = {a,b}`;SET_RULE `{a,b,a} = {a,b}`]);
    TYPIFY `~(v cross w = -- u)` (C SUBGOAL_THEN ASSUME_TAC);
      FIRST_X_ASSUM_ST `wedge` MP_TAC;
      REWRITE_TAC[wedge;IN_ELIM_THM];
      BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}={a,b}`]);
    TYPIFY `~( ( -- (u:real^3) = v) \/ (-- u = w))` (C SUBGOAL_THEN MP_TAC);
      DISCH_TAC;
      FIRST_X_ASSUM_ST `wedge` MP_TAC;
      REWRITE_TAC[Reuhady.WEDGE_SIMPLE];
      FIRST_X_ASSUM DISJ_CASES_TAC;
        ASM_REWRITE_TAC[IN_ELIM_THM];
        BY(REWRITE_TAC[arith `~(x < x)`]);
      ASM_REWRITE_TAC[IN_ELIM_THM];
      BY(REWRITE_TAC[AZIM_REFL;arith `~(&0 < &0)`]);
    REWRITE_TAC[DE_MORGAN_THM];
    REPEAT WEAKER_STRIP_TAC;
    COMMENT "wedge";
    TYPIFY `?g. deformation g {v, v cross w, w, --u}  (a,b) /\ ( g (v cross w)  = (\t.  f v t cross f w t)) /\ (g v = f v) /\ (g w = f w) /\ (g (-- u)  = (\t. -- f u t))` (C SUBGOAL_THEN MP_TAC);
      TYPIFY `\x. if (x = --u) then (\t. -- f u t) else if (x = v cross w) then (\t. f v t cross f w t) else f x` EXISTS_TAC;
      ASM_TAC THEN ASM_REWRITE_TAC[Localization.deformation;IN_INSERT;NOT_IN_EMPTY] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
      CONJ2_TAC;
        BY(REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC)) THEN ASM_REWRITE_TAC[] THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
      REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC)) THEN ASM_REWRITE_TAC[] THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[];
        BY(MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS THEN REWRITE_TAC[ETA_AX] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
      MATCH_MP_TAC CONTINUOUS_NEG;
      BY(REWRITE_TAC[ETA_AX] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC NHCXLRV [`-- (u:real^3)`;`v`;`v cross w`;`w`;`g`;`a`;`b`];
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      TYPIFY_GOAL_THEN `~collinear {vec 0, v cross w, --u}` (unlist REWRITE_TAC);
        FIRST_X_ASSUM_ST `wedge` MP_TAC;
        REWRITE_TAC[wedge;IN_ELIM_THM];
        BY(MESON_TAC[]);
      ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
      BY(ASM_REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS;GSYM COLL_IFF_COLL_CROSS2]);
    BY(MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `(?e. (&0 < e /\ e <= e1 /\ e <= e2 /\ e <= e3))` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e1,e2,e3}`];
    ANTS_TAC;
      CONJ_TAC;
        REWRITE_TAC[FINITE_RULES];
        BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
      BY(SET_TAC[]);
    REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `m` EXISTS_TAC;
    CONJ_TAC;
      REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC);
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e` EXISTS_TAC;
  REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN (REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN TRY REAL_ARITH_TAC))
  ]);;
  (* }}} *)

let zlz_wedge_skolem = 
prove_by_refinement(
  `!a b V E FF f.
     convex_local_fan (V,E,FF) /\
 (!x v. ?e3. x IN FF /\ v IN V
           ==> &0 < e3 /\
               (!t. --e3 < t /\ t < e3
                    ==> (f v t) IN 
                        wedge_in_fan_ge (f (FST x) t,f (SND x) t)
                        (IMAGE (IMAGE (\v. f v t)) E)))
     ==>
 (!x. ?e3. x IN FF
           ==> &0 < e3 /\
               (!t. --e3 < t /\ t < e3
                    ==> IMAGE (\v. f v t) V SUBSET
                        wedge_in_fan_ge (f (FST x) t,f (SND x) t)
                        (IMAGE (IMAGE (\v. f v t)) E)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
  DISCH_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`x`]);
  REWRITE_TAC[SKOLEM_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~(V = {})` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.LOFA_V_NOT_EMP;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `?e. &0 < e /\ (!v. v IN V ==> e <= e3 v)` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e3 V`];
    ANTS_TAC;
      CONJ_TAC;
        (MATCH_MP_TAC FINITE_IMAGE);
        MATCH_MP_TAC Local_lemmas.LOCAL_FAN_FINITE_V;
        BY(ASM_REWRITE_TAC[]);
      (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
      BY(ASM_REWRITE_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `m` EXISTS_TAC;
    REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
    REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY];
    REPEAT WEAKER_STRIP_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`x'`]);
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[SUBSET;IN_IMAGE];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`x''`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`t`]);
  ASM_REWRITE_TAC[];
  DISCH_THEN MATCH_MP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`x''`]);
  ASM_REWRITE_TAC[];
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let wedge_ge_refl = 
prove_by_refinement(
  `!v1 v2 v3 v4. v2 IN wedge_ge v1 v2 v3 v4`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE;Local_lemmas.AZIM_SPEC_DEGENERATE];
  BY(REWRITE_TAC[Counting_spheres.AZIM_NN])
  ]);;
  (* }}} *)

let zlz_wedge_refl = 
prove_by_refinement(
  `!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) /\
     (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
	 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==>
 (!v w. (w IN V /\ v IN {w, rho_node1 FF w, ivs_rho_node1 FF w}) ==> 
    ?e. &0 < e /\ (!t. -- e < t /\ t < e ==> f v t IN wedge_in_fan_ge (f w t , f (rho_node1 FF w) t) 
		       (IMAGE (IMAGE (\v. f v t)) E)))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
  INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`];
  ASM_REWRITE_TAC[];
  TYPIFY `e` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
  CONJ_TAC;
    TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[IN_IMAGE]);
  REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_REWRITE_TAC[Local_lemmas1.FST_LST_IN_WEDGE_GE];
  BY(REWRITE_TAC[wedge_ge_refl])
  ]);;
  (* }}} *)

let zlz_wedge_open = 
prove_by_refinement(
  `!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) /\
     (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
	 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==>
 (!v w. (v IN V /\ w IN V /\ v IN wedge (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)) ==> 
    ?e. &0 < e /\ (!t. -- e < t /\ t < e ==> f v t IN wedge_in_fan_ge (f w t , f (rho_node1 FF w) t) 
		       (IMAGE (IMAGE (\v. f v t)) E)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
  TYPIFY `v = w` ASM_CASES_TAC;
    INTRO_TAC zlz_wedge_refl [`a`;`b`;`V`;`E`;`FF`;`f`];
    ASM_REWRITE_TAC[];
    DISCH_THEN (C INTRO_TAC [`w`;`w`]);
    BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]);
  INTRO_TAC NHCXLRV_ALT [`v`;`(ivs_rho_node1 FF w)`;`w`;`(rho_node1 FF w)`;`f`;`a`;`b`];
  ASM_REWRITE_TAC[];
  TYPIFY `rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
    BY(ASM_REWRITE_TAC[]);
  GMATCH_SIMP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  ANTS_TAC;
    CONJ_TAC;
      MATCH_MP_TAC deformation_subset;
      TYPIFY `V` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
      BY(ASM_MESON_TAC[]);
    BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN]);
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[arith `--e < t /\ t < e <=> abs t < e`];
  TYPIFY `?e''. (&0 < e'') /\ e'' <= e  /\ e'' <= e'` (C SUBGOAL_THEN MP_TAC);
    TYPIFY `if (e <= e') then e else e'` EXISTS_TAC;
    BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e''` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]);
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  DISCH_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`t`]);
  ANTS_TAC;
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  DISCH_TAC;
  INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
  CONJ_TAC;
    TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[IN_IMAGE]);
  FIRST_X_ASSUM_ST `wedge` MP_TAC;
  ASM_REWRITE_TAC[];
  BY(SET_TAC[Leaf_cell.WEDGE_SUBSET_WEDGE_GE])
  ]);;
  (* }}} *)

let PROPERTIES_GENERIC_LOCAL_FAN_ALT = 
prove_by_refinement(
  `!V E FF u v.
    local_fan (V,E,FF) /\ u IN V /\ v IN V /\ ~(u = v) /\ generic V E  ==> ~collinear {vec 0,u,v}`,

  (* {{{ proof *)
  [
    BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN])
  ]);;
  (* }}} *)

let skolem_epsilon_old = 
prove_by_refinement(
  `!P Q s. (!e e' i. &0 < e /\ e <= e' /\ (i:A) IN s /\ P i==> (Q e' i ==> Q e i)) /\ FINITE s  ==>
    ((!i. ?e. (i IN s /\ P i) ==> (&0 < e /\ Q e i)) <=> (?e. !i. (i IN s /\ P i) ==> (&0 < e /\ Q e i)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(?i. i IN s /\ P i)` ASM_CASES_TAC;
    BY(ASM_MESON_TAC[]);
  RULE_ASSUM_TAC(REWRITE_RULE[]);
  MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a <=> b)`);
  CONJ_TAC;
    REWRITE_TAC[SKOLEM_THM];
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e {i | i IN s /\ P i}`];
    ANTS_TAC;
      CONJ_TAC;
        (MATCH_MP_TAC FINITE_IMAGE);
        MATCH_MP_TAC FINITE_SUBSET;
        TYPIFY `s` EXISTS_TAC;
        ASM_REWRITE_TAC[];
        BY(SET_TAC[]);
      (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
      ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;NOT_IN_EMPTY];
      BY(ASM_MESON_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `m` EXISTS_TAC;
    REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
    REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY;IN_ELIM_THM];
    REPEAT WEAKER_STRIP_TAC;
    ASM_REWRITE_TAC[];
    SUBCONJ_TAC;
      BY(ASM_MESON_TAC[]);
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let SKOLEM_EPSILON = 
prove_by_refinement(
  `!Q s. (!e e' i. &0 < e /\ e <= e' /\ (i:A) IN s ==> (Q e' i ==> Q e i)) /\ FINITE s  ==>
    ((!i. ?e. (&0 < e) /\ (i IN s ==> (Q e i))) <=> (?e. !i. (&0 < e) /\ (i IN s ==> ( Q e i))))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(?i. i IN s)` ASM_CASES_TAC;
    BY(ASM_MESON_TAC[]);
  RULE_ASSUM_TAC(REWRITE_RULE[]);
  MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a <=> b)`);
  CONJ2_TAC;
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[SKOLEM_THM];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e s`];
  ANTS_TAC;
    CONJ_TAC;
      (MATCH_MP_TAC FINITE_IMAGE);
      BY(ASM_REWRITE_TAC[]);
    (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
    ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;NOT_IN_EMPTY];
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `m` EXISTS_TAC;
  GEN_TAC;
  REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
  REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY;IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let EXISTS_AND_IMP = 
prove_by_refinement(
  `!P Q R. (?(d:A). (P /\ Q d ==> R d)) <=> (P ==> (?d. Q d ==> R d))`,

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

let XIV_DEFORMATION = 
prove_by_refinement(
  `!f dh r w a b.
    deformation f {w i | i <= r + 2} (a,b) /\ 
    pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\
    pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\
    (\ (i,j,k). dihV (vec 0) (w i) (w j) (w k)) = dh /\
    (!i. ?e2. i IN 1..r+1  ==> &0 < e2 /\
       (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\ 
    (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1))) /\ 
    (!p q.
       {p, q, q + 1} SUBSET 1..r+1 /\ ~(p = q) /\ ~(p = q + 1)
     ==> dh (p,q,q + 1) = &0) /\
    (!p q.
       {p, p + 1, q} SUBSET 1..r+1 /\ q > p + 1 ==> dh (p,p + 1,q) = &0) /\
    (!p q. {p + 1, p, q} SUBSET 1..r+1 /\ q < p ==> dh (p + 1,p,q) = &0)
    ==> (?e. &0 < e /\ (!t. abs t < e ==>
			  f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\
			  f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "prelims";
  COMMENT "find collinear epsilon";
  TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC));
    RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]);
    BY(ASM_MESON_TAC[]);
  TYPIFY `!i j. i IN 0..r+2 /\ j IN 0..r+2 /\ ~collinear {vec 0,w i,w j} ==> (?dc. &0 < dc /\ (!t. abs t < dc ==> ~collinear {vec 0, f (w i) t, f (w j) t}))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`&0`;`(vec 0):real^3`;`f (w i)`;`f (w j)`];
    RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;IN_NUMSEG]);
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]);
  COMMENT "skolemize collinear";
  TYPIFY `?dc. !i. (&0 < dc) /\ (i IN 0..r+2 ==> (!j. j IN 0..r+2 /\ ~collinear {vec 0,w i,w j} ==> (!t. abs t < dc ==> ~collinear {vec 0, f (w i) t, f (w j) t})))` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_NUMSEG];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`j`]);
      ANTS_TAC;
        BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
      DISCH_THEN (C INTRO_TAC [`t`]);
      ANTS_TAC;
        BY(REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
      BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
    GEN_TAC;
    REWRITE_TAC[MESON [arith `&0 < &1`] `(?dc. &0 < dc /\ (a ==> (!j. b j /\ c j ==> r dc j))) <=> (a ==> (?dc. !j. &0 < dc /\ (b j ==> (c j ==> r dc j))))`];
    DISCH_TAC;
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_NUMSEG];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM_ST `!` MP_TAC;
      ANTS_TAC;
        BY(ASM_REWRITE_TAC[]);
      DISCH_THEN (C INTRO_TAC [`t`]);
      ANTS_TAC;
        BY(REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
      BY(ASM_REWRITE_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`]);
    BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[arith `&0 < &1`]);
  FIRST_X_ASSUM_ST `collinear` MP_TAC THEN BURY_MP_TAC;
  FIRST_X_ASSUM_ST `collinear` kill;
  COMMENT "find dih epsilon";
  TYPIFY `!i j k e. &0 < e /\ i IN 1..r+1 /\ j IN 1 ..r+1 /\ k IN 1..r+1 /\ ~(i=j) /\ ~(i=k) /\ dh (i,j,k) = &0 ==> (? d. &0 < d /\ (!t. abs t < d ==> dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t) < e))` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "dh" THEN REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC));
      RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]);
      BY(ASM_MESON_TAC[]);
    INTRO_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE [`\(t:real). (vec 0):real^3`;`f (w i)`;`f (w j)`;`f (w k)`;`&0`];
    ANTS_TAC;
      RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;pairwise]);
      REWRITE_TAC[CONTINUOUS_CONST];
      FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC);
      ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
      RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]);
      TYPIFY_GOAL_THEN `k <= r + 2 /\ j <= r + 2 /\ i <= r + 2 ` (unlist REWRITE_TAC);
        BY(ASM_ARITH_TAC);
      REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC;
          BY(TYPIFY `i` EXISTS_TAC THEN ASM_ARITH_TAC);
        BY(TYPIFY `j` EXISTS_TAC THEN ASM_ARITH_TAC);
      BY(TYPIFY `k` EXISTS_TAC THEN ASM_ARITH_TAC);
    REWRITE_TAC[real_continuous_atreal];
    DISCH_THEN (C INTRO_TAC [`e`]);
    ASM_REWRITE_TAC[arith `abs (x' - &0) = abs x'`] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `d` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `i <= r + 2` (REPEAT o GMATCH_SIMP_TAC);
    ASM_REWRITE_TAC[];
    RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]);
    ASM_SIMP_TAC[arith `i <= r + 1 ==> i <= r + 2`];
    BY(REAL_ARITH_TAC);
  COMMENT "merge dih epsilon";
  TYPIFY `!e. &0 < e ==> (?d. !i. (&0 < d) /\ (i IN 1..r+1 ==> (!j k. j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i=k) /\ dh(i,j,k)= &0 ==> (!t. abs t < d ==> dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t) <                            e))))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_NUMSEG];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`j`;`k`]);
      ASM_REWRITE_TAC[];
      DISCH_THEN MATCH_MP_TAC;
      BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    GEN_TAC;
    REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (p ==> (!j k. a j /\ r j k ==> u j k d))) <=> (p ==> (?d. !j. &0 < d /\ (a j ==> (!k. r j k ==> u j k d))))`];
    DISCH_TAC;
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_NUMSEG];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`k`]);
      ASM_REWRITE_TAC[];
      DISCH_THEN MATCH_MP_TAC;
      BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    GEN_TAC;
    REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (p ==> (!k. a k /\ r k ==> u k d))) <=> (p ==> (?d. !k. &0 < d /\ (a k ==> (r k ==> u k d))))`];
    DISCH_TAC;
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_NUMSEG];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM_ST `dihV` MP_TAC;
      ASM_REWRITE_TAC[];
      DISCH_THEN MATCH_MP_TAC;
      BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    GEN_TAC;
    REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (a ==> b ==> c d)) <=> (a /\ b ==> (?d. &0 < d /\ c d))`];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`;`k`;`e`]);
    DISCH_THEN MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  FIRST_X_ASSUM MP_TAC;
  FIRST_X_ASSUM kill;
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "azim lb";
  TYPIFY `?c. !i. (&0 < c) /\ (i IN 1..r+1 ==> c < azim (vec 0) (w i) (w (i+1)) (w (i-1)))` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_NUMSEG];
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    GEN_TAC;
    REWRITE_TAC[MESON[arith `&0 < &1`] `(?c. &0 < c /\ (b ==> r c)) <=> (b ==> (?c. &0 < c /\ r c))`];
    DISCH_TAC;
    TYPIFY `azim (vec 0) (w i) (w (i+1)) (w (i-1)) / &2` EXISTS_TAC;
    FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`i`]);
    ASM_REWRITE_TAC[];
    BY(REAL_ARITH_TAC);
  FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
  COMMENT "azim deform lower bound";
  TYPIFY `!i. i IN 1..r+1 ==> (?d. &0 < d /\  (!t. abs t < d ==> (c < azim (vec 0) (f (w i) t) (f (w(i+1)) t) (f (w(i-1)) t))))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC));
      RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]);
      BY(ASM_MESON_TAC[]);
    INTRO_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE [`\(t:real). (vec 0):real^3`;`f (w i)`;`f (w (i+1))`;`f (w (i-1))`;`&0`];
    ANTS_TAC;
      RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;pairwise]);
      REWRITE_TAC[CONTINUOUS_CONST];
      FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC);
      ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
      RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]);
      TYPIFY_GOAL_THEN `i - 1 <= r + 2 /\ i + 1 <= r + 2 /\ i <= r + 2` (unlist REWRITE_TAC);
        BY(ASM_ARITH_TAC);
      GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
      REWRITE_TAC[GSYM azim_pos_iff_nz];
      TYPIFY_GOAL_THEN ` ~collinear {vec 0, w i, w (i - 1)}` (unlist REWRITE_TAC);
        FIRST_X_ASSUM_ST `collinear` kill;
        BY((FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC);
      REPEAT CONJ_TAC THEN (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC;
          BY(TYPIFY `i` EXISTS_TAC THEN ASM_ARITH_TAC);
        BY(TYPIFY `i+1` EXISTS_TAC THEN ASM_ARITH_TAC);
      BY(TYPIFY `i-1` EXISTS_TAC THEN ASM_ARITH_TAC);
    REWRITE_TAC[real_continuous_atreal];
    FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC);
    RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]);
    TYPIFY_GOAL_THEN `i - 1 <= r + 2 /\ i + 1 <= r + 2 /\ i <= r + 2` (unlist REWRITE_TAC);
      BY(ASM_ARITH_TAC);
    DISCH_THEN (C INTRO_TAC [`abs(azim (vec 0) (w i) (w (i+1)) (w (i-1)) - c)`]);
    FIRST_X_ASSUM (C INTRO_TAC [`i`]);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `c < azim a1 a2 a3 a4` MP_TAC;
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `abs` MP_TAC;
    ANTS_TAC;
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    ASM_REWRITE_TAC[arith `abs (x' - &0) = abs x'`] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `d` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[];
    BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  COMMENT "skolemize the azim delta";
  TYPIFY `?d. !i. &0 < d /\ (i IN 1..r+1 ==> (!t. abs t < d ==> c < azim (vec 0) (f (w i) t) (f (w (i + 1)) t)                            (f (w (i - 1)) t)))` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_NUMSEG];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`t`]);
      DISCH_THEN MATCH_MP_TAC;
      BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[arith `&0< &1`]);
  FIRST_X_ASSUM_ST `!i. i IN s ==> u` kill;
  COMMENT "skolemize azim<=pi";
  TYPIFY `?d2. !i. &0 < d2 /\ (i IN 1..r+1 ==> (!t. abs t < d2 ==> azim (vec 0) (f (w i) t) (f (w (i + 1)) t)                            (f (w (i - 1)) t) <=                            pi))` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_NUMSEG];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`t`]);
      DISCH_THEN MATCH_MP_TAC;
      BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    BY(FIRST_X_ASSUM_ST `azim a b c d <= pi` MP_TAC THEN MESON_TAC[arith `&0< &1`]);
  FIRST_X_ASSUM_ST `!i. i IN s ==> u` kill;
  COMMENT "pick eps";
  TYPIFY `?e. &0 < e /\ &2 * e = c` (C SUBGOAL_THEN MP_TAC);
    RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]);
    TYPIFY `c / &2` EXISTS_TAC;
    BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE) o GSYM);
  FIRST_X_ASSUM (C INTRO_TAC [`e`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?d'3. !d''. (&0 < d'3) /\ (d'' IN {d,d',d2,dc} ==> d'3 <= d'')` (C SUBGOAL_THEN MP_TAC);
    GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
    REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    GEN_TAC;
    RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]);
    TYPIFY `if (d'' IN {d,d',d2,dc}) then d'' else &1` EXISTS_TAC;
    CONJ_TAC;
      ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `&0 < d` MP_TAC) THEN REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY] THEN REAL_ARITH_TAC);
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `d'3` EXISTS_TAC;
  RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Xivphks.XIVPHKS_SHIFT [`\i. wedge_ge (vec 0) (f (w (i)) t) (f (w (i + 1)) t) (f (w (i-1)) t)`;`\ (i,j,k). azim (vec 0) (f (w i) t) (f (w (j)) t) (f (w (k)) t)`;`\ (i,j,k). dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t)`;`e`;`r`;`\i. f (w i) t`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    REWRITE_TAC[pairwise];
    RULE_ASSUM_TAC(REWRITE_RULE[pairwise]);
    TYPIFY `!j. j IN 0..r+1 ==> j IN 0..r+2` (C SUBGOAL_THEN ASSUME_TAC);
      BY(REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
    TYPIFY `!t. abs t < d'3 ==> abs t < dc` (C SUBGOAL_THEN ASSUME_TAC);
      REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`dc`]);
      BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
    CONJ_TAC;
      REPEAT (FIRST_X_ASSUM_ST `azim` kill);
      BY(ASM_MESON_TAC[]);
    CONJ_TAC;
      REPEAT (FIRST_X_ASSUM_ST `azim` kill);
      TYPIFY `!j. j IN 1..r+2 ==> j IN 0..r+2` (C SUBGOAL_THEN ASSUME_TAC);
        BY(REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
      BY(ASM_MESON_TAC[]);
    CONJ_TAC;
      TYPIFY `abs t < d'` (C SUBGOAL_THEN ASSUME_TAC);
        REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
        FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d'`]);
        BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
      BY(ASM_MESON_TAC[]);
    CONJ_TAC;
      TYPIFY `abs t < d2` (C SUBGOAL_THEN ASSUME_TAC);
        REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
        FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d2`]);
        BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
      BY(ASM_MESON_TAC[]);
    REPEAT (FIRST_X_ASSUM_ST `azim` kill);
    TYPIFY `abs t < d` (C SUBGOAL_THEN ASSUME_TAC);
      REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d`]);
      BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    TYPIFY `!i j k. {i,j,k} SUBSET 1..r+1 ==> i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1` (C SUBGOAL_THEN ASSUME_TAC);
      BY(SET_TAC[]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    CONJ_TAC;
      REPEAT (FIRST_X_ASSUM_ST `collinear` kill);
      BY(ASM_MESON_TAC[arith `~(p = p+1)`;arith `q > p+1 ==> ~(p = q)`]);
    BY(ASM_MESON_TAC[arith `~(p = p+1)`;arith `q < p  ==> ~(p+1 = q)`]);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`r`;`1`]);
  FIRST_X_ASSUM (C INTRO_TAC [`r`;`1`]);
  REWRITE_TAC[arith `(r:num) <= r`;arith `1 + 1 = 2 /\ 1 - 1 = 0 /\ (1+r)+1 = r + 2 /\ 1 + r <= r + 1 /\ (1 + r) - 1 = r`];
  REWRITE_TAC[arith `1 + r = r + 1`];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let XIV_ECAU = 
prove_by_refinement(
  `!f r w a b.
    deformation f {w i | i <= r + 2} (a,b) /\ 
    (!i. i IN 2..r+1 ==> w i IN aff_gt {vec 0,w 1 } {w 2} ) /\
    cyclic_set {w i | i  IN 1..r+1 } (vec 0) ((w 1) cross (w 2)) /\
    (!i. i IN 1..r ==> azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w i) = w (i+1)) /\
    pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\
    pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\
    (!i. ?e2. i IN 1..r+1  ==> &0 < e2 /\
       (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\ 
    (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1))) 
    ==> (?e. &0 < e /\ (!t. abs t < e ==>
			  f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\
			  f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC XIV_DEFORMATION;
  TYPED_ABBREV_TAC `dh = \ (i,j,k). dihV (vec 0) (w i) (w j) (w k)`;
  GEXISTL_TAC [`dh`;`a`;`b`];
  ASM_REWRITE_TAC[];
  INTRO_TAC KCZXLLE_SYM [`w o SUC`;`r`];
  REWRITE_TAC[o_THM;arith `1 <= r+1 /\ SUC 0 = 1 /\ SUC 1 = 2`];
  TYPIFY `{w (SUC i) | i <= r } = {w i | i IN 1..r+1}` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
    BY(MESON_TAC[arith `i <= r ==> (1 <= SUC i /\ SUC i <= r + 1)`;arith `(1 <= i /\ i <= r+1) ==> (PRE i <= r /\ SUC (PRE i) = i)`]);
  ASM_REWRITE_TAC[];
  TYPIFY_GOAL_THEN `(!i j.           i <= r /\ j <= r /\ ~(i = j)           ==> ~collinear {vec 0, w (SUC i), w (SUC j)})` (unlist REWRITE_TAC);
    REPEAT WEAKER_STRIP_TAC;
    RULE_ASSUM_TAC(REWRITE_RULE[pairwise]);
    FIRST_X_ASSUM (C INTRO_TAC [`SUC i`;`SUC j`]);
    REWRITE_TAC[SUC_INJ];
    ASM_REWRITE_TAC[];
    BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
  TYPIFY_GOAL_THEN `      (!i. 1 <= i /\ i <= r ==> w (SUC i) IN aff_gt {vec 0, w 1} {w 2})` (unlist REWRITE_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
  TYPIFY_GOAL_THEN `(!i. i < r           ==> azim_cycle {w i | i IN 1..r + 1} (vec 0) (w 1 cross w 2)               (w (SUC i)) =               w (SUC (i + 1)))` (unlist REWRITE_TAC);
    REPEAT WEAKER_STRIP_TAC;
    REWRITE_TAC[arith `SUC (i + 1) = SUC i + 1`];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
  TYPIFY `!i j k. i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i = k) /\ azim (vec 0) (w i) (w j) (w k) = &0 ==> dihV (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    GMATCH_SIMP_TAC (GSYM Polar_fan.AZIM_DIHV_SAME_STRONG);
    RULE_ASSUM_TAC (REWRITE_RULE[pairwise]);
    TYPIFY_GOAL_THEN `~collinear {vec 0, w i, w j} /\  ~collinear {vec 0, w i, w k}` (unlist REWRITE_TAC);
      BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
    ASM_REWRITE_TAC[];
    BY(MP_TAC PI_POS THEN REAL_ARITH_TAC);
  DISCH_TAC;
  EXPAND_TAC "dh" THEN REWRITE_TAC[];
  REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
  FIRST_X_ASSUM MP_TAC;
  TYPIFY_GOAL_THEN `(!i j k. k <= r /\      j <= r /\      1 <= r /\      i <= r /\      (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i)) ==> azim (vec 0) (w (SUC i)) (w (SUC j)) (w (SUC k)) = &0) <=> (!i j k.  k IN 1..r+1 /\ i IN 1..r+1 /\ j IN 1..r+1 /\ (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i))   ==> azim (vec 0) (w (i)) (w (j)) (w ( k)) = &0)` (unlist REWRITE_TAC);
    REWRITE_TAC[IN_NUMSEG];
    MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
    CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`PRE i`;`PRE j`;`PRE k`]);
      ASM_SIMP_TAC[arith `1 <= i ==> SUC (PRE i) = i`];
      DISCH_THEN MATCH_MP_TAC;
      BY(FIRST_X_ASSUM DISJ_CASES_TAC THEN REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM DISJ_CASES_TAC THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  DISCH_TAC;
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
    FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
    REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC);
    BY(ARITH_TAC);
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
    FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
    BY(REPLICATE_TAC 1(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MATCH_MP_TAC;
  FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
  FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
  BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC)
  ]);;
  (* }}} *)

(* was cycle_set_scale *)

let cyclic_set_scale = 
prove_by_refinement(
  `!U t (e:real^A). ~(t = &0) ==> (cyclic_set U (vec 0) (t % e) <=> cyclic_set U (vec 0) e)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.cyclic_set];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~FINITE U` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  ONCE_REWRITE_TAC[varith `vec 0 = a <=> a = vec 0`];
  ASM_REWRITE_TAC[VECTOR_MUL_EQ_0];
  TYPIFY `(e = vec 0)` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  RULE_ASSUM_TAC(REWRITE_RULE[]);
  ASM_REWRITE_TAC[];
  TYPIFY `affine hull {vec 0, t % e} = affine hull {vec 0,e}` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[AFFINE_HULL_2_ALT];
    REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_UNIV;arith `vec 0 + a = a /\ x - vec 0 = x`];
    GEN_TAC;
    REWRITE_TAC[VECTOR_MUL_ASSOC];
    BY(ASM_MESON_TAC[arith `~(t = &0) ==> u = (u * inv t) * t`]);
  TYPIFY `~(U INTER affine hull {vec 0, e} = {})` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  RULE_ASSUM_TAC(REWRITE_RULE[]) THEN ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `vec 0 - x =  -- x`];
  REWRITE_TAC[arith `-- (t % e) = t % (-- e)`];
  REWRITE_TAC[VECTOR_MUL_ASSOC];
  BY(ASM_MESON_TAC[arith `~(t = &0) ==> u = (u * inv t) * t`])
  ]);;
  (* }}} *)

let projection_scale = 
prove_by_refinement(
  `!e u t. (~(t = &0)) ==> projection (t % e) u = projection e u`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Sphere.projection];
  REWRITE_TAC[DOT_LMUL;DOT_RMUL];
  REWRITE_TAC[VECTOR_MUL_ASSOC];
  TYPIFY ` ((t * (u dot e)) / (t * t * (e dot e)) * t)  = (u dot e) / (e dot e)` (C SUBGOAL_THEN SUBST1_TAC);
    TYPIFY `e dot e = &0` ASM_CASES_TAC;
      ASM_REWRITE_TAC[];
      BY(REAL_ARITH_TAC);
    Calc_derivative.CALC_ID_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

let azim_cycle_scale = 
prove_by_refinement(
  `!U t e . (&0 < t)  ==> 
    azim_cycle U (vec 0) (t % e)  = azim_cycle U (vec 0) e `,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[FUN_EQ_THM];
  GEN_TAC;
  TYPIFY `U SUBSET {x}` ASM_CASES_TAC;
    BY(ASM_SIMP_TAC[Wrgcvdr_cizmrrh.W_SUBSET_SINGLETON_IMP_IDE]);
  REWRITE_TAC[Trigonometry.YESEEWW];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `x - vec 0 = x`];
  TYPIFY `(!x u. azim (vec 0) (t % e) x u = azim (vec 0) e x u) /\ (!u. projection (t % e) u = projection e u)` ENOUGH_TO_SHOW_TAC;
    BY(DISCH_THEN (unlist REWRITE_TAC));
  ASM_SIMP_TAC[AZIM_SPECIAL_SCALE];
  GEN_TAC;
  BY(ASM_SIMP_TAC[projection_scale;arith `&0 < t ==> ~(t = &0)`])
  ]);;
  (* }}} *)

let AZIM_CYCLE_SING_ALT = 
prove_by_refinement(
  `!x u v w. azim_cycle {v} x u w = v`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.azim_cycle];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `v = w` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[SUBSET_REFL]);
  TYPIFY_GOAL_THEN `~({v} SUBSET {w})` (unlist REWRITE_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
  TYPIFY_GOAL_THEN `!a b. {a} (b:real^3) <=> b IN {a}` (unlist REWRITE_TAC);
    BY(MESON_TAC[IN]);
  REWRITE_TAC[IN_SING];
  SELECT_TAC;
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM_ST `azim` MP_TAC;
  REWRITE_TAC[];
  TYPIFY `v` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_REWRITE_TAC[arith `x <= x`])
  ]);;
  (* }}} *)

let IDENTIFY_AZIM_CYCLE_SIMPLE = 
prove_by_refinement(
  `!W v w p u. ~(W SUBSET {p}) /\ p IN W /\
     cyclic_set W v w /\
     (~(u = p) /\ u IN W) /\
     (!q. ~(q = p) /\ q IN W /\ ~(q =u)          ==> azim v w p u < azim v w p q)
     ==> azim_cycle W v w p = u`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC Wrgcvdr_cizmrrh.IDENTIFY_AZIM_CYCLE;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
    BY(ASM_MESON_TAC [Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR]);
  CONJ_TAC;
    BY(ASM_MESON_TAC[IN]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `q = u` ASM_CASES_TAC;
    ASM_REWRITE_TAC[];
    BY(MESON_TAC[arith `x<=x`]);
  DISJ1_TAC;
  FIRST_X_ASSUM MATCH_MP_TAC;
  BY(ASM_MESON_TAC[IN])
  ]);;
  (* }}} *)

let coplanar_cross_scale = 
prove_by_refinement(
  `!u1 u2 v1 v2. coplanar {vec 0,u1,u2,v1,v2} /\ &0 < (v1 cross v2) dot (u1 cross u2) ==>
    (?t. &0 < t /\ v1 cross v2 = t % (u1 cross u2))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~collinear {vec 0,u1,u2}` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[GSYM CROSS_EQ_0];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `dot` MP_TAC THEN ASM_REWRITE_TAC[];
    REWRITE_TAC[DOT_RZERO];
    BY(REAL_ARITH_TAC);
  INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`u1`;`u2`;`v1`];
  INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`u1`;`u2`;`v2`];
  ASM_REWRITE_TAC[];
  TYPIFY_GOAL_THEN `coplanar {v2,vec 0,u1,u2} /\ coplanar {v1,vec 0,u1,u2} ` (unlist REWRITE_TAC);
    BY(ASM_MESON_TAC[COPLANAR_SUBSET;SET_RULE `{v2,v0,u1,u2} SUBSET {v0,u1,u2,v1,v2}`;SET_RULE `{v1,v0,u1,u2} SUBSET {v0,u1,u2,v1,v2}`]);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`u1`;`u2`;`v1`];
  INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`u1`;`u2`;`v2`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `v1 cross v2 = (t1' * t2 - t2' * t1) % (u1 cross u2)` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_REWRITE_TAC[CROSS_RADD;CROSS_LADD;CROSS_RMUL;CROSS_LMUL;CROSS_REFL];
    TYPIFY `u2 cross u1 = -- (u1 cross u2)` (C SUBGOAL_THEN SUBST1_TAC);
      BY(MESON_TAC[CROSS_SKEW]);
    BY(VECTOR_ARITH_TAC);
  TYPIFY `t1' * t2 - t2' * t1` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM_ST `dot` MP_TAC;
  ASM_REWRITE_TAC[DOT_LMUL];
  GMATCH_SIMP_TAC (CONJUNCT2 Real_ext.REAL_PROP_POS_LMUL);
  REWRITE_TAC[DOT_POS_LT];
  BY(ASM_MESON_TAC[CROSS_EQ_0])
  ]);;
  (* }}} *)

let azim_cycle_distinct = 
prove_by_refinement(
  `!U e v w.  FINITE U /\ v IN U /\ w IN U /\ ~(v = w) /\
    (!v. v IN U ==> ~(e dot (v cross azim_cycle U (vec 0) e v) = &0)) ==>
    (&0 < azim (vec 0) e v w)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(e = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`v`]);
    BY(ASM_REWRITE_TAC[DOT_LZERO]);
  TYPIFY `!v. v IN U ==> ~collinear {vec 0,e,v}` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC THEN DISCH_TAC;
    ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`v'`]);
    ASM_REWRITE_TAC[CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF];
    BY(REAL_ARITH_TAC);
  TYPIFY `~collinear {vec 0,e,azim_cycle U (vec 0) e v}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]);
  TYPIFY `&0 < azim (vec 0) e v (azim_cycle U (vec 0) e v)` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[azim_pos_iff_nz];
    GMATCH_SIMP_TAC AZIM_EQ_0;
    ASM_SIMP_TAC[];
    GMATCH_SIMP_TAC AFF_GT_2_1;
    REWRITE_TAC[IN_ELIM_THM];
    CONJ_TAC;
      BY(ASM_MESON_TAC[Fan.th3a]);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `dot` (C INTRO_TAC [`v`]);
    ASM_REWRITE_TAC[];
    TYPED_ABBREV_TAC `u = azim_cycle U (vec 0) e v`;
    FIRST_X_ASSUM_ST `%` SUBST1_TAC;
    REWRITE_TAC[DOT_RMUL;DOT_RADD;DOT_RZERO;CROSS_LADD;CROSS_LMUL;CROSS_LZERO;CROSS_REFL;DOT_CROSS_SELF];
    BY(REAL_ARITH_TAC);
  TYPIFY `w = azim_cycle U (vec 0) e v` ASM_CASES_TAC;
    BY(ASM_MESON_TAC[]);
  INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`e`;`v`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`w`]);
  ASM_REWRITE_TAC[];
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)


(*
let azim_cycle_nondeg = prove_by_refinement(
  `!U uu r. 
    1 < r /\
    U = {uu i | i IN 1..r+1 } /\
   (!i. i IN 1..r  ==> u i IN aff_gt{vec 0,u (r+1)} {u (r)} /\
      (!i. i IN 1..r ==> azim_cycle U (vec 0) (uu 1 cross uu 2) (uu i) = (uu (i+1))) /\
      azim_cycle U (vec 0) (uu 1 cross uu 2) (uu (r+1)) = u 1 /\
	(!i. i IN 1..r ==> &0 < (uu i cross uu (i+1)) dot (uu 1 cross uu 2))
	==>
	((!i. i IN 1..r ==> ~((uu 1 cross uu 2) dot (uu i cross uu (i+1)) = &0))
   (!i. 
      (`,
  (* {{{ proof *)
  [
  #
  ]);;
  (* }}} *)
*)


let azim_cycle_neg = 
prove_by_refinement(
  `!U e v w.  FINITE U /\ v IN U /\ azim_cycle U (vec 0) e v = w /\
    (!v. v IN U ==> ~(e dot (v cross azim_cycle U (vec 0) e v) = &0)) ==>
    (azim_cycle U (vec 0) (-- e) w = v)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(e = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`v`]);
    BY(ASM_REWRITE_TAC[DOT_LZERO]);
  TYPIFY `!v. v IN U ==> ~collinear {vec 0,e,v}` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC THEN DISCH_TAC;
    ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`v'`]);
    ASM_REWRITE_TAC[CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF];
    BY(REAL_ARITH_TAC);
  TYPIFY `w IN U` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]);
  PROOF_BY_CONTR_TAC;
  INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`-- (e:real^3)`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(v = w)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM_ST `dot` (C INTRO_TAC [`v`]);
    BY(ASM_REWRITE_TAC[CROSS_REFL;DOT_RZERO]);
  TYPIFY `&0 < azim (vec 0) e v w` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC azim_cycle_distinct;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM_ST `IN` (C INTRO_TAC [`v`]);
  ASM_REWRITE_TAC[];
  TYPED_ABBREV_TAC `w' = azim_cycle U (vec 0) (-- e) w`;
  TYPIFY `w' IN U` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]);
  REPEAT (GMATCH_SIMP_TAC Yxionxl2.AZIM_COMPL_NEG);
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  TYPIFY `azim (vec 0) e v w' + azim (vec 0) e w' w = azim (vec 0) e v w` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC (GSYM Fan.sum5_azim_fan);
    BY(ASM_SIMP_TAC[]);
  INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`(e:real^3)`;`v`];
  ASM_REWRITE_TAC[];
  DISCH_THEN (C INTRO_TAC [`w'`]);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `azim (vec 0) e v w + azim (vec 0) e w w' = azim (vec 0) e v w'` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC (GSYM Fan.sum4_azim_fan);
    BY(ASM_SIMP_TAC[]);
  TYPIFY `&0 <= azim (vec 0) e w w' /\ &0 <= azim (vec 0) e w' w` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
  TYPIFY `azim (vec 0) e w w' = &0` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  TYPIFY `(w' = w)` (C SUBGOAL_THEN ASSUME_TAC);
    PROOF_BY_CONTR_TAC;
    INTRO_TAC azim_cycle_distinct [`U`;` (e:real^3)`;`w`;`w'`];
    ASM_REWRITE_TAC[];
    BY(REAL_ARITH_TAC);
  INTRO_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`U`;`w`;`-- (e:real^3)`;`(vec 0):real^3`];
  ASM_REWRITE_TAC[];
  BY(ASM_TAC THEN SET_TAC[])
  ]);;
  (* }}} *)

(*
let azim_cycle_neg = prove_by_refinement(
  `!U e v w. ~(U SUBSET {w}) /\ FINITE U /\ cyclic_set U (vec 0) e /\ v IN U /\ ~(e dot (v cross w) = &0) /\
    azim_cycle U (vec 0) (e ) v = w ==>
    azim_cycle U (vec 0) (-- e) w  = v`,
  (* {{{ proof *)
  [
g/r
typ `U SUBSET {v}` asmcase
    art[Sphere.azim_cycle]
amt[]
st/r
intro (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`U`;`v`;`e`;`(vec 0):real^3`]
art[]
st/r
mmp IDENTIFY_AZIM_CYCLE_SIMPLE
art[]
conj
art[IN]
conj
rt[arith `-- e = (-- &1) % e`]
gm cyclic_set_scale
art[]
rat
st/r
fxa (C intro [`q`])
ants
amt[IN]
dt
repeat (gm Yxionxl2.AZIM_COMPL_NEG)
typ `~collinear {vec 0, e, w} /\ ~collinear {vec 0, e, q} /\ ~collinear {vec 0, e, v}` sat
ort[setr `{a,e,w} = {w,a,e}`]
repeat (gm Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR)
amt[IN]
art[]
rt[arith `x < y <=> ~(y <= x)`]
dt
(* COME BACK. TO HERE. still problems with degenerate cases. make azim progression condition on all of U *)
  ]);;
  (* }}} *)
*)

let XIV_ECAU_BACK = 
prove_by_refinement(
  `!f r w a b.
    deformation f {w i | i <= r + 2} (a,b) /\ 
    1 <= r /\
    (!i. i IN 1..r ==> w i IN aff_gt {vec 0,w (r+1) } {w r} ) /\
    cyclic_set {w i | i  IN 1..r+1 } (vec 0) ((w 1) cross (w 2)) /\
    // &0 < (w r cross (w (r+1))) dot (w 1 cross w 2) /\
    (!i. i IN 1..r ==> &0 < (w i cross (w (i+1))) dot (w 1 cross w 2)) /\
    {w 1, w 2} SUBSET aff_gt {vec 0,w (r+1)} {w r} /\
    (!i. i IN 1..r ==> azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w i) = w (i+1)) /\
    azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w (r+1)) = w 1 /\
    pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\
    pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\
    (!i. ?e2. i IN 1..r+1  ==> &0 < e2 /\
       (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\ 
    (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1))) 
    ==> (?e. &0 < e /\ (!t. abs t < e ==>
			  f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\
			  f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `&0 < (w r cross (w (r+1))) dot (w 1 cross w 2)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM MATCH_MP_TAC;
    REWRITE_TAC[IN_NUMSEG];
    BY(ASM_REWRITE_TAC[arith `r <= (r:num)`]);
  MATCH_MP_TAC XIV_DEFORMATION;
  TYPED_ABBREV_TAC `dh = \ (i,j,k). dihV (vec 0) (w i) (w j) (w k)`;
  GEXISTL_TAC [`dh`;`a`;`b`];
  ASM_REWRITE_TAC[];
  INTRO_TAC KCZXLLE_SYM [`\i. w((r+1)-i) `;`r`];
  REWRITE_TAC[arith `1 <= r+1 /\ ((r+1)-0 = (r+1)) /\ ((r+1)-1 = r)`];
  TYPIFY `{w ((r+1)-i) | i | i <= r } = {w i | i IN 1..r+1}` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
    GEN_TAC;
    MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
    CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC;
      ASM_REWRITE_TAC[];
      TYPIFY `(r+1)-i` EXISTS_TAC;
      REWRITE_TAC[];
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    ASM_REWRITE_TAC[];
    TYPIFY `(r+1)-i` EXISTS_TAC;
    CONJ_TAC;
      BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    AP_TERM_TAC;
    BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  COMMENT "collinear";
  TYPIFY_GOAL_THEN `(!i j.           i <= r /\ j <= r /\ ~(i = j)           ==> ~collinear {vec 0, w ((r+1)-i), w ((r+1)-j)})` (unlist REWRITE_TAC);
    REPEAT WEAKER_STRIP_TAC;
    RULE_ASSUM_TAC(REWRITE_RULE[pairwise]);
    FIRST_X_ASSUM (C INTRO_TAC [`(r+1)-i`;`(r+1)-j`]);
    ASM_REWRITE_TAC[];
    BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
  COMMENT "aff_gt";
  TYPIFY_GOAL_THEN `      (!i. 1 <= i /\ i <= r ==> w ((r+1)-i) IN aff_gt {vec 0, w (r+1)} {w r})` (unlist REWRITE_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
  COMMENT "cyclic set";
  INTRO_TAC coplanar_cross_scale [`w 1`;`w 2`;`w r`;`w (r+1)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[coplanar];
    GEXISTL_TAC [`(vec 0):real^3`;`w r`;`w (r+1)`];
    TYPIFY `{vec 0,w r, w (r+1)} SUBSET affine hull {vec 0, w r, w (r + 1)} /\ {w 1, w 2} SUBSET affine hull {vec 0, w r, w (r + 1)}` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    CONJ_TAC;
      BY(REWRITE_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL]);
    MATCH_MP_TAC SUBSET_TRANS;
    TYPIFY `aff_gt {vec 0,w(r+1)} {w r}` EXISTS_TAC;
    CONJ_TAC;
      BY(ASM_REWRITE_TAC[]);
    TYPIFY `{vec 0,w r, w(r+1)} = {vec 0,w (r+1)} UNION {w (r)}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `         cyclic_set {w i | i IN 1..r + 1} (vec 0) (w (r + 1) cross w r)` (C SUBGOAL_THEN ASSUME_TAC);
    ONCE_REWRITE_TAC[CROSS_SKEW];
    ASM_REWRITE_TAC[];
    REWRITE_TAC[arith `-- (t % v) = (-- t) % v`];
    GMATCH_SIMP_TAC cyclic_set_scale;
    ASM_REWRITE_TAC[];
    BY(FIRST_X_ASSUM_ST `&0 < t` MP_TAC THEN REAL_ARITH_TAC);
  COMMENT "azim_cycle";
  TYPIFY `(!i. i < r               ==> azim_cycle {w i | i IN 1..r + 1} (vec 0)                   (w (r + 1) cross w r)                   (w ((r + 1) - i)) =                   w ((r + 1) - (i + 1)))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    ONCE_REWRITE_TAC[CROSS_SKEW];
    ASM_REWRITE_TAC[];
    REWRITE_TAC[arith `-- (t % v) = t % (-- v)`];
    GMATCH_SIMP_TAC azim_cycle_scale;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC azim_cycle_neg;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      TYPIFY `{w i | i IN 1..r+1} = IMAGE w (1..r+1)` (C SUBGOAL_THEN SUBST1_TAC);
        BY(SET_TAC[]);
      MATCH_MP_TAC FINITE_IMAGE;
      BY(REWRITE_TAC[FINITE_NUMSEG]);
    TYPIFY `(r+1)-(i+1) = r - i` (C SUBGOAL_THEN SUBST1_TAC);
      BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
    CONJ_TAC;
      REWRITE_TAC[IN_ELIM_THM;IN_NUMSEG];
      TYPIFY `r- (i:num)` EXISTS_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
    CONJ_TAC;
      TYPIFY `(r+1) - i = (r - i) + 1` (C SUBGOAL_THEN SUBST1_TAC);
        BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(REWRITE_TAC[IN_NUMSEG] THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
    REWRITE_TAC[IN_NUMSEG;IN_ELIM_THM];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    ASM_REWRITE_TAC[];
    TYPIFY `(i':num) < r+1` ASM_CASES_TAC;
      TYPIFY `azim_cycle {w i | 1 <= i /\ i <= r + 1} (vec 0) (w 1 cross w 2) (w i') = w (i'+1)` (C SUBGOAL_THEN SUBST1_TAC);
        REWRITE_TAC[GSYM IN_NUMSEG];
        FIRST_X_ASSUM MATCH_MP_TAC;
        BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
      MATCH_MP_TAC (arith `&0 < x ==> ~(x = &0)`);
      REWRITE_TAC[DOT_SYM];
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(REWRITE_TAC[IN_NUMSEG] THEN REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    TYPIFY `i' = r+1` (C SUBGOAL_THEN ASSUME_TAC);
      BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    ASM_REWRITE_TAC[GSYM IN_NUMSEG];
    TYPIFY `w 1 IN aff_gt {vec 0, w(r+1)} {w r}` (C SUBGOAL_THEN MP_TAC);
      BY(FIRST_X_ASSUM_ST `aff_gt` MP_TAC THEN SET_TAC[]);
    GMATCH_SIMP_TAC AFF_GT_2_1;
    REWRITE_TAC[IN_ELIM_THM];
    CONJ_TAC;
      MATCH_MP_TAC Fan.th3a;
      RULE_ASSUM_TAC(REWRITE_RULE[pairwise]);
      FIRST_X_ASSUM MATCH_MP_TAC;
      REWRITE_TAC[IN_NUMSEG];
      BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    TYPED_ABBREV_TAC `e = w 1 cross w 2`;
    FIRST_X_ASSUM_ST `dot` MP_TAC;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_RZERO;CROSS_REFL;DOT_RMUL;DOT_RADD;DOT_RZERO];
    REWRITE_TAC[arith `t * &0 + x = x`];
    ONCE_REWRITE_TAC[CROSS_SKEW];
    REWRITE_TAC[DOT_RNEG;REAL_ENTIRE];
    ONCE_REWRITE_TAC[DOT_SYM];
    BY(REPEAT (FIRST_X_ASSUM_ST `&0 < x` MP_TAC) THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `!i j k. P` MP_TAC;
  ASM_REWRITE_TAC[];
  REPLICATE_TAC 4 (FIRST_X_ASSUM kill);
  DISCH_TAC;
  COMMENT "work on dihedral angles";
  TYPIFY `!i j k.          k IN 1..r+1 /\          j IN 1..r+1 /\          i IN 1..r+1 /\          (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i))          ==> azim (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[IN_NUMSEG];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`(r+1)-i`;`(r+1)-j`;`(r+1)-k`]);
    ASM_SIMP_TAC[arith `i <= r+1 ==> (r+1)-((r+1)-i) = i`];
    DISCH_THEN MATCH_MP_TAC;
    BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  FIRST_X_ASSUM_ST `(r+1)-i` kill;
  TYPIFY `!i j k. i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i = k) /\ azim (vec 0) (w i) (w j) (w k) = &0 ==> dihV (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    GMATCH_SIMP_TAC (GSYM Polar_fan.AZIM_DIHV_SAME_STRONG);
    RULE_ASSUM_TAC (REWRITE_RULE[pairwise]);
    TYPIFY_GOAL_THEN `~collinear {vec 0, w i, w j} /\  ~collinear {vec 0, w i, w k}` (unlist REWRITE_TAC);
      BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
    ASM_REWRITE_TAC[];
    BY(MP_TAC PI_POS THEN REAL_ARITH_TAC);
  EXPAND_TAC "dh" THEN REWRITE_TAC[];
  REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
  FIRST_X_ASSUM MP_TAC;
  DISCH_TAC;
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
    FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
    REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC);
    BY(ARITH_TAC);
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
    FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
    BY(REPLICATE_TAC 1(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MATCH_MP_TAC;
  FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
  FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
  BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC)
  ]);;
  (* }}} *)

let zlz_wedge_boundary = 
prove_by_refinement(
  `!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) /\
     (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
	 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==>
   (!x v. ?e3. x IN FF /\ v IN V
           ==> &0 < e3 /\
               (!t. --e3 < t /\ t < e3
                    ==> (f v t) IN 
                        wedge_in_fan_ge (f (FST x) t,f (SND x) t)
                        (IMAGE (IMAGE (\v. f v t)) E)))`,

  (* {{{ proof *)
  [
  COMMENT "start here";
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
  REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `w = FST x`;
  TYPIFY `x = (w,rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `FST x,SND x = (w,rho_node1 FF w)` ENOUGH_TO_SHOW_TAC;
      BY(REWRITE_TAC[PAIR]);
    ASM_REWRITE_TAC[PAIR_EQ];
    MATCH_MP_TAC EQ_SYM;
    MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE;
    BY(ASM_MESON_TAC[PAIR]);
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
  TYPIFY `w IN V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]);
  TYPIFY `v IN {w, rho_node1 FF w, ivs_rho_node1 FF w}` ASM_CASES_TAC;
    INTRO_TAC zlz_wedge_refl [`a`;`b`;`V`;`E`;`FF`;`f`];
    ASM_REWRITE_TAC[];
    DISCH_THEN (C INTRO_TAC [`v`;`w`]);
    BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]);
  TYPIFY `rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `v IN wedge (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` ASM_CASES_TAC;
    INTRO_TAC zlz_wedge_open [`a`;`b`;`V`;`E`;`FF`;`f`];
    ASM_REWRITE_TAC[];
    DISCH_THEN (C INTRO_TAC [`v`;`w`]);
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `v IN wedge_ge  (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC);
    RULE_ASSUM_TAC(REWRITE_RULE[Localization.convex_local_fan]);
    ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`w,rho_node1 FF w`]);
    ASM_REWRITE_TAC[];
    REWRITE_TAC[SUBSET];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`v`]);
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
    BY(ASM_MESON_TAC[]);
  TYPIFY `azim (vec 0) w (rho_node1 FF w) v = &0 \/ azim (vec 0) w (rho_node1 FF w) v = azim  (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM MP_TAC;
    BY(ASM_REWRITE_TAC[Reuhady.WEDGE_GE_WEDGE;IN_UNION;IN_ELIM_THM]);
  TYPIFY `?r. r < CARD V /\ v = ITER r (rho_node1 FF) w` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC (GEN_ALL Local_lemmas.LOFA_IMP_LT_CARD_SET_V) [`E`;`FF`;`V`;`w`];
    REWRITE_TAC[EXTENSION;IN_ELIM_THM];
    ASM_REWRITE_TAC[];
    DISCH_THEN (C INTRO_TAC [`v`]);
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
  TYPIFY `1 < r /\ r < CARD V - 1` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `~(r = 0) /\ ~(r = 1) /\ ~(r = CARD V - 1)` ENOUGH_TO_SHOW_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
    REWRITE_TAC[GSYM DE_MORGAN_THM];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `~(ITER r f w IN s INSERT t)` MP_TAC;
    REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_REWRITE_TAC[ITER;ITER_1];
      BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]);
    BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]);
  INTRO_TAC (GEN_ALL Local_lemmas.EGHNAVX) [`E`;`V`;`(\i. azim (vec 0) w (rho_node1 FF w) (ITER i (rho_node1 FF) w))`;`FF`;`r`;`w`;`(\i. ITER i (rho_node1 FF) w)`;`CARD V` ];
  ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;ITER_1];
  ANTS_TAC;
    MATCH_MP_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN;
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[LEFT_IMP_EXISTS_THM];
  ASM_SIMP_TAC[arith `1 < r ==> 0 < r`];
  (REPEAT WEAKER_STRIP_TAC);
  COMMENT "added material here";
  COMMENT "eliminate wedge_in_fan_ge";
  TYPIFY `?e3. &0 < e3 /\      (!t. --e3 < t /\ t < e3           ==> f (ITER r (rho_node1 FF) w) t IN               wedge_ge (vec 0) (f w t) (f (rho_node1 FF w) t) (f (ivs_rho_node1 FF w) t))` ENOUGH_TO_SHOW_TAC;
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `if (e <= e3) then e else e3` EXISTS_TAC;
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `abs t < e` (C SUBGOAL_THEN ASSUME_TAC);
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
    CONJ_TAC;
      TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      REWRITE_TAC[IN_IMAGE];
      TYPIFY `w` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM_ST `wedge_ge` (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[];
    DISCH_THEN MATCH_MP_TAC;
    BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  INTRO_TAC zlz_azim [`a`;`b`;`V`;`E`;`FF`;`f`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  TYPIFY `!v. v IN V ==> &0 < azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v)` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC (GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) [`E`;`V`;`FF`];
    ASM_REWRITE_TAC[];
    DISCH_THEN (GMATCH_SIMP_TAC o GSYM);
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC Local_lemmas.INTERIOR_ANGLE1_POS;
    BY(ASM_REWRITE_TAC[]);
  COMMENT "azim_in_fan -> azim";
  TYPIFY `!v. ?e2. v IN V                ==> &0 < e2 /\                   (!t. --e2 < t /\ t < e2                        ==> azim (vec 0) (f v t) (f (rho_node1 FF v) t) (f (ivs_rho_node1 FF v) t) <= pi)` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`v', rho_node1 FF v'`]);
    REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
    GMATCH_SIMP_TAC Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2;
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `if (e <= e2) then e else e2` EXISTS_TAC;
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `abs t < e /\ abs t < e2` (C SUBGOAL_THEN ASSUME_TAC);
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`v'`;`t`];
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`v'`;`t`];
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `azim_in_fan` (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[arith `-- e2 < t /\ t < e2 <=> abs t < e2`];
    MATCH_MP_TAC (arith `(a = b) ==> (a <= pi ==> b <= pi)`);
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND;
    TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[IN_IMAGE];
    TYPIFY `v'` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC);
  FIRST_X_ASSUM kill;
  COMMENT "end added";
  COMMENT "MAIN BRANCH: follow forward azim = 0";
  FIRST_X_ASSUM DISJ_CASES_TAC;
    FIRST_X_ASSUM MP_TAC;
    FIRST_X_ASSUM kill;
    DISCH_TAC;
    FIRST_X_ASSUM_ST `interior_angle1` MP_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MP_TAC;
    REPLICATE_TAC 2 (FIRST_X_ASSUM kill);
    REPEAT WEAKER_STRIP_TAC;
    COMMENT "add KOM";
    INTRO_TAC Local_lemmas.KOMWBWC [`E`;`V`;`affine hull {(vec 0),w,rho_node1 FF w}`;`r`;`FF`;`{ITER i (rho_node1 FF) w | i <= r}`;`w cross rho_node1 FF w`;`ITER r (rho_node1 FF) w`;`w`];
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      REWRITE_TAC[plane];
      CONJ_TAC;
        GEXISTL_TAC [`(vec 0):real^3`;`w`;`rho_node1 FF w`];
        REWRITE_TAC[];
        BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]);
      CONJ_TAC;
        MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
        BY(SET_TAC[]);
      REWRITE_TAC[SUBSET;IN_ELIM_THM];
      REPEAT WEAKER_STRIP_TAC;
      ASM_REWRITE_TAC[];
      ASM_CASES_TAC `i=0`;
        ASM_REWRITE_TAC[ITER];
        MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
        BY(SET_TAC[]);
      TYPIFY `aff_gt {vec 0,w} {rho_node1 FF w} SUBSET affine hull {vec 0,w,rho_node1 FF w}` ENOUGH_TO_SHOW_TAC;
        FIRST_X_ASSUM (C INTRO_TAC [`ITER i (rho_node1 FF) w`;`i`]);
        ASM_SIMP_TAC[arith `~(i=0) ==> (0 < i)`];
        BY(SET_TAC[]);
      TYPIFY `{vec 0,w,rho_node1 FF w } = {vec 0,w} UNION {rho_node1 FF w}` (C SUBGOAL_THEN SUBST1_TAC);
        BY(SET_TAC[]);
      BY(REWRITE_TAC[AFF_GT_SUBSET_AFFINE_HULL]);
    REPEAT WEAKER_STRIP_TAC;
    COMMENT "abbreviate uu";
    TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
      MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
      BY(ASM_REWRITE_TAC[]);
    TYPIFY `!i. ITER i (rho_node1 FF) (ivs_rho_node1 FF w) IN V` (C SUBGOAL_THEN ASSUME_TAC);
      MATCH_MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V;
      BY(ASM_REWRITE_TAC[]);
    TYPED_ABBREV_TAC `w0 = ivs_rho_node1 FF w`;
    TYPED_ABBREV_TAC `uu = (\i. ITER i (rho_node1 FF) w0)`;
    TYPIFY `!i. ITER i (rho_node1 FF) w0 = uu i` (C SUBGOAL_THEN ASSUME_TAC);
      EXPAND_TAC "uu";
      BY(REWRITE_TAC[]);
    TYPIFY `w0 = uu 0 /\ w = uu 1 /\ rho_node1 FF w = uu 2 /\ (!i. ITER i (rho_node1 FF) w = uu (i+1))` (C SUBGOAL_THEN ASSUME_TAC);
      EXPAND_TAC "uu";
      REWRITE_TAC[ITER;ITER_1];
      EXPAND_TAC "w0";
      REWRITE_TAC[arith `2 = 1+1`;GSYM ITER_ADD;ITER_1];
      REPEAT (GMATCH_SIMP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS);
      BY(ASM_MESON_TAC[]);
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM (fun t -> RULE_ASSUM_TAC(REWRITE_RULE[t]) THEN ASSUME_TAC t);
    COMMENT "apply XIV_ECAU";
    TYPIFY `(?e3. &0 < e3 /\                  (!t. abs t < e3                       ==> f (uu 1) t IN                           wedge_ge (vec 0) (f (uu (r + 1)) t)                           (f (uu (r + 2)) t)                           (f (uu r) t) /\                           f (uu (r + 1)) t IN                           wedge_ge (vec 0) (f (uu 1) t) (f (uu 2) t)                           (f (uu 0) t)))` ENOUGH_TO_SHOW_TAC;
      REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
      BY(MESON_TAC[]);
    MATCH_MP_TAC XIV_ECAU;
    GEXISTL_TAC [`a`;`b`];
    COMMENT "cyclic set condition";
    TYPIFY `{uu i | i IN 1 .. r+1} = {uu (i+1) | i <= r}` (C SUBGOAL_THEN SUBST1_TAC);
      REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
      GEN_TAC;
      MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
      CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC;
        TYPIFY `PRE i` EXISTS_TAC;
        ASM_SIMP_TAC[arith `1 <= i ==> PRE i + 1 = i`];
        BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
      TYPIFY `i+1` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      BY(REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    ASM_REWRITE_TAC[];
    COMMENT "deformation condition";
    CONJ_TAC;
      MATCH_MP_TAC deformation_subset;
      TYPIFY `V` EXISTS_TAC;
      ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM];
      BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
    COMMENT "aff_gt";
    CONJ_TAC;
      REWRITE_TAC[IN_NUMSEG];
      REPEAT WEAKER_STRIP_TAC;
      GMATCH_SIMP_TAC (arith `2 <= i ==> i = PRE i + 1`);
      ASM_REWRITE_TAC[];
      FIRST_X_ASSUM MATCH_MP_TAC;
      TYPIFY `uu (PRE i + 1)` EXISTS_TAC;
      BY(REWRITE_TAC[] THEN (REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC));
    COMMENT "azim_cycle";
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`uu i`;`PRE i`]);
      DISCH_THEN GMATCH_SIMP_TAC;
      CONJ_TAC;
        BY(FIRST_X_ASSUM MP_TAC THEN (REWRITE_TAC[IN_NUMSEG]) THEN MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`;arith `i <= r /\ 1 <= i ==> PRE i < r`]);
      TYPIFY `uu i = ITER i (rho_node1 FF) (uu 0) /\ uu (i+1) = ITER (i+1) (rho_node1 FF) (uu 0)` ENOUGH_TO_SHOW_TAC;
        DISCH_THEN (unlist REWRITE_TAC);
        REWRITE_TAC[arith `i + 1 = 1 +i`];
        BY(REWRITE_TAC[GSYM ITER_ADD;ITER_1]);
      BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
    TYPIFY `!i. 1 <= i ==> rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` (C SUBGOAL_THEN ASSUME_TAC);
      (FIRST_X_ASSUM_ST `ITER` kill);
      FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM);
      REPEAT WEAKER_STRIP_TAC;
      REWRITE_TAC[arith `i+1 = 1+i`];
      REWRITE_TAC[GSYM ITER_ADD;ITER_1];
      GMATCH_SIMP_TAC (arith `1 <= i ==> i = 1 + (i - 1)`);
      ASM_REWRITE_TAC[GSYM ITER_ADD;ITER_1];
      GMATCH_SIMP_TAC Local_lemmas.IVS_RHO_IDD;
      CONJ_TAC;
        BY(ASM_MESON_TAC[]);
      REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
      BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
    COMMENT "0 < azim";
    TYPIFY_GOAL_THEN ` (!i. i IN 1..r + 1 ==> &0 < azim (vec 0) (uu i) (uu (i + 1)) (uu (i - 1)))` (unlist REWRITE_TAC);
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM_ST `&0 < azim a b c d` (C INTRO_TAC [`uu i`]);
      ANTS_TAC;
        BY(ASM_MESON_TAC[]);
      TYPIFY `rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` ENOUGH_TO_SHOW_TAC;
        BY(DISCH_THEN (unlist REWRITE_TAC));
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]);
    COMMENT "azim <= pi";
    TYPIFY_GOAL_THEN `(!i. ?e2. i IN 1..r + 1            ==> &0 < e2 /\               (!t. abs t < e2                    ==> azim (vec 0) (f (uu i) t) (f (uu (i + 1)) t)                        (f (uu (i - 1)) t) <=                        pi))` (unlist REWRITE_TAC);
      GEN_TAC;
      REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
      DISCH_TAC;
      FIRST_X_ASSUM_ST `azim a b c d <= pi` (C INTRO_TAC [`uu i`]);
      REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
      ANTS_TAC;
        BY(ASM_MESON_TAC[]);
      (REPEAT WEAKER_STRIP_TAC);
      TYPIFY `e2` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`t`]);
      ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
      TYPIFY `rho_node1 FF (uu i) = uu(i+1) /\ ivs_rho_node1 FF (uu i) = uu (i - 1)` ENOUGH_TO_SHOW_TAC;
        BY(DISCH_THEN (unlist REWRITE_TAC));
      BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]);
    COMMENT "pairwise";
    REWRITE_TAC[pairwise];
    TYPIFY `!i. uu (i) IN V` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]);
    TYPIFY `(!i j. i IN 0..r+1 /\ j IN 0..r+1 /\ ~(i = j)==> ~(uu i = uu j)) /\ (!i j. i IN 1..r+2 /\ j IN 1..r+2 /\ ~(i=j) ==> ~(uu i = uu j))` ENOUGH_TO_SHOW_TAC;
      REPEAT (FIRST_X_ASSUM_ST `azim` kill);
      BY(ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN_ALT]);
    CONJ_TAC;
      REWRITE_TAC[IN_NUMSEG];
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MP_TAC;
      FIRST_X_ASSUM_ST `ITER` kill;
      REWRITE_TAC[];
      FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM);
      BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `i <= r+1 /\ 1 < r /\ r < CARD V - 1 ==> i < CARD V`]);
    TYPIFY `!i. 1 <= i ==> uu i = ITER (PRE i) (rho_node1 FF) (w)` (C SUBGOAL_THEN ASSUME_TAC);
      ASM_REWRITE_TAC[];
      BY(MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`]);
    REWRITE_TAC[IN_NUMSEG];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[];
    FIRST_X_ASSUM_ST `ITER` (REPEAT o GMATCH_SIMP_TAC);
    TYPIFY `w IN V` (C SUBGOAL_THEN MP_TAC);
      BY(ASM_REWRITE_TAC[]);
    TYPIFY `PRE i < CARD V /\ PRE j < CARD V` (C SUBGOAL_THEN MP_TAC);
      BY(REPEAT (FIRST_X_ASSUM_ST `CARD` MP_TAC) THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[arith `1<= i /\ i <= r+2 /\ 1 < r /\ r < CARD V - 1 ==> PRE i < CARD V`]);
    REPEAT (FIRST_X_ASSUM_ST `local_fan` MP_TAC);
    REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
    BY(MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `1 <= i /\ 1 <= j /\ PRE i = PRE j ==> (i = j)`]);
  (COMMENT "SECOND MAIN BRANCH");
  FIRST_X_ASSUM_ST `azim a b c d = &0` kill;
  TYPIFY `ITER (CARD V - 1) (rho_node1 FF) w = ivs_rho_node1 FF w` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM_ST `interior_angle1` MP_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `r' = CARD V - r`;
  TYPED_ABBREV_TAC `w' = ITER r (rho_node1 FF) w`;
  COMMENT "add KOM";
  INTRO_TAC Local_lemmas.KOMWBWC [`E`;`V`;`affine hull {(vec 0),w,ivs_rho_node1 FF w}`;`r'`;`FF`;`{ITER i (rho_node1 FF) w' | i <= r'}`;`w' cross rho_node1 FF w'`;`w`;`w'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    REWRITE_TAC[plane];
    CONJ_TAC;
      GEXISTL_TAC [`(vec 0):real^3`;`w`;`ivs_rho_node1 FF w`];
      REWRITE_TAC[];
      BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]);
    CONJ_TAC;
      MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
      BY(SET_TAC[]);
    REWRITE_TAC[SUBSET;IN_ELIM_THM];
    REPEAT WEAKER_STRIP_TAC;
    ASM_REWRITE_TAC[];
    EXPAND_TAC "w'";
    REWRITE_TAC[ITER_ADD];
    ASM_CASES_TAC `(i:num)=r'`;
      ASM_REWRITE_TAC[];
      TYPIFY `r' + r = CARD V` (C SUBGOAL_THEN SUBST1_TAC);
        BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `r < CARD V - 1` MP_TAC THEN ARITH_TAC);
      GMATCH_SIMP_TAC Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2;
      CONJ_TAC;
        BY(ASM_MESON_TAC[]);
      MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
      BY(SET_TAC[]);
    TYPIFY `aff_gt {vec 0,w} {ivs_rho_node1 FF w} SUBSET affine hull {vec 0,w,ivs_rho_node1 FF w}` ENOUGH_TO_SHOW_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`ITER (i+r) (rho_node1 FF) w`;`i+(r:num)`]);
      ANTS_TAC;
        ASM_REWRITE_TAC[arith `r <= (i:num) + r`];
        BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `r < CARD V - 1` MP_TAC THEN ARITH_TAC);
      BY(SET_TAC[]);
    TYPIFY `{vec 0,w,ivs_rho_node1 FF w } = {vec 0,w} UNION {ivs_rho_node1 FF w}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(REWRITE_TAC[AFF_GT_SUBSET_AFFINE_HULL]);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "abbreviate uu, forward order";
  TYPIFY `ivs_rho_node1 FF w' IN V` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i. ITER i (rho_node1 FF) (ivs_rho_node1 FF w') IN V` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V;
    BY(ASM_REWRITE_TAC[]);
  TYPED_ABBREV_TAC `w0 = ivs_rho_node1 FF w'`;
  TYPED_ABBREV_TAC `uu = (\i. ITER i (rho_node1 FF) w0)`;
  TYPIFY `!i. ITER i (rho_node1 FF) w0 = uu i` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "uu";
    BY(REWRITE_TAC[]);
  TYPIFY `w0 = uu 0 /\ w' = uu 1 /\ rho_node1 FF w' = uu 2 /\ (!i. ITER i (rho_node1 FF) w' = uu (i+1))` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "uu";
    REWRITE_TAC[ITER;ITER_1];
    EXPAND_TAC "w0";
    REWRITE_TAC[arith `2 = 1+1`;GSYM ITER_ADD;ITER_1];
    REPEAT (GMATCH_SIMP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS);
    BY(ASM_MESON_TAC[]);
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM (fun t -> RULE_ASSUM_TAC(REWRITE_RULE[t]) THEN ASSUME_TAC t);
  TYPIFY `1 < r' /\ r' < CARD V - 1` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "r'";
    BY(FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC THEN ARITH_TAC);
  TYPIFY `ivs_rho_node1 FF w = uu(r')` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `r' = PRE r' + 1` (C SUBGOAL_THEN SUBST1_TAC);
      BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
    TYPIFY `uu (PRE r' + 1) = ITER (PRE r') (rho_node1 FF) (ITER r (rho_node1 FF) w)` (C SUBGOAL_THEN SUBST1_TAC);
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[ITER_ADD];
    TYPIFY `PRE r' + r = CARD V - 1` (C SUBGOAL_THEN SUBST1_TAC);
      EXPAND_TAC "r'";
      BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V-1` MP_TAC) THEN ARITH_TAC);
    GMATCH_SIMP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1;
    BY(ASM_MESON_TAC[]);
  TYPIFY `!i j. ITER i (rho_node1 FF) (uu j) = uu (i+j)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `ITER` kill;
    FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM);
    BY(REWRITE_TAC[ITER_ADD]);
  TYPIFY `w = uu (r'+1)` (C SUBGOAL_THEN ASSUME_TAC);
    ONCE_REWRITE_TAC[arith `r' + 1 = 1 + r'`];
    FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
    REWRITE_TAC[ITER_1];
    FIRST_X_ASSUM ((unlist REWRITE_TAC) o GSYM);
    BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]);
  TYPIFY `rho_node1 FF w = uu (r'+2)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM SUBST1_TAC;
    REWRITE_TAC[arith `r' + 2 = 1 + (r' + 1)`];
    BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[ITER_1]);
  ASM_REWRITE_TAC[];
  COMMENT "apply XIV_ECAU";
  TYPIFY `(?e3. &0 < e3 /\                  (!t. abs t < e3                       ==> f (uu 1) t IN                           wedge_ge (vec 0) (f (uu (r' + 1)) t)                           (f (uu (r' + 2)) t)                           (f (uu r') t) /\                           f (uu (r' + 1)) t IN                           wedge_ge (vec 0) (f (uu 1) t) (f (uu 2) t)                           (f (uu 0) t)))` ENOUGH_TO_SHOW_TAC;
    REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
    BY(MESON_TAC[]);
  MATCH_MP_TAC XIV_ECAU_BACK;
  GEXISTL_TAC [`a`;`b`];
  COMMENT "cyclic set condition";
  TYPIFY `{uu i | i IN 1 .. r'+1} = {uu (i+1) | i <= r'}` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
    GEN_TAC;
    MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
    CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC;
      TYPIFY `PRE i` EXISTS_TAC;
      ASM_SIMP_TAC[arith `1 <= i ==> PRE i + 1 = i`];
      BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    TYPIFY `i+1` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    BY(REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  ASM_REWRITE_TAC[];
  COMMENT "deformation condition";
  CONJ_TAC;
    MATCH_MP_TAC deformation_subset;
    TYPIFY `V` EXISTS_TAC;
    ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM];
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
  ASM_SIMP_TAC[arith `1 < r' ==> 1 <= r'`];
  COMMENT "aff_gt";
  TYPIFY `!i. uu(i+ CARD V) = uu i` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    INTRO_TAC Localization.PERIODIC_RHO_NODE1 [`V`;`E`;`FF`;`uu 0`];
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[Oxl_def.periodic];
    ASM_REWRITE_TAC[];
    BY(MESON_TAC[]);
  TYPIFY `!i. r <= i ==> ITER i (rho_node1 FF) w = uu (i - (r-1))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `ITER i = ITER ((i-r) + r)` (C SUBGOAL_THEN SUBST1_TAC);
      AP_TERM_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM (C INTRO_TAC [`i - (r-1)`]);
    DISCH_THEN (SUBST1_TAC o GSYM);
    AP_TERM_TAC;
    EXPAND_TAC "r'";
    BY(FIRST_X_ASSUM MP_TAC THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN ARITH_TAC);
  SUBCONJ_TAC;
    REWRITE_TAC[IN_NUMSEG] THEN REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `aff_gt` (C INTRO_TAC [`ITER (i+(r-1)) (rho_node1 FF) w`;`(i+(r-1))`]);
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC);
      EXPAND_TAC "r'";
      BY(ARITH_TAC);
    TYPIFY `(i+r-1) + r'+ 1 = i+ CARD V` ENOUGH_TO_SHOW_TAC;
      BY(DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]);
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC);
  DISCH_TAC;
  TYPIFY_GOAL_THEN `{uu 1, uu 2} SUBSET aff_gt {vec 0, uu (r' + 1)} {uu r'}` (unlist REWRITE_TAC);
    REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY;SUBSET];
    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_NUMSEG;arith `1 <= 1 /\ 1 <= 2`];
      BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC);
    BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC);
  COMMENT "cross";
  CONJ_TAC;
    REWRITE_TAC[IN_NUMSEG] THEN REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `&0 < (a cross b) dot c` (C INTRO_TAC [`PRE i`]);
    TYPIFY `PRE i < r' /\ PRE i + 1 = i /\ (PRE i+1)+1 = i+1` ENOUGH_TO_SHOW_TAC;
      BY(MESON_TAC[]);
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  COMMENT "azim_cycle";
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`uu i`;`PRE i`]);
    DISCH_THEN GMATCH_SIMP_TAC;
    CONJ_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN (REWRITE_TAC[IN_NUMSEG]) THEN MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`;arith `i <= r' /\ 1 <= i ==> PRE i < r'`]);
    FIRST_X_ASSUM (C INTRO_TAC [`1`;`i`]);
    BY(REWRITE_TAC[ITER_1;arith `1 + i = i + 1`]);
  CONJ_TAC;
    FIRST_X_ASSUM_ST `azim_cycle` MP_TAC;
    TYPIFY_GOAL_THEN `r' < CARD FF` (unlist REWRITE_TAC);
      GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_CARD_FF_V_EQ;
      TYPIFY `V` EXISTS_TAC;
      CONJ_TAC;
        BY(ASM_MESON_TAC[]);
      BY(FIRST_X_ASSUM_ST `r' < CARD V - 1` MP_TAC THEN ARITH_TAC);
    BY(FIRST_X_ASSUM_ST `w = uu(r'+1)` MP_TAC THEN MESON_TAC[]);
  COMMENT "0 < azim";
  TYPIFY `!i. rho_node1 FF (uu i) = uu(i+1)` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`1`;`i`]);
    BY(REWRITE_TAC[ITER_1;arith `1+i = i+1`]);
  TYPIFY `!i. 1 <= i ==> ivs_rho_node1 FF (uu i) = uu (i-1)` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    TYPED_ABBREV_TAC `a = uu(i-1)`;
    TYPIFY `i = 1 + (i-1)` (C SUBGOAL_THEN SUBST1_TAC);
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    FIRST_X_ASSUM (C INTRO_TAC [`1`;`i-1`]);
    REWRITE_TAC[ITER_1];
    DISCH_THEN (SUBST1_TAC o GSYM);
    EXPAND_TAC "a'";
    GMATCH_SIMP_TAC Local_lemmas.IVS_RHO_IDD;
    BY(ASM_MESON_TAC[]);
  TYPIFY_GOAL_THEN ` (!i. i IN 1..r' + 1 ==> &0 < azim (vec 0) (uu i) (uu (i + 1)) (uu (i - 1)))` (unlist REWRITE_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `&0 < azim a b c d` (C INTRO_TAC [`uu i`]);
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    TYPIFY `rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` ENOUGH_TO_SHOW_TAC;
      BY(DISCH_THEN (unlist REWRITE_TAC));
    BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]);
  COMMENT "azim <= pi";
  TYPIFY_GOAL_THEN `(!i. ?e2. i IN 1..r' + 1            ==> &0 < e2 /\               (!t. abs t < e2                    ==> azim (vec 0) (f (uu i) t) (f (uu (i + 1)) t)                        (f (uu (i - 1)) t) <=                        pi))` (unlist REWRITE_TAC);
    GEN_TAC;
    REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `azim a b c d <= pi` (C INTRO_TAC [`uu i`]);
    REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    (REPEAT WEAKER_STRIP_TAC);
    TYPIFY `e2` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
    TYPIFY `ivs_rho_node1 FF (uu i) = uu (i - 1)` ENOUGH_TO_SHOW_TAC;
      BY(DISCH_THEN (unlist REWRITE_TAC));
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]);
  COMMENT "pairwise";
  REWRITE_TAC[pairwise];
  TYPIFY `!i. uu (i) IN V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]);
  TYPIFY `(!i j. i IN 0..r'+1 /\ j IN 0..r'+1 /\ ~(i = j)==> ~(uu i = uu j)) /\ (!i j. i IN 1..r'+2 /\ j IN 1..r'+2 /\ ~(i=j) ==> ~(uu i = uu j))` ENOUGH_TO_SHOW_TAC;
    REPEAT (FIRST_X_ASSUM_ST `azim` kill);
    BY(ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN_ALT]);
  CONJ_TAC;
    REWRITE_TAC[IN_NUMSEG];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    (REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `ITER` kill));
    REWRITE_TAC[];
    FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM);
    BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `i <= r'+1 /\ 1 < r' /\ r' < CARD V - 1 ==> i < CARD V`]);
  TYPIFY `!i. 1 <= i ==> uu i = ITER (PRE i) (rho_node1 FF) (w')` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_REWRITE_TAC[];
    BY(MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`]);
  REWRITE_TAC[IN_NUMSEG];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[];
  FIRST_X_ASSUM_ST `ITER` (REPEAT o GMATCH_SIMP_TAC);
  TYPIFY `w' IN V` (C SUBGOAL_THEN MP_TAC);
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `PRE i < CARD V /\ PRE j < CARD V` (C SUBGOAL_THEN MP_TAC);
    BY(REPEAT (FIRST_X_ASSUM_ST `CARD` MP_TAC) THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[arith `1<= i /\ i <= r'+2 /\ 1 < r' /\ r' < CARD V - 1 ==> PRE i < CARD V`]);
  REPEAT (FIRST_X_ASSUM_ST `local_fan` MP_TAC);
  REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
  BY(MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `1 <= i /\ 1 <= j /\ PRE i = PRE j ==> (i = j)`])
  ]);;
  (* }}} *)

(*
let ZLZTHIC_concl = 
`!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) /\
     (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
	 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi)
     ==> (?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> convex_local_fan
                       (IMAGE (\v. f v t) V,
                        IMAGE (IMAGE (\v. f v t)) E,
                        IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
                       generic (IMAGE (\v. f v t) V)
                       (IMAGE (IMAGE (\v. f v t)) E)))`;;
*)

let ZLZTHIC = 
prove_by_refinement(
`!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) /\
     (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
	 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi)
     ==> (?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> convex_local_fan
                       (IMAGE (\v. f v t) V,
                        IMAGE (IMAGE (\v. f v t)) E,
                        IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
                       generic (IMAGE (\v. f v t) V)
                       (IMAGE (IMAGE (\v. f v t)) E)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC zlz_reduction;
  GEXISTL_TAC [`a`;`b`];
  ASM_REWRITE_TAC[];
  CONJ_TAC;
    MATCH_MP_TAC zlz_generic;
    GEXISTL_TAC [`a`;`b`;`E`];
    BY(ASM_REWRITE_TAC[]);
  CONJ_TAC;
    MATCH_MP_TAC zlz_wedge_skolem;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC zlz_wedge_boundary;
    GEXISTL_TAC [`a`;`b`];
    BY(ASM_REWRITE_TAC[]);
  MATCH_MP_TAC zlz_azim;
  GEXISTL_TAC [`a`;`b`;`V`];
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)


end;;