(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Introduction                                                      *)
(* Chapter: Local Fan                                                         *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2013-02-18                                                           *)
(* ========================================================================== *)

(*
Various odds and ends from the first part of the Local fan chapter
*)

module Localization = struct

  open Hales_tactic;;

parse_as_infix("has_orders",(12,"right"));;
parse_as_infix("cyclic_on",(13,"right"));;

let has_orders = new_definition ` (f: A -> A) has_orders k <=>
(! i. 0 < i /\ i < k ==> ~( ITER i f = I )) /\
ITER k f = I `;;

let order = new_definition ` order f x y = (@n. ITER n f x =y /\ (!i. 0< i /\ i< n ==> ~(ITER i f x= y)))`;;


let cyclic_on = new_definition` f cyclic_on (S:A -> bool) <=>
(! x. x IN S ==> S = {z | ?n. z = ITER n f x }) `;;

let dih2k = new_definition` dih2k (H: (A) hypermap) k <=> 
CARD (dart H) = 2 * k
/\ (! x. x IN (dart H) ==> let S = face H x in 
         dart H = S UNION (IMAGE (node_map H) S ))
/\ (face_map H ) has_orders k /\
(edge_map H ) has_orders 2 /\
(node_map H) has_orders 2 `;;

let EE = new_definition` EE v S = {w | {v,w} IN S }`;;

let ord_pairs = new_definition` ord_pairs E = { a,b | {a,b} IN E } `;;

let self_pairs = new_definition` self_pairs E V = { (v,v) | v IN V /\
 EE v E = {} } `;;

let darts_of_hyp = new_definition` darts_of_hyp E V = ord_pairs E UNION 
self_pairs E V `;;

let ee_of_hyp = new_definition` ee_of_hyp (x,V,E) ((a:real^3),(b:real^3)) = 
if (a,b) IN darts_of_hyp E V then (b,a) else (a,b)`;;

let nn_of_hyp = new_definition` nn_of_hyp (x,V,E) (v,u) =
if (v,u) IN darts_of_hyp E V then
(v, azim_cycle (EE v E) x v u) else (v,u)`;;

let ivs_azim_cycle = new_definition`ivs_azim_cycle W v0 v w =
if W = {} then w else 
(@x. x IN W /\ azim_cycle W v0 v x = w ) `;;

let ff_of_hyp = new_definition` ff_of_hyp (x,V,E) (v,u) =
if (v,u) IN darts_of_hyp E V then
(u, ivs_azim_cycle (EE u E) x u  v) else (v,u)`;;

let HYP = new_definition` HYP (x,V,E) = (darts_of_hyp E V,
ee_of_hyp (x,V,E), nn_of_hyp (x,V,E), ff_of_hyp (x,V,E)) `;;

let local_fan = new_definition ` local_fan (V,E,FF ) <=>
 let H = hypermap ( HYP (vec 0, (V: real^3 -> bool), E)) in
  FAN (vec 0, V, E) /\
  (?x. x IN ( dart H) /\ FF = face H x ) /\
dih2k H (CARD FF ) `;;

let rho_node1 = new_definition `!(v:real^3) FF. rho_node1 FF v = (@w. v,w IN FF)`;;

let azim_in_fan = new_definition` azim_in_fan (v:real^3,w:real^3) E = 
let d = (azim_cycle (EE v E) ( vec 0 ) v w) in
 if CARD ( EE v E ) > 1 then 
 azim (vec 0 ) v w d else &2 * pi `;;

let wedge_in_fan_gt = new_definition`wedge_in_fan_gt (v,w) E = 
  if CARD (EE v E) > 1 then
wedge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else if 
EE v E = {w} then { x | ~ ( x IN aff_ge {vec 0, v} {w} ) } else
{ x | ~ ( x IN aff {vec 0, v} )} `;;

let wedge_ge = new_definition `wedge_ge  v0 v1 w1 w2 = { z |
&0 <= azim v0 v1 w1 z /\ azim v0 v1 w1 z <= azim v0 v1 w1 w2 }`;;

let wedge_in_fan_ge = new_definition` wedge_in_fan_ge ((v:real^3),w) E = 
  if CARD (EE v E) > 1 then
wedge_ge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else { x:real^3 | T } `;;

let convex_local_fan = new_definition
  `convex_local_fan (V,E,FF) <=>
   local_fan (V,E,FF) /\
   (!x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E)`;;

let v_prime = new_definition `v_prime V FF = {v| v IN V /\
 (?w. (v,w) IN FF )} `;;

let e_prime = new_definition ` e_prime E FF = {{v,w} | {v,w} IN E /\ 
(v,w) IN FF } `;;

let generic = new_definition` generic V E <=>
(! v w u. {v,w} IN E /\ u IN V ==> aff_ge { vec 0 } {v,w} INTER 
aff_lt {vec 0} {u} = {} )`;;

let circular = new_definition ` circular V E <=> 
(? v w u. {v,w} IN E /\ u IN V /\ ~(aff_gt { vec 0 } {v,w} INTER 
aff_lt {vec 0} {u} = {}) )`;;

let lunar = new_definition
` lunar (v,w) V E <=> ~(circular V E) /\ {v,w} SUBSET V /\
~( v = w ) /\ collinear {vec 0, v, w } `;;

let rho_node1 = new_definition ` rho_node1 (FF:real^3 # real^3 -> bool) v = (@w. (v,w) IN FF)`;;

let ivs_rho_node1 = new_definition ` ivs_rho_node1 (FF:real^3 # real^3 -> bool) v = (@a. a,v IN FF )`;;

let interior_angle1 = new_definition
` interior_angle1 x FF v = azim x v (rho_node1 FF v) (@a. a,v IN FF)`;;

let sol_local = new_definition ` sol_local E f= &2 * pi+ sum f (\e. azim_in_fan e E- pi)`;;

let rho_fun = new_definition `rho_fun y = &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;

let tau_fun = new_definition `tau_fun V E f = sum (f) (\e. rho_fun(norm(FST e)) * (azim_in_fan e E)) - (pi + sol0) * &(CARD f -2)`;;

let deformation = new_definition 
` deformation ff V (a,b) <=> (&0) IN real_interval (a,b) /\
(! v r. v IN V /\ r IN real_interval (a,b) ==> (ff v) continuous atreal r) /\
(!v. v IN V ==> ff v (&0) = v )`;;

let localization = new_definition `localization (V, E) FF = (v_prime V FF, e_prime E FF) `;;

let a_ear0=new_definition`a_ear0 J (i,j)=( if i  MOD 3=j MOD 3 then &0 else
 (if {i  MOD 3,j MOD 3} IN J then sqrt(&8) else &2)) `;;

let b_ear0=new_definition`b_ear0 J (i,j)=( if i  MOD 3=j MOD 3 then &0 else
 (if {i  MOD 3,j MOD 3} IN J then cstab else &2* h0)) `;;

let JNVXCRC = new_definition
 `polar_fan(V,(E:(real^3->bool)->bool),FF) =
        let r = rho_node1 FF in
        let prime = \v. v cross (r v) in
        ({ prime v | v IN V},
         { {prime v,prime(r v)} | v IN V},
         { (prime v,prime(r v)) | v IN V})`;;




(* deprecated:
let v_slice = new_definition ` v_slice f (v,w) = 
{ ITER i f v | ! j. j < i ==> ~( ITER j f v = w ) }`;;


let e_slice = new_definition ` e_slice f (v,w) = 
{w,v} INSERT 
{ {ITER i f v, ITER (i + 1) f v} | ! j. j < i + 1 ==> ~( ITER j f v = w)} `;;


let f_slice = new_definition ` f_slice f (v,w) = 
(w,v) INSERT
{ (ITER i f v, ITER (i + 1) f v) | ! j. j < i + 1 ==> ~ (ITER j f v = w)} `;;
*)


let slicev = new_definition ` slicev E FF v w = {u| ?n. 0<= n /\ n<= order (rho_node1 FF) v w /\ u= ITER n (rho_node1 FF) v}`;;

let slicee = new_definition ` slicee E FF v w = {e| ?u. u IN (slicev E FF v w) DELETE w /\ e={u,rho_node1 FF u} } UNION {{w,v}}`;;

let slicef = new_definition ` slicef E FF v w = {f| ?u. u IN (slicev E FF v w) DELETE w /\ f=(u,rho_node1 FF u) } UNION {(w,v)}`;;

let FAN_EDGE_SUBSET_V = prove_by_refinement(
  `!V E e. FAN(vec 0, V, E) /\ e IN E ==> e SUBSET V`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Fan_defs.FAN;UNIONS_SUBSET];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let FAN_EDGE_EL_V = prove_by_refinement(
  `!V E u v. FAN(vec 0,V,E) /\ {u,v} IN E ==> v IN V`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `v IN {u,v}` (C SUBGOAL_THEN ASSUME_TAC);
    BY(SET_TAC[]);
  BY(ASM_MESON_TAC[FAN_EDGE_SUBSET_V;SUBSET])
  ]);;
  (* }}} *)

(* renamed from FAN_EE, EE_EQ_set_of_edge *)

let EE_elim = prove_by_refinement(
  `!V E (v:real^3). FAN(vec 0,V,E) ==> EE v E = set_of_edge v V E`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[EE;Fan_defs.set_of_edge];
  REWRITE_TAC[EXTENSION;IN_ELIM_THM];
  BY(ASM_MESON_TAC[FAN_EDGE_EL_V])
  ]);;
  (* }}} *)

(* renamed from darts_of_hyp_EQ_dart_of_fan *)

let darts_of_hyp_elim = prove_by_refinement(
  `!V E. FAN(vec 0,V,E) ==> darts_of_hyp E V = dart_of_fan (V,E)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[darts_of_hyp;Fan_defs.dart_of_fan;ord_pairs;self_pairs;SUBSET];
  REPEAT WEAKER_STRIP_TAC;
  ASM_SIMP_TAC[GSYM EE_elim];
  BY(SET_TAC[])
  ]);;
  (* }}} *)

let dart_of_fan_eq = prove_by_refinement(
 `!V E.
         dart_of_fan (V,E) =
         dart1_of_fan (V,E) UNION {v,v | v IN V /\ set_of_edge v V E = {}}`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Fan_defs.dart_of_fan;EXTENSION;IN_UNION;Fan_defs.dart1_of_fan];
  BY(SET_TAC[])
  ]);;
  (* }}} *)


(* renamed from ee_of_hyp_EQ_e_fan_pair_ext *)

let ee_of_hyp_elim = prove_by_refinement(
  `!V E (x:A).  FAN(vec 0,V,E)  ==> ee_of_hyp(x,V,E) = e_fan_pair_ext(V,E)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM];
  REWRITE_TAC[ee_of_hyp;Fan_defs.e_fan_pair_ext;Fan_defs.e_fan_pair];
  ASM_SIMP_TAC[darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ];
  REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  COND_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

let AZIM_CYCLE_EQ_SIGMA_FAN_ALT = prove_by_refinement(
  `!V E u v. FAN (vec 0,V,E) /\ u IN set_of_edge v V E
        ==> azim_cycle (set_of_edge v V E) (vec 0) v u = sigma_fan (vec 0) V E v u`,
  (* {{{ proof *)
  [
  BY(ASM_MESON_TAC[EE_elim;Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN])
  ]);;
  (* }}} *)

(* renamed from nn_of_hyp_EQ_n_fan_pair_ext : *)

let nn_of_hyp_elim = prove_by_refinement(
  `!V E.  FAN(vec 0,V,E)  ==> nn_of_hyp((vec 0),V,E) = n_fan_pair_ext(V,E)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM];
  REWRITE_TAC[nn_of_hyp;Fan_defs.n_fan_pair_ext;Fan_defs.n_fan_pair];
  ASM_SIMP_TAC[EE_elim;darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ];
  REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC;
    (ASM_REWRITE_TAC[PAIR_EQ]);
    GMATCH_SIMP_TAC AZIM_CYCLE_EQ_SIGMA_FAN_ALT;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[Fan_defs.dart1_of_fan;Fan_defs.set_of_edge];
    REWRITE_TAC[IN_ELIM_PAIR_THM];
    REWRITE_TAC[IN_ELIM_THM];
    BY(ASM_MESON_TAC[FAN_EDGE_EL_V]);
  ASM_REWRITE_TAC[];
  TYPIFY`~(p1 = p2)` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  FIRST_X_ASSUM (ASSUME_TAC o (REWRITE_RULE[]));
  ASM_REWRITE_TAC[];
  COND_CASES_TAC;
    ASM_REWRITE_TAC[PAIR_EQ];
    INTRO_TAC Wrgcvdr_cizmrrh.W_SUBSET_SINGLETON_IMP_IDE [`{}:real^3->bool`;`p2`];
    ANTS_TAC;
      BY(SET_TAC[]);
    BY(MESON_TAC[]);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

(* renamed from ivs_azim_cycle_EQ_inverse_sigma_fan *)

let ivs_azim_cycle_elim = prove_by_refinement(
  `!V E p1 p2. FAN(vec 0,V,E)   /\ {p1,p2} IN E  
  ==> ivs_azim_cycle (set_of_edge p1 V E) (vec 0) p1 p2 = inverse_sigma_fan (vec 0) V E p1 p2`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  ASM_SIMP_TAC[GSYM Fan_misc.INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN];
  ASM_SIMP_TAC[ (GSYM Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN)];
  BY(ASM_MESON_TAC[EE_elim])
  ]);;
  (* }}} *)

(* renamed from ff_of_hyp_EQ_f_fan_pair_ext: *)

let ff_of_hyp_elim = prove_by_refinement(
  `!V E.  FAN(vec 0,V,E)  ==> ff_of_hyp(vec 0,V,E) = f_fan_pair_ext(V,E)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM];
  REWRITE_TAC[ff_of_hyp;Fan_defs.f_fan_pair_ext;Fan_defs.f_fan_pair];
  ASM_SIMP_TAC[darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ];
  REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC;
    (ASM_REWRITE_TAC[PAIR_EQ]);
    ASM_SIMP_TAC[EE_elim];
    GMATCH_SIMP_TAC ivs_azim_cycle_elim;
    ASM_REWRITE_TAC[];
    RULE_ASSUM_TAC (REWRITE_RULE[Fan_defs.dart1_of_fan;IN_ELIM_PAIR_THM]);
    BY(ASM_MESON_TAC[Collect_geom.PER_SET2]);
  ASM_REWRITE_TAC[];
  COND_CASES_TAC THEN REWRITE_TAC[];
  ASM_REWRITE_TAC[PAIR_EQ];
  ASM_SIMP_TAC[EE_elim];
  BY(REWRITE_TAC[Wrgcvdr_cizmrrh.IVS_AZIM_EMPTY_IDE])
  ]);;
  (* }}} *)

let HYP_elim = prove_by_refinement(
  `!V E. FAN (vec 0, V, E) ==> HYP ((vec 0),V,E) = (dart_of_fan (V,E),
  e_fan_pair_ext(V,E),n_fan_pair_ext(V,E),f_fan_pair_ext(V,E))`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_SIMP_TAC[HYP;darts_of_hyp_elim;ee_of_hyp_elim;nn_of_hyp_elim;ff_of_hyp_elim])
  ]);;
  (* }}} *)

let hypermap_HYP_elim = prove_by_refinement(
  `!V E.  FAN(vec 0,V,E) ==> hypermap ( HYP (vec 0, (V: real^3 -> bool), E)) = hypermap_of_fan (V,E) `,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_SIMP_TAC[Fan_defs.HYPERMAP_OF_FAN_ALT;HYP_elim])
  ]);;
  (* }}} *)

let local_fan2 = prove_by_refinement(
  `!V E FF. local_fan (V,E,FF ) <=>
 let H = hypermap_of_fan (V,E) in
  FAN (vec 0, V, E) /\
  FF IN face_set H /\
  dih2k H (CARD FF ) `,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[local_fan;LET_DEF;LET_END_DEF];
  TYPIFY `FAN(vec 0,V,E)` ASM_CASES_TAC;
    ASM_SIMP_TAC[hypermap_HYP_elim];
    BY(ASM_MESON_TAC[Hypermap.lemma_in_face_set;Hypermap.lemma_face_representation]);
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let WRGCVDR_BIJ = prove_by_refinement(
  `!V E FF. local_fan (V,E,FF) 
        ==> BIJ FST FF V`,
  (* {{{ proof *)
  [
    BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.WRGCVDR;FUN_EQ_THM])
  ]);;
  (* }}} *)

let  WRGCVDR_ORBIT = prove_by_refinement(
  `!V E FF. local_fan (V,E,FF) ==>
      (!v. v IN V ==> orbit_map (rho_node1 FF) v = V) `,
  (* {{{ proof *)
  [
    BY(MESON_TAC[ Local_lemmas.LOCAL_FAN_ORBIT_MAP_V])
  ]);;
  (* }}} *)

let ALL_TO_THE_NONPARALLEL_PART_ALT = prove_by_refinement(
  `!a b V E phii. deformation phii V (a,b) /\ FAN (vec 0,V,E)
        ==> (?e. &0 < e /\
                 (!t. --e < t /\ t < e
                      ==> UNIONS (IMAGE (IMAGE (\v. phii v t)) E) SUBSET
                          IMAGE (\v. phii v t) V /\
                          graph (IMAGE (IMAGE (\v. phii v t)) E) /\
                          fan1
                          ((vec 0):real^3,
                           IMAGE (\v. phii (v:real^3) t) V,
                           IMAGE (IMAGE (\v. phii v t)) E) /\
                          fan2
                          ((vec 0):real^3,
                           IMAGE (\v. phii v t) V,
                           IMAGE (IMAGE (\v. phii v t)) E) /\
                          fan6
                          (vec 0,
                           IMAGE (\v. phii v t) V,
                           IMAGE (IMAGE (\v. phii v t)) E)))`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC Local_lemmas1.ALL_TO_THE_NONPARALLEL_PART;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

(* moved to deformation.hl
let XRECQNS = prove_by_refinement(
  `!a b V E f.
    deformation f V (a,b) /\ FAN (vec 0,V,E) ==>
     (?e. &0 < e /\ (!t. --e < t /\ t < e ==>
        FAN(vec 0,
	    IMAGE (\v. f (v:real^3) t) V,
                               IMAGE (IMAGE (\v. f v t)) E)))`,
  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  REWRITE_TAC[Fan.FAN];
  INTRO_TAC ALL_TO_THE_NONPARALLEL_PART_ALT [`a`;`b`;`V`;`E`;`f`];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  INTRO_TAC Deformation.FAN7_SMALL_DEFORMATION [`V`;`E`;`a`;`b`;`f`];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  TYPIFY `if (e < e') then e else e'` EXISTS_TAC;
  COND_CASES_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    BY(ASM_MESON_TAC[arith `&0 < e /\ e < e' /\ -- e < t /\ t < e ==> -- e' < t /\ t < e'`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_MESON_TAC[arith `&0 < e' /\ ~(e < e') /\ -- e' < t /\ t < e' ==> -- e < t /\ t < e`])
  ]);;
  (* }}} *)
*)

let COMPATIBLE_BW_TWO_LEMMAS2_ALT = prove_by_refinement(
  `!V E FF HS fv fw v w. (convex_local_fan (V,E,FF) /\
         v IN V /\
         w IN V /\
         ~(v = w) /\
         (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\
         HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
         fv = face HS (v,rho_node1 FF v)) /\
        fw = face HS (w,rho_node1 FF w)
        ==> (v_prime V fv = slicev E FF v w /\
             e_prime (E UNION {{v, w}}) fv = slicee E FF v w /\
             fv = slicef E FF v w) /\
            v_prime V fw = slicev E FF w v /\
            e_prime (E UNION {{w, v}}) fw = slicee E FF w v /\
            fw = slicef E FF w v`,
  (* {{{ proof *)
  [
  MESON_TAC[Nkezbfc_local.COMPATIBLE_BW_TWO_LEMMAS2]
  ]);;
  (* }}} *)

let EJRCFJD_ALT = prove_by_refinement(
  `!V E FF HS fv fw v w. convex_local_fan (V,E,FF) /\
        v IN V /\
        w IN V /\
        ~(v = w) /\
        (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\
        HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
        fv = face HS (v,rho_node1 FF v) /\
        fw = face HS (w,rho_node1 FF w)
        ==> convex_local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\
            convex_local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw) /\
            (!ff. sum {i | i < CARD V}
                  (\i. ff i *
                       interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v)) =
                  sum
                  {i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fv}
                  (\i. ff i *
                       interior_angle1 (vec 0) fv (ITER i (rho_node1 FF) v)) +
                  sum
                  {i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fw}
                  (\i. ff i *
                       interior_angle1 (vec 0) fw (ITER i (rho_node1 FF) v)))`,
  (* {{{ proof *)
  [
  MESON_TAC[Local_lemmas1.EJRCFJD]
  ]);;
  (* }}} *)

let WEDGE_VV = prove_by_refinement(
  `!a b c d. ~(b IN wedge a b c d) `,
  (* {{{ proof *)
  [
  REWRITE_TAC[wedge;IN_ELIM_THM];
  REPEAT GEN_TAC;
  TYPIFY `{a,b,b} = {a,b}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  BY(REWRITE_TAC[COLLINEAR_2])
  ]);;
  (* }}} *)

let ejr_distinct = prove_by_refinement(
  `!V E FF v w. convex_local_fan (V,E,FF) /\
    v IN V /\ 
  (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==>
    ~(w = v)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `aff_gt` MP_TAC;
  REWRITE_TAC[NOT_FORALL_THM];
  TYPIFY `(v,rho_node1 FF v)` EXISTS_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]);
  ASM_REWRITE_TAC[];
  TYPIFY `{v,v} = {v}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]);
  ASM_REWRITE_TAC[wedge_in_fan_gt];
  TYPIFY `v IN aff_gt {vec 0} {v}` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC AFF_GT_1_1;
    REWRITE_TAC[DISJOINT;IN_ELIM_THM];
    REWRITE_TAC[EXTENSION;IN_INTER;IN_SING;NOT_IN_EMPTY];
    CONJ_TAC;
      RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN]);
      RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN;LET_DEF;LET_END_DEF;Fan_defs.fan2]);
      BY(ASM_MESON_TAC[]);
    GEXISTL_TAC [`&0`;`&1`];
    REWRITE_TAC[arith `&0 < &1`;arith `&0 + &1 = &1`];
    BY(VECTOR_ARITH_TAC);
  REWRITE_TAC[SUBSET];
  BY(ASM_MESON_TAC[WEDGE_VV])
  ]);;
  (* }}} *)

(*
  TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]);
  FIRST_X_ASSUM_ST `wedge_in_fan_gt` MP_TAC;
*)

let WEDGE_EDGE_NOT_ADJ = prove_by_refinement(
  `!V E FF v .  local_fan (V,E,FF) /\
         v IN V ==>
           ~(aff_gt {vec 0} {v, rho_node1 FF v} SUBSET wedge_in_fan_gt (v,rho_node1 FF v) E) `,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]);
  FIRST_X_ASSUM_ST `wedge_in_fan_gt` MP_TAC;
  ASM_REWRITE_TAC[wedge_in_fan_gt];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Nkezbfc_local.AFF_GT_SUBSET_WEDGE_IMP_VERTEX [`(vec 0):real^3`;`v`;`rho_node1 FF v`;`rho_node1 FF v`;`azim_cycle (EE v E) (vec 0) v (rho_node1 FF v)`];
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC Local_lemmas1.LF_AZIM_CYCLE_EQ_IVS_ND;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS;Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]);
  BY(REWRITE_TAC[wedge;IN_ELIM_THM;AZIM_REFL;arith `~(&0 < &0)`])
  ]);;
  (* }}} *)

let PERIODIC_RHO_NODE1 = prove_by_refinement(
  `!V E FF v.  local_fan (V,E,FF) /\ v IN V ==> periodic (\i. ITER i (rho_node1 FF) v) (CARD V)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Oxl_def.periodic;GSYM ITER_ADD];
  REPEAT WEAKER_STRIP_TAC;
  AP_TERM_TAC;
  MATCH_MP_TAC Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let V_PRIME_SUBSET_V = prove_by_refinement(
  `!V f.  v_prime (V:real^3->bool) (f:real^3 # real^3 -> bool) SUBSET V`,
  (* {{{ proof *)
  [
  REWRITE_TAC[v_prime;SUBSET;IN_ELIM_THM];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let SLICEV_IMAGE = prove_by_refinement(
  `!V E FF v w i.
     convex_local_fan (V,E,FF) /\
     v IN V /\
     w IN V /\
     (!u u1.
          u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
     (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
     (i < CARD V) /\
     (w = ITER i (rho_node1 FF) v)
     ==>
       slicev E FF v w = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j < i+1 } `,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
  TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
  TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
  INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]);
  COMMENT "remove a many lines here";
  TYPIFY `!j. j < CARD V /\ ITER j (rho_node1 FF) v IN v_prime V fv <=> j < i+1` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM);
    ASM_REWRITE_TAC[IN_DIFF;IN_SING];
    BY(ASM_MESON_TAC[]);
  COMMENT "v_prime as image";
  TYPIFY `v_prime V fv = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j < i+1 }` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC Local_lemmas1.POINTS_IN_HAFL_CIRCLE;
    GEXISTL_TAC [`w`;`FF`;`v`];
    CONJ_TAC;
      GEXISTL_TAC [`E`;`HS`];
      ASM_REWRITE_TAC[IN_DIFF;IN_SING];
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE];
    X_GEN_TAC `u:real^3`;
    REWRITE_TAC[Geomdetail.EQ_EXPAND];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      TYPIFY `n` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      REWRITE_TAC[arith `n < i+1 <=> ~(i < n)`];
      BY(ASM_MESON_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `x` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `m < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
      BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC);
    TYPIFY `m = i` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA]);
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let LOCAL_FAN_ORBIT_MAP_EXPLICIT = prove
 (`!V E FF v w.
        local_fan(V,E,FF) /\ v IN V /\ w IN V
        ==> ?i. i < CARD V /\ w = ITER i (rho_node1 FF) v`,
  REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o
    MATCH_MP Local_lemmas.LOCAL_FAN_ORBIT_MAP_V) THEN
  REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER; Hypermap.orbit_map] THEN
  ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
  DISCH_THEN(MP_TAC o SPEC `w:real^3`) THEN ASM_REWRITE_TAC[GE; LE_0] THEN
  DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
  EXISTS_TAC `n MOD (CARD(V:real^3->bool))` THEN
  FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOCAL_FAN_FINITE_V) THEN
  FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN
  MP_TAC(ISPECL [`n:num`; `CARD(V:real^3->bool)`] DIVISION) THEN
  ABBREV_TAC `i = n MOD (CARD(V:real^3->bool))` THEN
  ABBREV_TAC `m = n DIV (CARD(V:real^3->bool))` THEN
  ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_THEN(K ALL_TAC) THEN
  SPEC_TAC(`m:num`,`p:num`) THEN
  INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
  ONCE_REWRITE_TAC[ARITH_RULE `(a + b) + c:num = (a + c) + b`] THEN
  ONCE_REWRITE_TAC[GSYM ITER_ADD] THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID) THEN
  ASM_SIMP_TAC[]);;

let SLICEW_IMAGE = prove_by_refinement(
  `!V E FF v w n.
     convex_local_fan (V,E,FF) /\
     v IN V /\
     w IN V /\
     (!u u1.
          u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
     (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
     (n < CARD V) /\
     (w = ITER n (rho_node1 FF) v)
     ==>
       slicev E FF w v = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j = 0 \/ (n <= j /\ j < CARD V) }`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
  TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
  TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
  INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]);
  TYPIFY `!j. j < CARD V /\ ITER j (rho_node1 FF) v IN v_prime V fw <=> (j =0) \/ (n <= j /\ j < CARD V)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM2);
    ASM_REWRITE_TAC[IN_DIFF;IN_SING];
    BY(ASM_MESON_TAC[]);
  COMMENT "v_prime as image";
  TYPIFY `v_prime V fw = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j = 0 \/ (n <= j /\ j < CARD V) }` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[EXTENSION;IN_IMAGE];
    X_GEN_TAC `u:real^3`;
    TYPIFY `u IN v_prime V fw` ASM_CASES_TAC;
      ASM_REWRITE_TAC[];
      INTRO_TAC V_PRIME_SUBSET_V [`V`;`fw`];
      REWRITE_TAC[SUBSET];
      DISCH_THEN (C INTRO_TAC [`u`]);
      DISCH_TAC;
      INTRO_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT [`V`;`E`;`FF`;`v`;`u`];
      ANTS_TAC;
        BY(ASM_MESON_TAC[]);
      REWRITE_TAC[IN_ELIM_THM];
      REPEAT WEAKER_STRIP_TAC;
      TYPIFY `i` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[]);
    ASM_REWRITE_TAC[];
    REWRITE_TAC[NOT_EXISTS_THM;IN_ELIM_THM];
    BY(ASM_MESON_TAC[]);
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

(* Might extract things like the exact card of slicev, and the fact that 3 < CARD V *)

let CARD_SLICEV_LT = prove_by_refinement(
  `!V E FF v w.
     convex_local_fan (V,E,FF) /\
     v IN V /\
     w IN V /\
     (!u u1.
          u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
     (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==>
      CARD (slicev E FF v w) < CARD V`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
  TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
  TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
  INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]);
  INTRO_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT [`V`;`E`;`FF`;`v`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `1 < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas1.DIFFERENCE_IMP_LT_CARDV;
    ASM_REWRITE_TAC[arith `n < 1 <=> n = 0`];
    BY(ASM_MESON_TAC[ITER]);
  TYPIFY `~(i = CARD V - 1)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    TYPIFY `w = ivs_rho_node1 FF v` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]);
    INTRO_TAC WEDGE_EDGE_NOT_ADJ [`V`;`E`;`FF`;`w`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    REWRITE_TAC[];
    RULE_ASSUM_TAC (ONCE_REWRITE_RULE[Collect_geom.PER_SET2]);
    TYPIFY `w,rho_node1 FF w IN FF` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]);
    TYPIFY `rho_node1 FF w = v` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]);
    BY(ASM_MESON_TAC[]);
  TYPIFY `!j. j < CARD V /\ ITER j (rho_node1 FF) v IN v_prime V fv <=> j < i+1` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM);
    ASM_REWRITE_TAC[IN_DIFF;IN_SING];
    BY(ASM_MESON_TAC[]);
  COMMENT "v_prime as image";
  TYPIFY `v_prime V fv = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j < i+1 }` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC Local_lemmas1.POINTS_IN_HAFL_CIRCLE;
    GEXISTL_TAC [`w`;`FF`;`v`];
    CONJ_TAC;
      GEXISTL_TAC [`E`;`HS`];
      ASM_REWRITE_TAC[IN_DIFF;IN_SING];
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE];
    X_GEN_TAC `u:real^3`;
    REWRITE_TAC[Geomdetail.EQ_EXPAND];
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      TYPIFY `n` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      REWRITE_TAC[arith `n < i+1 <=> ~(i < n)`];
      BY(ASM_MESON_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `x` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `m < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
      BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    TYPIFY `m = i` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA]);
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  COMMENT "now use IMAGE CARD";
  FIRST_X_ASSUM (SUBST1_TAC);
  MATCH_MP_TAC LET_TRANS;
  TYPIFY `CARD {j | j < i + 1}` EXISTS_TAC;
  CONJ_TAC;
    MATCH_MP_TAC CARD_IMAGE_LE;
    BY(REWRITE_TAC[FINITE_NUMSEG_LT]);
  REWRITE_TAC[CARD_NUMSEG_LT];
  BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
  ]);;
  (* }}} *)

let SLICEW_BIJ = prove_by_refinement(
  `!V E FF v w n.
         convex_local_fan (V,E,FF) /\
         v IN V /\
         w IN V /\
         (!u u1.
              u IN {v, w} /\ u1 IN V /\ ~(u = u1)
              ==> ~collinear {vec 0, u, u1}) /\
         (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
         n < CARD V /\
         w = ITER n (rho_node1 FF) v
         ==> 
             BIJ (\j. ITER j (rho_node1 FF) v)
             {j | j = 0 \/ n <= j /\ j < CARD V} (slicev E FF w v)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[BIJ];
  REPEAT WEAKER_STRIP_TAC;
  SUBCONJ2_TAC;
    INTRO_TAC SLICEW_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    DISCH_THEN SUBST1_TAC;
    BY(REWRITE_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]);
  REWRITE_TAC[SURJ;INJ];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY `FINITE V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]);
  TYPIFY `0 < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_SIMP_TAC[ arith `0 < x <=> ~(x = 0)`;CARD_EQ_0;EXTENSION;NOT_IN_EMPTY;NOT_FORALL_THM];
    BY(ASM_MESON_TAC[]);
  INTRO_TAC Local_lemmas1.LT_CARD_MONO_LOFA [];
  ASM_REWRITE_TAC[];
  DISCH_THEN MATCH_MP_TAC;
  BY(ASM_MESON_TAC[])
 ]);;
  (* }}} *)

let SLICEV_BIJ = prove_by_refinement(
  `!V E FF v w n.
         convex_local_fan (V,E,FF) /\
         v IN V /\
         w IN V /\
         (!u u1.
              u IN {v, w} /\ u1 IN V /\ ~(u = u1)
              ==> ~collinear {vec 0, u, u1}) /\
         (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
         n < CARD V /\
         w = ITER n (rho_node1 FF) v
         ==> 
             BIJ (\j. ITER j (rho_node1 FF) v)
             {j | j < n + 1} (slicev E FF v w)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[BIJ];
  REPEAT WEAKER_STRIP_TAC;
  SUBCONJ2_TAC;
    INTRO_TAC SLICEV_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    DISCH_THEN SUBST1_TAC;
    BY(REWRITE_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]);
  REWRITE_TAC[SURJ;INJ];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY `FINITE V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]);
  TYPIFY `0 < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_SIMP_TAC[ arith `0 < x <=> ~(x = 0)`;CARD_EQ_0;EXTENSION;NOT_IN_EMPTY;NOT_FORALL_THM];
    BY(ASM_MESON_TAC[]);
  INTRO_TAC Local_lemmas1.LT_CARD_MONO_LOFA [];
  ASM_REWRITE_TAC[];
  DISCH_THEN MATCH_MP_TAC;
  BY(ASM_MESON_TAC[arith `x < n+1 /\ n < c==> x < c`])
 ]);;
  (* }}} *)

let CARD_SLICEV = prove_by_refinement(
  `!V E FF v w .
         convex_local_fan (V,E,FF) /\
         v IN V /\
         w IN V /\
         (!u u1.
              u IN {v, w} /\ u1 IN V /\ ~(u = u1)
              ==> ~collinear {vec 0, u, u1}) /\
         (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) 
         ==> CARD (slicev E FF v w) + CARD(slicev E FF w v) = CARD V + 2`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?n. n < CARD V /\ w = ITER n (rho_node1 FF) v` (C SUBGOAL_THEN MP_TAC);
    COMMENT "insert";
    TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
    MATCH_MP_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT;
    TYPIFY `E` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC SLICEV_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  INTRO_TAC SLICEW_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPED_ABBREV_TAC  `f = (\j. ITER j (rho_node1 FF) v)` ;
  TYPIFY `CARD {j | j < n + 1} =  CARD (slicev E FF v (ITER n (rho_node1 FF) v))` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC Misc_defs_and_lemmas.BIJ_CARD;
    ASM_REWRITE_TAC[FINITE_NUMSEG_LT];
    BY(ASM_MESON_TAC[]);
  DISCH_THEN (SUBST1_TAC o GSYM);
  TYPIFY `CARD {j | j =0 \/ ( n <= j /\ j < CARD V)} =  CARD (slicev E FF w v)` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC Misc_defs_and_lemmas.BIJ_CARD;
    TYPIFY `f` EXISTS_TAC;
    CONJ2_TAC;
      BY(ASM_REWRITE_TAC[]);
    MATCH_MP_TAC FINITE_SUBSET;
    TYPIFY `{0} UNION {j | j < CARD V}` EXISTS_TAC;
    CONJ_TAC;
      MATCH_MP_TAC FINITE_UNION_IMP;
      BY(ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY;FINITE_NUMSEG_LT]);
    BY(SET_TAC[]);
  ASM_REWRITE_TAC[];
  DISCH_THEN (SUBST1_TAC o GSYM);
  REWRITE_TAC[CARD_NUMSEG_LT];
  TYPIFY `{j | j  = 0 \/ n <= j /\ j < CARD V } = {0} UNION {j | n <= j /\ j < CARD V}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  INTRO_TAC Geomdetail.CARD_EQUATION [`{0}`;`{j | n <= j /\ j < CARD V}`];
  ANTS_TAC;
    REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
    MATCH_MP_TAC FINITE_SUBSET;
    TYPIFY ` {j | j < CARD V}` EXISTS_TAC;
    ASM_REWRITE_TAC[FINITE_NUMSEG_LT];
    BY(SET_TAC[]);
  TYPIFY `({0} INTER {j | n <= j /\ j < CARD V}) = {}` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;IN_SING;IN_ELIM_THM];
    TYPIFY `~(n=0)` ENOUGH_TO_SHOW_TAC;
      BY(ARITH_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM_ST `w = ITER n r v` MP_TAC;
    ASM_REWRITE_TAC[ITER];
    INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
    DISCH_THEN MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  REWRITE_TAC[CARD_CLAUSES;arith `x + 0 = x`];
  DISCH_THEN SUBST1_TAC;
  REWRITE_TAC[Geomdetail.CARD_SING];
  TYPIFY `{j | n <= j /\  j < CARD V} = (n.. (CARD V - 1))` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[EXTENSION;IN_NUMSEG;IN_ELIM_THM];
    BY(REPEAT (FIRST_X_ASSUM_ST `n < CARD V` MP_TAC) THEN ARITH_TAC);
  REWRITE_TAC[CARD_NUMSEG];
  BY(REPEAT (FIRST_X_ASSUM_ST `n < CARD V` MP_TAC) THEN ARITH_TAC)
  ]);;
  (* }}} *)

let HAFL_CIRCLE_FORM_LOCAL_FAN_ALT = prove_by_refinement(
  `!V E FF v w HS fv. (local_fan (V,E,FF) /\
      v IN V /\
      w IN V /\
      ~(v = w) /\
      (!z t. z IN {v, w} /\ t IN V DIFF {z} ==> ~collinear {vec 0, z, t}) /\
      (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E)) /\
     HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
     fv = face HS (v,rho_node1 FF v)
     ==> local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GEN_ALL Local_lemmas1.HAFL_CIRCLE_FORM_LOCAL_FAN) [];
  DISCH_THEN MATCH_MP_TAC;
  GEXISTL_TAC [`HS`;`FF`];
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT = prove_by_refinement(
  `!V E FF v w HS fv. (local_fan (V,E,FF) /\
      v IN V /\
      w IN V /\
      ~(v = w) /\
      (!z t. z IN {v, w} /\ t IN V DIFF {z} ==> ~collinear {vec 0, z, t}) /\
      (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E)) /\
     HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
     fv = face HS (v,rho_node1 FF v) /\
     fw = face HS (w,rho_node1 FF w)
     ==> local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\
         local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GEN_ALL Local_lemmas1.HAFL_CIRCLE_FORM_LOCAL_FAN2) [];
  DISCH_THEN MATCH_MP_TAC;
  GEXISTL_TAC [`HS`;`FF`];
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let CARD_SLICEF = prove_by_refinement(
  `!V E FF v w .
         convex_local_fan (V,E,FF) /\
         v IN V /\
         w IN V /\
         (!u u1.
              u IN {v, w} /\ u1 IN V /\ ~(u = u1)
              ==> ~collinear {vec 0, u, u1}) /\
         (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) 
         ==> CARD (slicef E FF v w) + CARD(slicef E FF w v) = CARD FF + 2`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
  TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
  TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
  INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY` local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\          local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw)` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT;
    GEXISTL_TAC [`FF`;`HS`];
    ASM_REWRITE_TAC[IN_DIFF;IN_SING];
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `FINITE FF /\ FINITE fv /\ FINITE fw` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF]);
  REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP Local_lemmas.LOFA_IMP_BIJ_FF_V)));
  INTRO_TAC CARD_SLICEV [`V`;`E`;`FF`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM MP_TAC;
  BY(MESON_TAC[Local_lemmas.BIJ_IMP_CARD_EQ])
  ]);;
  (* }}} *)

let aff_ge_INTER_aff_lt = prove_by_refinement(
  `! (y:real^A). ~(y = vec 0) ==> aff_ge {vec 0} {y} INTER aff_lt {vec 0} {y} = {}`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  ASM_SIMP_TAC[AFF_GE_1_1_0];
  GMATCH_SIMP_TAC AFF_LT_1_1;
  REWRITE_TAC[DISJOINT;IN_SING;EXTENSION;IN_INTER;IN_ELIM_THM;NOT_IN_EMPTY];
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[VECTOR_MUL_RZERO];
  REWRITE_TAC[varith `a % y = vec 0 + t2 % (y:real^A) <=> (a - t2) % y = vec 0`];
  ASM_REWRITE_TAC[VECTOR_MUL_EQ_0];
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let ejr_generic = prove_by_refinement(
  `!V E FF v w.
     convex_local_fan (V,E,FF) /\
     v IN V /\
     w IN V /\
     (!u u1.
          u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
     (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
    generic V E
  ==> generic (slicev E FF v w) (slicee E FF v w)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[generic];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
  TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
  TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
  INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY `e_prime (E UNION {{v,w}}) fv SUBSET (E UNION {{v,w}})` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.E_PRIME_SUBSET_E]);
  TYPIFY `{v',w'} IN E \/ {v',w'} = {v,w}` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `x IN slicee E FF v w` MP_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[SUBSET;IN_UNION;IN_SING];
    BY(MESON_TAC[]);
  FIRST_X_ASSUM (DISJ_CASES_TAC);
    FIRST_X_ASSUM_ST `generic` MP_TAC;
    REWRITE_TAC[generic];
    DISCH_THEN MATCH_MP_TAC;
    BY(ASM_MESON_TAC[V_PRIME_SUBSET_V;SUBSET]);
  FIRST_X_ASSUM (fun t -> REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[t]) THEN REPEAT WEAKER_STRIP_TAC;
  GMATCH_SIMP_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge;
  CONJ_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]);
  REWRITE_TAC[GSYM SUBSET_EMPTY];
  MATCH_MP_TAC SUBSET_TRANS;
  TYPIFY `(aff_gt {vec 0} {v,w} INTER aff_lt {vec 0} {u}) UNION (aff_ge {vec 0} {v} INTER aff_lt {vec 0} {u}) UNION (aff_ge {vec 0} {w} INTER aff_lt {vec 0} {u})` EXISTS_TAC;
  CONJ_TAC;
    BY(SET_TAC[]);
  REWRITE_TAC[UNION_SUBSET;SUBSET_EMPTY];
  TYPIFY `u IN V` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[V_PRIME_SUBSET_V;SUBSET]);
  TYPIFY `~(v = vec 0) /\ ~(w = vec 0) /\ ~(u = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
    RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN;Fan_defs.fan2;LET_DEF;LET_END_DEF]);
    BY(ASM_MESON_TAC[]);
  CONJ2_TAC;
    CONJ_TAC;
      PROOF_BY_CONTR_TAC;
      TYPIFY `collinear {vec 0,u,v}` (C SUBGOAL_THEN ASSUME_TAC);
        BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL]);
      TYPIFY `u = v` ASM_CASES_TAC;
        BY(ASM_MESON_TAC[aff_ge_INTER_aff_lt]);
      BY(ASM_MESON_TAC[Collect_geom.PER_SET3;IN_INSERT]);
    PROOF_BY_CONTR_TAC;
    TYPIFY `collinear {vec 0,u,w}` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL]);
    TYPIFY `u = w` ASM_CASES_TAC;
      BY(ASM_MESON_TAC[aff_ge_INTER_aff_lt]);
    BY(ASM_MESON_TAC[Collect_geom.PER_SET3;IN_INSERT]);
  TYPIFY `aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt (u,rho_node1 FF u) E /\ aff_lt {vec 0} {u} INTER wedge_in_fan_gt (u,rho_node1 FF u) E = {}` ENOUGH_TO_SHOW_TAC;
    BY(SET_TAC[]);
  CONJ_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]);
  REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER];
  GEN_TAC;
  GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_LOFA_DETER2;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[TAUT `~(a /\ b) <=> ( a ==> ~b)`];
  ASM_SIMP_TAC[Nkezbfc_local.AFF_LT_1_1;IN_ELIM_THM;wedge];
  REWRITE_TAC[VECTOR_MUL_RZERO;VECTOR_ADD_LID];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM_ST `collinear` MP_TAC;
  ASM_REWRITE_TAC[];
  ASM_SIMP_TAC[Local_lemmas.COLLINEAR_ONCE_VEC_0];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let LOFA_IMP_LT_CARD_SET_V_ALT = prove_by_refinement(
  `!V E FF v. local_fan (V,E,FF) /\ v IN V
         ==> {ITER n (rho_node1 FF) v | n < CARD V} = V`,
  (* {{{ proof *)
  [
    BY(MESON_TAC[Local_lemmas.LOFA_IMP_LT_CARD_SET_V])
  ]);;
  (* }}} *)

let ejr_sum = prove_by_refinement(
  `!V E FF HS v w f fv fw.
     convex_local_fan (V,E,FF) /\
     v IN V /\
     w IN V /\
     hypermap (HYP (vec 0,V,E UNION {{v, w}})) = HS /\
     face HS (v,rho_node1 FF v) = fv /\ 
     face HS (w,rho_node1 FF w) = fw /\ 
      (!u u1.
          u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
     (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E)  // /\
     ==> sum FF (\e. f (FST e) * azim_in_fan e E) =
         sum fv
         (\e. f (FST e) * azim_in_fan e (e_prime (E UNION {{v, w}}) fv)) +
         sum fw
         (\e. f (FST e) * azim_in_fan e (e_prime (E UNION {{w, v}}) fw))`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[generic];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY `?n. n < CARD V /\ w = ITER n (rho_node1 FF) v` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT;
    TYPIFY `E` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`(\i. f (ITER i (rho_node1 FF) v))`]);
  REWRITE_TAC[];
  COMMENT "replace first index set";
  TYPIFY `{i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fv } = {i | i < n + 1}` (C SUBGOAL_THEN SUBST1_TAC);
    INTRO_TAC SLICEV_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`];
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    REWRITE_TAC[IN_IMAGE;IN_ELIM_THM];
    REWRITE_TAC[EXTENSION;IN_ELIM_THM];
    X_GEN_TAC `i:num`;
    REWRITE_TAC[Geomdetail.EQ_EXPAND];
    CONJ2_TAC;
      REPEAT WEAKER_STRIP_TAC;
      SUBCONJ_TAC;
        BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC);
      DISCH_TAC;
      TYPIFY `i` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `i = x'` ENOUGH_TO_SHOW_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC);
    BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA;arith `x' < n+1 /\ n < c ==> x' < c`]);
  COMMENT "n not 0";
  TYPIFY `~(n=0)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM_ST `w = ITER n r v` MP_TAC;
    BY(ASM_REWRITE_TAC[ITER]);
  COMMENT "replace second index set";
  TYPIFY `{i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fw } = {i | i = 0 \/ n <= i /\ i < CARD V}` (C SUBGOAL_THEN SUBST1_TAC);
    INTRO_TAC SLICEW_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`];
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    REWRITE_TAC[IN_IMAGE;IN_ELIM_THM];
    REWRITE_TAC[EXTENSION;IN_ELIM_THM];
    X_GEN_TAC `i:num`;
    REWRITE_TAC[Geomdetail.EQ_EXPAND];
    CONJ2_TAC;
      REPEAT WEAKER_STRIP_TAC;
      SUBCONJ_TAC;
        BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
      DISCH_TAC;
      TYPIFY `i` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `i = x'` ENOUGH_TO_SHOW_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC);
    TYPIFY `x' < CARD V` (C SUBGOAL_THEN MP_TAC);
      BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA]);
  MATCH_MP_TAC (arith `(a = a' /\ b = b' /\ c = c') ==> (a = b + c ==> a' = b' + c')`);
  COMMENT "match summands";
  TYPIFY `!fu. ((\u. f u * interior_angle1 (vec 0) fu u) o (\i. ITER i (rho_node1 FF) v)) = (\i. f (ITER i (rho_node1 FF) v) *           interior_angle1 (vec 0) fu (ITER i (rho_node1 FF) v))` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_THM]);
  COMMENT "first sum";
  CONJ_TAC;
    TYPIFY `BIJ (\i. (ITER i (rho_node1 FF) v)) {i | i < CARD V} V` (C SUBGOAL_THEN ASSUME_TAC);
      REWRITE_TAC[BIJ];
      SUBCONJ2_TAC;
        TYPIFY `IMAGE (\i.  (ITER i (rho_node1 FF) v)) {i | i < CARD V} = V` ENOUGH_TO_SHOW_TAC;
          BY(MESON_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]);
        INTRO_TAC LOFA_IMP_LT_CARD_SET_V_ALT [`V`;`E`;`FF`;`v`];
        ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE];
        BY(MESON_TAC[]);
      REWRITE_TAC[SURJ;INJ];
      DISCH_TAC;
      ASM_REWRITE_TAC[];
      ASM_REWRITE_TAC[IN_ELIM_THM];
      BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA]);
    FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
    DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) FF u`]);
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    TYPIFY `BIJ FST FF V` (C SUBGOAL_THEN ASSUME_TAC);
      MATCH_MP_TAC WRGCVDR_BIJ;
      BY(ASM_MESON_TAC[]);
    FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
    DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) FF u`]);
    DISCH_THEN (SUBST1_TAC o GSYM);
    MATCH_MP_TAC SUM_EQ;
    REWRITE_TAC[o_THM];
    GEN_TAC;
    DISCH_TAC;
    TYPIFY `FST x IN V` ENOUGH_TO_SHOW_TAC;
      DISCH_TAC;
      AP_TERM_TAC;
      BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2]);
  COMMENT "prep for slice cases";
  TYPIFY `local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\ local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT;
    GEXISTL_TAC [`FF`;`HS`];
    ASM_REWRITE_TAC[IN_DIFF;IN_SING];
    BY(ASM_MESON_TAC[]);
  COMMENT "second sum";
  CONJ_TAC;
    INTRO_TAC SLICEV_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    DISCH_TAC;
    FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
    DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) fv u`]);
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    TYPIFY `BIJ FST fv (v_prime V fv)` (C SUBGOAL_THEN ASSUME_TAC);
      MATCH_MP_TAC WRGCVDR_BIJ;
      BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
    FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
    DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) fv u`]);
    DISCH_THEN (SUBST1_TAC o GSYM);
    MATCH_MP_TAC SUM_EQ;
    REWRITE_TAC[o_THM];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `FST x IN v_prime V fv` ENOUGH_TO_SHOW_TAC;
      DISCH_TAC;
      AP_TERM_TAC;
      BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]);
    BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2]);
  COMMENT "last case";
  INTRO_TAC SLICEW_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
  DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) fw u`]);
  ASM_REWRITE_TAC[];
  DISCH_THEN SUBST1_TAC;
  TYPIFY `BIJ FST fw (v_prime V fw)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC WRGCVDR_BIJ;
    BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
  FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
  DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) fw u`]);
  DISCH_THEN (SUBST1_TAC o GSYM);
  MATCH_MP_TAC SUM_EQ;
  REWRITE_TAC[o_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `FST x IN v_prime V fw` ENOUGH_TO_SHOW_TAC;
    DISCH_TAC;
    AP_TERM_TAC;
    BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]);
  BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2])
  ]);;
  (* }}} *)

let EJRCFJD_ALT2 = prove_by_refinement(
 `!V E FF v w.
     convex_local_fan (V,E,FF) /\
     v IN V /\
     w IN V /\
     (!u u1.
          u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
     (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E)
     ==> convex_local_fan (slicev E FF v w,slicee E FF v w,slicef E FF v w) /\
         convex_local_fan (slicev E FF w v,slicee E FF w v,slicef E FF w v) /\
         tau_fun V E FF >=
         tau_fun (slicev E FF v w) (slicee E FF v w) (slicef E FF v w) +
         tau_fun (slicev E FF w v) (slicee E FF w v) (slicef E FF w v) /\
         sol_local E FF =
         sol_local (slicee E FF v w) (slicef E FF v w) +
         sol_local (slicee E FF w v) (slicef E FF w v) /\
         CARD (slicev E FF v w) < CARD V /\
         CARD (slicev E FF w v) < CARD V /\
         (generic V E
          ==> generic (slicev E FF v w) (slicee E FF v w) /\
              generic (slicev E FF w v) (slicee E FF w v))`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
  TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
  TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
  INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `CARD (v_prime V fv) < CARD V /\ CARD (v_prime V fw) < CARD V` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `v_prime` (SUBST1_TAC o GSYM));
    CONJ_TAC;
      MATCH_MP_TAC CARD_SLICEV_LT;
      BY(ASM_REWRITE_TAC[]);
    MATCH_MP_TAC CARD_SLICEV_LT;
    ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[Collect_geom.PER_SET3]);
  TYPIFY `(generic V E  ==> generic (v_prime V fv) (e_prime (E UNION {{v, w}}) fv) /\      generic (v_prime V fw) (e_prime (E UNION {{w, v}}) fw))` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    DISCH_TAC;
    CONJ_TAC;
      INTRO_TAC ejr_generic [`V`;`E`;`FF`;`v`;`w`];
      ANTS_TAC;
        BY(ASM_REWRITE_TAC[]);
      BY(ASM_MESON_TAC[]);
    INTRO_TAC ejr_generic [`V`;`E`;`FF`;`w`;`v`];
    ANTS_TAC;
      ASM_REWRITE_TAC[];
      ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
      ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[Collect_geom.PER_SET3]);
    BY(ASM_MESON_TAC[]);
  COMMENT "now tau and sol";
  REWRITE_TAC[sol_local;tau_fun];
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
  TYPIFY` local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\          local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw)` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT;
    GEXISTL_TAC [`FF`;`HS`];
    ASM_REWRITE_TAC[IN_DIFF;IN_SING];
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "insert";
  TYPIFY ` CARD FF + 2 = CARD fv + CARD fw` (C SUBGOAL_THEN ASSUME_TAC);
    COMMENT "cut insert to here";
    INTRO_TAC CARD_SLICEF [`V`;`E`;`FF`;`v`;`w`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    BY(REWRITE_TAC[]);
  COMMENT "tau sum";
  INTRO_TAC ejr_sum [`V`;` E`;` FF`;` HS`;` v`;` w`;`rho_fun o (norm: (real^3-> real))`;` fv`;` fw`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REWRITE_TAC[o_THM];
  DISCH_THEN SUBST1_TAC;
  CONJ_TAC;
    MATCH_MP_TAC (arith `c1 = c2 + c3 ==> ((a + b) - c1 >= a - c2 + b - c3)`);
    REWRITE_TAC[arith `a * b + a * c = a * (b + c)`];
    AP_TERM_TAC;
    REWRITE_TAC[REAL_OF_NUM_ADD];
    REWRITE_TAC[REAL_OF_NUM_EQ];
    TYPIFY `(2 <= CARD FF /\ 2 <= CARD fv /\ 2 <= CARD fw) /\ CARD FF + 2 = CARD fv + CARD fw` ENOUGH_TO_SHOW_TAC;
      BY(ARITH_TAC);
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_CARD_FF_V_EQ;
    TYPIFY`V` EXISTS_TAC;
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    CONJ_TAC;
      MATCH_MP_TAC Hypermap.CARD_ATLEAST_2;
      GEXISTL_TAC [`v`;`w`];
      ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]);
    REPEAT (GMATCH_SIMP_TAC (arith `2 < x ==> 2 <= x`));
    REPEAT (GMATCH_SIMP_TAC (Local_lemmas1.LOFA_HYP_UNION_CARD_GT2));
    REWRITE_TAC[IN_DIFF;IN_SING];
    CONJ_TAC;
      GEXISTL_TAC [`V`;`E`;`w`;`HS`;`FF`;`v`];
      BY(ASM_MESON_TAC[]);
    GEXISTL_TAC [`V`;`E`;`v`;`HS`;`FF`;`w`];
    ASM_REWRITE_TAC[];
    ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[Collect_geom.PER_SET3]);
  COMMENT "final sum";
  INTRO_TAC ejr_sum [`V`;` E`;` FF`;` HS`;` v`;` w`;`\ (v:real^3). &1`;` fv`;` fw`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  REWRITE_TAC[o_THM;arith `&1 * x = x`];
  TYPIFY `FINITE fv /\ FINITE fw /\ FINITE FF` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF]);
  ASM_SIMP_TAC[SUM_SUB];
  ASM_SIMP_TAC[SUM_CONST];
  DISCH_THEN kill;
  MATCH_MP_TAC (arith `cf + t2 = cv + c2 ==>t2 + (tv + tw) - cf = (t2 + tv - cv) + (t2 + tw - c2)`);
  MATCH_MP_TAC (arith `cf + &2 = cv + cw ==> cf * pi + &2 * pi = cv * pi + cw * pi`);
  REWRITE_TAC[REAL_OF_NUM_ADD];
  REWRITE_TAC[REAL_OF_NUM_EQ];
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let NKEZBFC = prove_by_refinement(
  `!V E FF. convex_local_fan(V,E,FF) /\ generic V E
  ==> &0 <= sol_local E FF`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MP_TAC Nkezbfc_local.NKEZBFC_PREP;
  ANTS_TAC;
    BY(REWRITE_TAC[EJRCFJD_ALT2 ]);
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let azim_dart_azim_in_fan = prove_by_refinement(
  `!V E x. FAN((vec 0),V,E) /\ ({FST x,SND x} IN E)
    ==> azim_dart (V,E) x = azim_in_fan x E`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FORALL_PAIR_THM;FST;SND];
  REWRITE_TAC[Fan_defs.azim_dart;(* L *)azim_in_fan;Fan_defs.azim_fan];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[LET_DEF;LET_END_DEF];
  TYPIFY `~(p1 = p2)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    RULE_ASSUM_TAC (REWRITE_RULE[Fan.FAN;Fan.graph]);
    REPEAT (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`{p1,p2}`]);
    REWRITE_TAC[Local_lemmas1.SET2_HAS_SIZE2];
    BY(ASM_MESON_TAC[IN]);
  ASM_SIMP_TAC[GSYM (* L *)EE_elim];
  COND_CASES_TAC THEN ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN;
  TYPIFY `V` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  ASM_SIMP_TAC[GSYM (* L *)EE_elim];
  BY(ASM_REWRITE_TAC[(* L *)EE;IN_ELIM_THM])
  ]);;
  (* }}} *)

let rho_fun = new_definition `rho_fun y =  &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;

let rho_rho_fun = prove_by_refinement(
  `!y. rho_fun y = rho y`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.rho;rho_fun;Sphere.const1;Sphere.ly;Sphere.interp];
  REWRITE_TAC[GSYM Nonlinear_lemma.sol0_EQ_sol_y;Sphere.h0];
  REWRITE_TAC[arith `a + b = a + c <=> c = b`];
  GEN_TAC;
  MATCH_MP_TAC (arith `(sol0/pi)*(&1 - a) = (sol0/pi)*(c*e) ==> sol0/pi - sol0/pi * a = c * inv pi * sol0 * e`);
  AP_TERM_TAC;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let h_dart = new_definition `h_dart (x:real^3#B) = norm (FST x)  / &2`;;

let tauVEF = new_definition `tauVEF (V,E,f) = 
  sum f ( \ x. azim_dart (V,E) x * (&1 + (sol0/pi) * (&1 - lmfun (h_dart x))))   + (pi + sol0)*(&2 - &(CARD(f)))`;;

let tau_fun = new_definition `tau_fun V E f =  sum (f) (\e. rho_fun(norm(FST e)) * (azim_in_fan e E)) - (pi + sol0) * &(CARD f -2)`;;

let ly_EQ_lmfun = prove(`!x:real^3#real^3. norm (FST x) <= &2 * h0 ==> lmfun (h_dart x) = ly (norm (FST x))`,
   REWRITE_TAC[Pack_defs.lmfun; Sphere.ly; Sphere.interp; h_dart; Pack_defs.h0] THEN
     REAL_ARITH_TAC);;

let tauVEF_tau_fun = prove_by_refinement(
  `!V E f. FAN ((vec 0),V,E) /\ 
    2 <= CARD f /\ 
    (!x. x IN f ==> norm(FST x) <= &2 * h0) /\
    (!x. x IN f ==> {FST x,SND x} IN E)
  ==> tau_fun V E f = tauVEF (V,E,f)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[tauVEF;tau_fun];
  GMATCH_SIMP_TAC (GSYM REAL_OF_NUM_SUB);
  ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `x - u * (v - w) = x' + u * (w - v) <=> x = x'`];
  MATCH_MP_TAC SUM_EQ;
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[];
  MATCH_MP_TAC (arith `x = x' /\ y = y' ==> x*y' = y*x'`);
  REWRITE_TAC[rho_rho_fun;Sphere.rho;Nonlinear_lemma.sol0_over_pi_EQ_const1];
  CONJ_TAC;
    MATCH_MP_TAC (arith `(l = l') ==> &1 + c - c * l = &1 + c *(&1 - l')`);
    BY(ASM_SIMP_TAC[ly_EQ_lmfun]);
  GMATCH_SIMP_TAC azim_dart_azim_in_fan;
  BY(ASM_SIMP_TAC[])
  ]);;
  (* }}} *)


 end;;