(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Zithlqn = struct


open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;




let s_init_J_empty= 
prove_by_refinement(
`!s. MEM s  s_init_list_v39   ==> scs_J_v39 s = (\i j. F)`,

  (* {{{ proof *)
[
REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;LET_DEF;LET_END_DEF;set_of_list; FORALL_IN_CLAUSES;
scs_J_v39_explicit;mk_unadorned_v39]
]);;
  (* }}} *)

let dsv_scs_init= 
prove_by_refinement(
` MEM s  s_init_list_v39   ==> dsv_v39 s vv = scs_d_v39 s`,

  (* {{{ proof *)
[
SIMP_TAC[s_init_J_empty;dsv_J_empty]
]);;
  (* }}} *)


let exists_point_in_V= 
prove_by_refinement(
`  convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
    3 <= CARD V /\ CARD V <= 6 
==> ?v. v IN V`,

  (* {{{ proof *)
[
ONCE_REWRITE_TAC[SET_RULE`(?v. v IN V)<=> ~(V={})`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;CARD_CLAUSES])
THEN ARITH_TAC
]);;
  (* }}} *)






let exists_vv_FF= 
prove_by_refinement(
`  convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
    3 <= CARD V /\ CARD V <= 6 
/\ v, w IN FF
==> ?vv.
 vv 0=v /\ vv 1= w
/\ (!i. vv i= vv (i MOD (CARD V)))
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\ V = IMAGE vv (:num) /\ E = IMAGE (\i. {vv i, vv (SUC i)}) (:num)
/\ FF = IMAGE (\i. vv i,vv (SUC i)) (:num)`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN EXISTS_TAC`(\i:num. ITER i (rho_node1 FF) v)`
THEN REWRITE_TAC[IMAGE;]
THEN STRIP_TAC;

REWRITE_TAC[ITER];

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`1= SUC 0`; ITER]
THEN MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;];

MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN 
MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`;`(V:real^3->bool)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN`!i. ITER i (rho_node1 FF) v = ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v` ASSUME_TAC;

GEN_TAC
THEN REWRITE_TAC[GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[th])
THEN REWRITE_TAC[Hypermap.lemma_add_exponent_function;Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
THEN RESA_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i MOD CARD (V:real^3->bool)`)
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2)[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`]
THEN MRESAL_TAC Hypermap.power_map_fix_point[`CARD (V:real^3->bool)`;`(rho_node1 FF)`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`][Wrgcvdr_cizmrrh.POWER_TO_ITER];

STRIP_TAC;

POP_ASSUM MP_TAC
THEN SET_TAC[];

STRIP_TAC;

POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LT_CARD_MONO_LOFA)
[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`v:real^3`]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD CARD(V:real^3->bool)`;`j MOD CARD(V:real^3->bool)`])
THEN POP_ASSUM MATCH_MP_TAC
THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
THEN MRESA_TAC DIVISION [`j:num`;`CARD (V:real^3->bool)`];

REMOVE_ASSUM_TAC
THEN SUBGOAL_THEN`V = {y | ?x. x IN (:num) /\ y = ITER x (rho_node1 FF) v}` ASSUME_TAC;

REWRITE_TAC[EXTENSION]
THEN GEN_TAC
THEN EQ_TAC;

REWRITE_TAC[IN_ELIM_THM]
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas.LOFA_IMP_LT_CARD_SET_V
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN EXISTS_TAC`n:num`
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[];

REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`x':num`]);

ASM_REWRITE_TAC[]
THEN STRIP_TAC;

ONCE_REWRITE_TAC[EXTENSION]
THEN GEN_TAC
THEN EQ_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESAL_TAC local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;][LET_DEF;LET_END_DEF]
THEN MRESA_TAC Topology.expand_edge_graph_fan[`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN SUBGOAL_THEN `(w:real^3) IN EE v' E`ASSUME_TAC;

POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[EE;IN_ELIM_THM];

POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v':real^3`;]
THEN REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B\/ A=C`]
THEN STRIP_TAC;

EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[ITER];

MP_TAC(ARITH_RULE`x =0 \/ 0<x`)
THEN STRIP_TAC;

POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th;ITER] THEN REPEAT STRIP_TAC)
THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`v':real^3`)
THEN EXISTS_TAC`CARD (V:real^3->bool) -1`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC Tecoxbm.RHO_IVS_IDD
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN SET_TAC[];

SUBGOAL_THEN`(?x'. x = SUC x')` (fun th-> MP_TAC th THEN STRIP_TAC);

EXISTS_TAC`x-1`
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

EXISTS_TAC`x'':num`
THEN ASM_REWRITE_TAC[ITER]
THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th -> MRESA1_TAC th `x'':num`)
THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)
[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER x'' (rho_node1 FF) v:real^3`;]
THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN SET_TAC[];

REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th -> MRESA1_TAC th `x':num`)
THEN REWRITE_TAC[ITER]
THEN MRESA1_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E`ITER x' (rho_node1 FF) v`;

ONCE_REWRITE_TAC[EXTENSION]
THEN GEN_TAC
THEN EQ_TAC;

STRIP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x:real^3#real^3`)
THEN POP_ASSUM (fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`(V:real^3->bool)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[ITER]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];

REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas1.LOCAL_FAN_ORBIT_MAP_VITERFF
THEN ASM_REWRITE_TAC[ITER;ARITH_RULE`A+1= SUC A`]
THEN STRIP_TAC 
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
]);;
  (* }}} *)







let exists_vv= 
prove_by_refinement(
`  convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
    3 <= CARD V /\ CARD V <= 6 
==> ?vv. (!i. vv i= vv (i MOD (CARD V)))
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\ V = IMAGE vv (:num) /\ E = IMAGE (\i. {vv i, vv (SUC i)}) (:num)
/\ FF = IMAGE (\i. vv i,vv (SUC i)) (:num)`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN MP_TAC exists_point_in_V
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN EXISTS_TAC`(\i:num. ITER i (rho_node1 FF) v)`
THEN REWRITE_TAC[IMAGE;]
THEN SUBGOAL_THEN`!i. ITER i (rho_node1 FF) v = ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v` ASSUME_TAC;

GEN_TAC
THEN REWRITE_TAC[GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[th])
THEN REWRITE_TAC[Hypermap.lemma_add_exponent_function;Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
THEN RESA_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i MOD CARD (V:real^3->bool)`)
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2)[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`]
THEN MRESAL_TAC Hypermap.power_map_fix_point[`CARD (V:real^3->bool)`;`(rho_node1 FF)`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`][Wrgcvdr_cizmrrh.POWER_TO_ITER];

STRIP_TAC;

POP_ASSUM MP_TAC
THEN SET_TAC[];

STRIP_TAC;

POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LT_CARD_MONO_LOFA)
[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`v:real^3`]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD CARD(V:real^3->bool)`;`j MOD CARD(V:real^3->bool)`])
THEN POP_ASSUM MATCH_MP_TAC
THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
THEN MRESA_TAC DIVISION [`j:num`;`CARD (V:real^3->bool)`];

REMOVE_ASSUM_TAC
THEN SUBGOAL_THEN`V = {y | ?x. x IN (:num) /\ y = ITER x (rho_node1 FF) v}` ASSUME_TAC;

REWRITE_TAC[EXTENSION]
THEN GEN_TAC
THEN EQ_TAC;

REWRITE_TAC[IN_ELIM_THM]
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas.LOFA_IMP_LT_CARD_SET_V
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN EXISTS_TAC`n:num`
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[];

REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`x':num`]);

ASM_REWRITE_TAC[]
THEN STRIP_TAC;

ONCE_REWRITE_TAC[EXTENSION]
THEN GEN_TAC
THEN EQ_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESAL_TAC local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;][LET_DEF;LET_END_DEF]
THEN MRESA_TAC Topology.expand_edge_graph_fan[`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN SUBGOAL_THEN `(w:real^3) IN EE v' E`ASSUME_TAC;

POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[EE;IN_ELIM_THM];

POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v':real^3`;]
THEN REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B\/ A=C`]
THEN STRIP_TAC;

EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[ITER];

MP_TAC(ARITH_RULE`x =0 \/ 0<x`)
THEN STRIP_TAC;

POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th;ITER] THEN REPEAT STRIP_TAC)
THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`v':real^3`)
THEN EXISTS_TAC`CARD (V:real^3->bool) -1`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC Tecoxbm.RHO_IVS_IDD
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN SET_TAC[];

SUBGOAL_THEN`(?x'. x = SUC x')` (fun th-> MP_TAC th THEN STRIP_TAC);

EXISTS_TAC`x-1`
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

EXISTS_TAC`x'':num`
THEN ASM_REWRITE_TAC[ITER]
THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th -> MRESA1_TAC th `x'':num`)
THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)
[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER x'' (rho_node1 FF) v:real^3`;]
THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN SET_TAC[];

REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th -> MRESA1_TAC th `x':num`)
THEN REWRITE_TAC[ITER]
THEN MRESA1_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E`ITER x' (rho_node1 FF) v`;

ONCE_REWRITE_TAC[EXTENSION]
THEN GEN_TAC
THEN EQ_TAC;

STRIP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x:real^3#real^3`)
THEN POP_ASSUM (fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`(V:real^3->bool)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[ITER]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];

REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MP_TAC Local_lemmas1.LOCAL_FAN_ORBIT_MAP_VITERFF
THEN ASM_REWRITE_TAC[ITER;ARITH_RULE`A+1= SUC A`]
THEN STRIP_TAC 
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
]);;
  (* }}} *)




let SUC_MOD_NOT_EQ=
prove_by_refinement(
`~(i MOD 3 = SUC i MOD 3)`,

  (* {{{ proof *)
[
REWRITE_TAC[ADD1]
THEN STRIP_TAC
THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"YEU")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN MRESAL_TAC DIV_MONO[`i:num`;`i+1`;`3`][ARITH_RULE`~(3=0)/\ i<= i+1`]
THEN MRESAL_TAC DIVISION[`i+1:num`;`3`][ARITH_RULE`~(3=0)`]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`i DIV 3 <= (i + 1) DIV 3 ==>  (i + 1) DIV 3 = i DIV 3 \/ i DIV 3 < (i + 1) DIV 3`)
THEN RESA_TAC;
 
REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
THEN ARITH_TAC;

STRIP_TAC 
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN "YEU"(fun th-> GEN_REWRITE_TAC(LAND_CONV  o LAND_CONV  o ONCE_DEPTH_CONV)[th])
THEN REWRITE_TAC[ARITH_RULE`(i DIV 3 * 3 + (i + 1) MOD 3) + 1 = (i + 1) DIV 3 * 3 + (i + 1) MOD 3
<=>  1 = ((i + 1) DIV 3 - i DIV 3) * 3`]
THEN MP_TAC(ARITH_RULE`i DIV 3 < (i + 1) DIV 3 ==> 1<= ( (i + 1) DIV 3 -i DIV 3 )`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE` 1<= ( (i + 1) DIV 3 -i DIV 3 )==> 3<= ( (i + 1) DIV 3 -i DIV 3 ) *3`)
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC
]);;
  (* }}} *)




let SUC_MOD_EQ1=
prove_by_refinement(
`(SUC i MOD 3 = SUC j MOD 3)
/\ i<=j
==>
(i MOD 3 = j MOD 3) `,

  (* {{{ proof *)
[
REWRITE_TAC[ADD1]
THEN STRIP_TAC
THEN MRESAL_TAC DIVISION[`i+1:num`;`3`][ARITH_RULE`~(3=0)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`i + 1 = (i + 1) DIV 3 * 3 + (j + 1) MOD 3
<=>  (j + 1) MOD 3= (i + 1) - ((i + 1) DIV 3 * 3) `]
THEN STRIP_TAC
THEN MRESAL_TAC DIVISION[`j+1:num`;`3`][ARITH_RULE`~(3=0)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`j + 1 = (j + 1) DIV 3 * 3 + (i + 1) - (i + 1) DIV 3 * 3 <=> j+ (i + 1) DIV 3 * 3  =   (j + 1) DIV 3 * 3 +i `]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`i<=j==> i+1<= j+1`)
THEN RESA_TAC
THEN MRESAL_TAC DIV_MONO[`i+1`;`j+1`;`3`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`j + (i + 1) DIV 3 * 3 = (j + 1) DIV 3 * 3 + i
/\ i<= j /\ (i + 1) DIV 3 <= (j + 1) DIV 3
==> j -i = 3*((j + 1) DIV 3 - (i + 1) DIV 3) `)
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC DIV_MONO[`i:num`;`j:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`j = j DIV 3 * 3 + j MOD 3
/\ i = i DIV 3 * 3 + i MOD 3 /\ i<= j/\ i DIV 3<= j DIV 3
==> j-i = ((j DIV 3 - i DIV 3) * 3 + j MOD 3)  -i MOD 3 `)
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o  DEPTH_CONV)[th])
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESAL_TAC MOD_MULT[`3`;`(j + 1) DIV 3 - (i + 1) DIV 3`][ARITH_RULE`~(3=0)/\ (a*b=b*a)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[ARITH_RULE`a*b=b*a`]
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MP_TAC(ARITH_RULE`i MOD 3 <=j MOD 3 \/ j MOD 3 < i MOD 3:num`)
THEN STRIP_TAC;

MP_TAC(ARITH_RULE`
i MOD 3 <=j MOD 3
==> 
((j DIV 3 - i DIV 3) * 3 + j MOD 3) - i MOD 3
= (j DIV 3 - i DIV 3) * 3 + j MOD 3 - i MOD 3
`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`(j DIV 3 - i DIV 3)`;`3`;`j MOD 3 - i MOD 3`]
THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`j MOD 3 < 3 /\ i MOD 3 <=j MOD 3
 ==> j MOD 3 - i MOD 3 < 3 `)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC MOD_LT[`j MOD 3 - i MOD 3`;`3`]
THEN ASM_TAC
THEN ARITH_TAC;

MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`i MOD 3 < 3/\ j MOD 3< i MOD 3 
 ==> (3+ j MOD 3) - i MOD 3 < 3  /\ 0< (3+ j MOD 3) - i MOD 3`)
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`j DIV 3 - i DIV 3 =0  \/ 1<= j DIV 3 - i DIV 3:num`)
THEN STRIP_TAC;

POP_ASSUM (fun th -> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE` (0 * 3 + j MOD 3) - i MOD 3= j MOD 3 - i MOD 3`])
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`j MOD 3 < i MOD 3
/\ j - i = j MOD 3 - i MOD 3 /\ i<= j ==>  j=i `)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC;

STRIP_TAC
THEN MP_TAC(ARITH_RULE`1 <= j DIV 3 - i DIV 3 /\ 0 < (3 + j MOD 3) - i MOD 3
==> ((j DIV 3 - i DIV 3) * 3 + j MOD 3) - i MOD 3
=((j DIV 3 - i DIV 3)-1) * 3 +(3+ j MOD 3) - i MOD 3`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`(j DIV 3 - i DIV 3 -1)`;`3`;`(3+ j MOD 3) - i MOD 3`]
THEN MRESA_TAC MOD_LT[`(3+j MOD 3) - i MOD 3`;`3`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC
]);;
  (* }}} *)

let SUC_MOD_EQ=
prove_by_refinement(
`(SUC i MOD 3 = SUC j MOD 3)
==>
(i MOD 3 = j MOD 3) `,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`i<=j\/ j<=i:num`)
THEN STRIP_TAC;

MATCH_MP_TAC SUC_MOD_EQ1
THEN ASM_REWRITE_TAC[];

MRESA_TAC (GEN_ALL SUC_MOD_EQ1)[`j:num`;`i:num`]
THEN ASM_REWRITE_TAC[]
]);;
  (* }}} *)


let NOT_IMP_SUC_MOD_EQ=
prove_by_refinement(
`~(i MOD 3 = j MOD 3) 
==> ~(SUC i MOD 3 = SUC j MOD 3)`,

[SIMP_TAC[CONTRAPOS_THM;]
THEN REWRITE_TAC[SUC_MOD_EQ]]);;


let IMP_SUC_MOD_EQ1=
prove_by_refinement(
` ~(k=0) /\ (i MOD k = j MOD k) 
/\ i<= j
==> (SUC i MOD k = SUC j MOD k)`,

  (* {{{ proof *)
[
REWRITE_TAC[ADD1]
THEN STRIP_TAC
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN REMOVE_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i:num = i  DIV k * k + j  MOD k
==>  j  MOD k = i - (i DIV k * k) `)
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th] THEN ASSUME_TAC th)
THEN RESA_TAC
THEN MRESAL_TAC DIVISION[`j:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`i<=j==> i+1<= j+1`)
THEN RESA_TAC
THEN MRESAL_TAC DIV_MONO[`i:num`;`j:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`j = (j  DIV k) * k + i -  (i  DIV k) * k 
/\ i +1 <= j+1 /\ i  DIV k <= j  DIV k /\ ~(k=0)
==> j -i =  (j DIV k) *k - (i  DIV k) *k `)
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
THEN ONCE_REWRITE_TAC[MULT_AC]
THEN MRESAL_TAC DIV_MONO[`i+1:num`;`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN MRESA_TAC LE_MULT_RCANCEL[`((i+1) DIV k)`;`((j+1) DIV k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`i + 1 = (i + 1) DIV k * k + (i + 1) MOD k
/\ j + 1 = (j + 1) DIV k * k + (j + 1) MOD k /\ i<= j/\ ((i+1) DIV k)*k<= ((j+1) DIV k)*k
==> j-i = (((j + 1) DIV k * k  - (i + 1) DIV k * k) + (j + 1) MOD k) - (i + 1) MOD k`)
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
THEN ASM_REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESAL_TAC MOD_MULT[`k:num`;`j DIV k - i DIV k`][ARITH_RULE`~(3=0)/\ (a*b=b*a)`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MP_TAC(ARITH_RULE`(i+1) MOD k <=(j+1) MOD k \/ (j+1) MOD k < (i+1) MOD k:num`)
THEN STRIP_TAC;

MP_TAC(ARITH_RULE`
(i+1) MOD k <=(j+1) MOD k
==> 
((((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k) - (i + 1) MOD k)=
(((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k - (i + 1) MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`((j + 1) DIV k - (i + 1) DIV k)`;`k:num`;`(j + 1) MOD k - (i + 1) MOD k`]
THEN MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`(j + 1) MOD k < k /\ (i + 1) MOD k <=(j + 1) MOD k 
 ==> (j + 1) MOD k  - (i + 1) MOD k < k `)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC MOD_LT[`(j + 1) MOD k  - (i + 1) MOD k`;` k:num`]
THEN REPLICATE_TAC 8 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`(i+1) MOD k < k/\ (j+1) MOD k< (i+1) MOD k 
 ==> (k+ (j+1) MOD k) - (i+1) MOD k < k  /\ 0< (k+ (j+1) MOD k) - (i+1) MOD k`)
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`(j+1) DIV k - (i+1) DIV k =0  \/ 1<= (j+1) DIV k - (i+1) DIV k`)
THEN STRIP_TAC;

POP_ASSUM (fun th -> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE` (0 * k + (j + 1) MOD k) - (i + 1) MOD k= (j + 1) MOD k - (i + 1) MOD k`])
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`(j + 1) MOD k < (i + 1) MOD k
/\ j - i = (j + 1) MOD k - (i + 1) MOD k /\ i<= j ==>  j=i `)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC;

STRIP_TAC
THEN MRESAL_TAC LE_MULT_RCANCEL[`1`;`((j + 1) DIV k - (i + 1) DIV k)`;`k:num`][ARITH_RULE`1*k=k`]
THEN MP_TAC(ARITH_RULE`k <= ((j + 1) DIV k - (i + 1) DIV k)*k /\ 0 < (k + (j + 1) MOD k) - (i + 1) MOD k
==> ((((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k) - (i + 1) MOD k)
=
((((j + 1) DIV k - (i + 1) DIV k) * k- 1*k)+(k+ (j + 1) MOD k) - (i + 1) MOD k)
`)
THEN RESA_TAC
THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
THEN MRESA_TAC MOD_MULT_ADD[`((j + 1) DIV k - (i + 1) DIV k - 1)`;`k:num`;`(k + (j + 1) MOD k) - (i + 1) MOD k`]
THEN MRESA_TAC MOD_LT[`(k + (j + 1) MOD k) - (i + 1) MOD k`;`k:num`]
THEN REPLICATE_TAC 4 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC
]);;
  (* }}} *)


let IMP_SUC_MOD_EQ=
prove_by_refinement(
` ~(k=0) /\ (i MOD k = j MOD k) 
==> (SUC i MOD k = SUC j MOD k)`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`i<=j\/ j<=i:num`)
THEN STRIP_TAC;
MATCH_MP_TAC IMP_SUC_MOD_EQ1
THEN ASM_REWRITE_TAC[];
MRESA_TAC (GEN_ALL IMP_SUC_MOD_EQ1)[`j:num`;`i:num`;`k:num`]
THEN ASM_REWRITE_TAC[]
]);;
  (* }}} *)



let CHOOSE_MOD_3=
prove_by_refinement(
`~(i MOD 3 = j MOD 3) /\ ~(SUC j MOD 3 = i MOD 3)
==> j MOD 3 = SUC i MOD 3`,

  (* {{{ proof *)
[
MP_TAC(ARITH_RULE`i MOD 3= 0 \/ i MOD 3= 1 \/ i MOD 3= 2`)
THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
THEN MP_TAC(ARITH_RULE`j MOD 3= 0 \/ j MOD 3= 1 \/ j MOD 3= 2`)
THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
THEN MP_TAC(ARITH_RULE`SUC j MOD 3= 0 \/ SUC j MOD 3= 1 \/ SUC j MOD 3= 2`)
THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
THEN REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`SUC j MOD 3 IN {0, 1, 2} /\
 j MOD 3 IN {0, 1, 2} /\ i MOD 3 IN {0, 1, 2}
==> {SUC j MOD 3, j MOD 3, i MOD 3 }SUBSET {0, 1, 2}`)
THEN RESA_TAC
THEN SUBGOAL_THEN`CARD {SUC j MOD 3, j MOD 3, i MOD 3 }=3` ASSUME_TAC;

ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY;]
THEN MRESA1_TAC(GEN_ALL SUC_MOD_NOT_EQ)`j:num`
THEN ARITH_TAC;

SUBGOAL_THEN`CARD {0, 1, 2 }=3` ASSUME_TAC;

ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY;]
THEN ARITH_TAC;

SUBGOAL_THEN`FINITE {0, 1, 2 }` ASSUME_TAC;

ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY;];

MRESA_TAC CARD_SUBSET_EQ[`{SUC j MOD 3, j MOD 3, i MOD 3 }`;`{0, 1, 2}`]
THEN MP_TAC(ARITH_RULE`SUC i MOD 3= 0 \/ SUC i MOD 3= 1 \/ SUC i MOD 3= 2`)
THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN ONCE_REWRITE_TAC[SET_RULE` A IN {B,C,D}<=> (A=B\/ A=C\/A=D)`]
THEN MRESA1_TAC(GEN_ALL SUC_MOD_NOT_EQ)`i:num`
THEN MRESA_TAC(GEN_ALL NOT_IMP_SUC_MOD_EQ)[`i:num`;`j:num`]
THEN RESA_TAC
]);;
  (* }}} *)




let SMALL_BALL_ANNULUS_6=
prove_by_refinement(
`   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w))
==>     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) /\ dist(v,w)<= &6 )`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC;
REPLICATE_TAC 4 (POP_ASSUM MP_TAC) 
THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[];
MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
==> v IN ball_annulus /\ w IN ball_annulus`)
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC
]);;
  (* }}} *)





let SMALL_BALL_ANNULUS_6_sqrt8=
prove_by_refinement(
`   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w))
==>     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w) /\ dist(v,w)<= &6 )`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC;
REPLICATE_TAC 4 (POP_ASSUM MP_TAC) 
THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[];
MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
==> v IN ball_annulus /\ w IN ball_annulus`)
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC
]);;
  (* }}} *)



let SMALL_BALL_ANNULUS_6_3=
prove_by_refinement(
`   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w))
==>     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w) /\ dist(v,w)<= &6 )`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC;
REPLICATE_TAC 4 (POP_ASSUM MP_TAC) 
THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[];
MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
==> v IN ball_annulus /\ w IN ball_annulus`)
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC
]);;
  (* }}} *)



let CS_ADJ=
prove(`cs_adj = (\k a1 a2 i j. (if (i MOD k = j MOD k) then &0
			       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))`,

MP_TAC( GENL [`k:num`;`a1:real`;`a2:real`;`i:num`;`j:num`] (SPEC_ALL cs_adj))
THEN REWRITE_TAC[GSYM FUN_EQ_THM]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
THEN SIMP_TAC[FUN_EQ_THM]);;



let ZITHLQN_CASE_3=
prove_by_refinement(
`    V SUBSET ball_annulus /\
     CARD V =3 /\    
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
/\ (s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
         mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd))
/\ (!i.  vv (i MOD (CARD V))= vv i)
/\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
/\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
==>  vv IN BBs_v39 s`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;Oxl_def.periodic;mk_unadorned_v39;CS_ADJ]
THEN STRIP_TAC;

ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];

STRIP_TAC
THEN REPEAT GEN_TAC;

ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN MP_TAC(ARITH_RULE`i MOD 3 = j MOD 3 \/ ~(i MOD 3 = j MOD 3)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[DIST_POS_LE]
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[DIST_REFL]
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC j MOD 3 = i MOD 3 \/ ~(SUC j MOD 3 = i MOD 3)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 7 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

MP_TAC CHOOSE_MOD_3
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;]
THEN ARITH_TAC
]);;
  (* }}} *)



let ZITHLQN_CASE_4=
prove_by_refinement(
`   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
     CARD V =4 /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
/\ (s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
         mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd))
/\ (!i.  vv (i MOD (CARD V))= vv i)
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
/\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
==>  vv IN BBs_v39 s`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN MP_TAC SMALL_BALL_ANNULUS_6
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
THEN STRIP_TAC;

ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];

STRIP_TAC
THEN REPEAT GEN_TAC;

ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[DIST_POS_LE]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[DIST_REFL]
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];


SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;


REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);


 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
THEN POP_ASSUM MATCH_MP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
THEN STRIP_TAC;

EXISTS_TAC`i:num`
THEN SET_TAC[];

EXISTS_TAC`j:num`
THEN SET_TAC[];
]);;
  (* }}} *)





let ZITHLQN_CASE_5=
prove_by_refinement(
`   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
     CARD V =5 /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
/\ (s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
     mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd))
/\ (!i.  vv (i MOD (CARD V))= vv i)
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
/\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
==>  vv IN BBs_v39 s`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN MP_TAC SMALL_BALL_ANNULUS_6
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
THEN STRIP_TAC;

ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];

STRIP_TAC
THEN REPEAT GEN_TAC;

ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[DIST_POS_LE]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[DIST_REFL]
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];

SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;

REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);

REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
THEN POP_ASSUM MATCH_MP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
THEN STRIP_TAC;

EXISTS_TAC`i:num`
THEN SET_TAC[];

EXISTS_TAC`j:num`
THEN SET_TAC[];

]);;
  (* }}} *)





let ZITHLQN_CASE_6=
prove_by_refinement(
`   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
     CARD V =6 /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)  ) /\
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
/\ (s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
     mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd))
/\ (!i.  vv (i MOD (CARD V))= vv i)
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
/\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
==>  vv IN BBs_v39 s`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN MP_TAC SMALL_BALL_ANNULUS_6
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
THEN STRIP_TAC;

ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];

STRIP_TAC
THEN REPEAT GEN_TAC;

ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN MP_TAC(ARITH_RULE`i MOD 6 = j MOD 6 \/ ~(i MOD 6 = j MOD 6)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[DIST_POS_LE]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[DIST_REFL]
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC j MOD 6 = i MOD 6 \/ ~(SUC j MOD 6 = i MOD 6)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC i MOD 6 = j MOD 6 \/ ~(SUC i MOD 6 = j MOD 6)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`6`][ARITH_RULE`~(6=0)`];

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`6`][ARITH_RULE`~(6=0)`];

SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;

REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);

REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
THEN POP_ASSUM MATCH_MP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
THEN STRIP_TAC;

EXISTS_TAC`i:num`
THEN SET_TAC[];

EXISTS_TAC`j:num`
THEN SET_TAC[];
]);;
  (* }}} *)






let ZITHLQN_CASE_5_pro_cs=
prove_by_refinement(
 `   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
     CARD V =5 /\
(!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\
       (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
       {v0,w0} IN E /\
       &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8
/\ (s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k ,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd))
/\ (!i.  vv (i MOD (CARD V))= vv i)
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
/\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
/\ vv 0= v0 /\ vv 1= w0
==>  vv IN BBs_v39 s`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN MP_TAC SMALL_BALL_ANNULUS_6
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
THEN STRIP_TAC;

ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];

STRIP_TAC
THEN REPEAT GEN_TAC;

ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[DIST_POS_LE]
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[DIST_REFL]
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`{i MOD 5,j MOD 5}={0,1} \/ ~({i MOD 5,j MOD 5}={0,1})`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`(~(i=j:num))`ASSUME_TAC;

STRIP_TAC
THEN POP_ASSUM (fun th-> REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[th]);

MP_TAC(SET_RULE`{i MOD 5,j MOD 5} = {0, 1} /\ ~(i MOD 5=j MOD 5)/\ ~(0=1)==> (i MOD 5=0 /\ j MOD 5=1)\/ (i MOD 5=1 /\ j MOD 5=0)`)
THEN ASM_REWRITE_TAC[ARITH_RULE`~(0=1)`]
THEN STRIP_TAC
THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th` j:num` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;

REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[];

SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;

STRIP_TAC
THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0`]
THEN SET_TAC[];

POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 14 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;

REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[];

SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;

STRIP_TAC
THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0`]
THEN SET_TAC[];

POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 15 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC);

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];

SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;

REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);

REPLICATE_TAC 18 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th -> REPLICATE_TAC 18  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
THEN POP_ASSUM MATCH_MP_TAC
THEN REPLICATE_TAC 10 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
THEN STRIP_TAC;

EXISTS_TAC`i:num`
THEN SET_TAC[];

EXISTS_TAC`j:num`
THEN SET_TAC[];
]);;
  (* }}} *)









let ZITHLQN_CASE_4_3=
prove_by_refinement(
`   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
     CARD V =4 /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w) ) /\
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
/\ (s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
      mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd))
/\ (!i.  vv (i MOD (CARD V))= vv i)
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
/\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
==>  vv IN BBs_v39 s`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN MP_TAC SMALL_BALL_ANNULUS_6_3
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
THEN STRIP_TAC;

ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];

STRIP_TAC
THEN REPEAT GEN_TAC;

ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[DIST_POS_LE]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[DIST_REFL]
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];

SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;

REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);

 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
THEN POP_ASSUM MATCH_MP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
THEN STRIP_TAC;

EXISTS_TAC`i:num`
THEN SET_TAC[];

EXISTS_TAC`j:num`
THEN SET_TAC[];
]);;
  (* }}} *)








let ZITHLQN_CASE_5_sqrt8=
prove_by_refinement(
`   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
     CARD V =5 /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8  <= dist(v,w) ) /\
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
/\ (s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
     mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd))
/\ (!i.  vv (i MOD (CARD V))= vv i)
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
/\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
==>  vv IN BBs_v39 s`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN MP_TAC  SMALL_BALL_ANNULUS_6_sqrt8
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
THEN STRIP_TAC;

ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];

STRIP_TAC
THEN REPEAT GEN_TAC;

ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[DIST_POS_LE]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[DIST_REFL]
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];

SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;

REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);

REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
THEN POP_ASSUM MATCH_MP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
THEN STRIP_TAC;

EXISTS_TAC`i:num`
THEN SET_TAC[];

EXISTS_TAC`j:num`
THEN SET_TAC[];
]);;
  (* }}} *)













let ZITHLQN_CASE_4_pro_cs=
prove_by_refinement(
 `   convex_local_fan (V,E,FF) /\
    packing V /\
    V SUBSET ball_annulus /\
     CARD V =4 /\
(!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\
       (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
       {v0,w0} IN E /\
       &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8
/\ (s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k ,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
     mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd))
/\ (!i.  vv (i MOD (CARD V))= vv i)
/\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
/\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
/\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
/\ vv 0= v0 /\ vv 1= w0
==>  vv IN BBs_v39 s`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN MP_TAC SMALL_BALL_ANNULUS_6_sqrt8
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
THEN STRIP_TAC;

ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];

STRIP_TAC
THEN REPEAT GEN_TAC;

ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[DIST_POS_LE]
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[DIST_REFL]
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`{i MOD 4,j MOD 4}={0,1} \/ ~({i MOD 4,j MOD 4}={0,1})`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`(~(i=j:num))`ASSUME_TAC;

STRIP_TAC
THEN POP_ASSUM (fun th-> REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[th]);

MP_TAC(SET_RULE`{i MOD 4,j MOD 4} = {0, 1} /\ ~(i MOD 4=j MOD 4)/\ ~(0=1)==> (i MOD 4=0 /\ j MOD 4=1)\/ (i MOD 4=1 /\ j MOD 4=0)`)
THEN ASM_REWRITE_TAC[ARITH_RULE`~(0=1)`]
THEN STRIP_TAC
THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th` j:num` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;

REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[];

SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;

STRIP_TAC
THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0`]
THEN SET_TAC[];

POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 14 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;

REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];

SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;

REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[];

SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;

STRIP_TAC
THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0`]
THEN SET_TAC[];

POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 15 REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);

ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;

STRIP_TAC
THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[th])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC);

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];

POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];

SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;

REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);

REPLICATE_TAC 18 (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th -> REPLICATE_TAC 18  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
THEN POP_ASSUM MATCH_MP_TAC
THEN REPLICATE_TAC 10 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
THEN STRIP_TAC;

EXISTS_TAC`i:num`
THEN SET_TAC[];

EXISTS_TAC`j:num`
THEN SET_TAC[];
]);;
  (* }}} *)





let exists_vv3=
prove_by_refinement(
`&2 <= norm v1 /\
    &2 <= norm v2 /\
    &2 <= norm v3 /\
    norm v1 <= &2 * h0 /\
    norm v2 <= &2 * h0 /\
    norm v3 <= &2 * h0 /\
    &2 <= dist(v1,v2) /\
    &2 <= dist(v1,v3) /\
    &2 <= dist(v2,v3) /\
    dist(v1,v2) <= &2 * h0 /\
    dist(v1,v3) <= &2 * h0 /\
    dist(v2,v3) <= &2 * h0 
/\ (!i. vv i = 
if i MOD 3 = 0 then v1 else
if i MOD 3 = 1 then v2 else v3)
/\ V= IMAGE vv (:num)  /\  E=  IMAGE (\i. {vv i, vv (SUC i)}) (:num) 
/\  FF= IMAGE (\i. vv i,vv (SUC i)) (:num) 
==> 
       (!i.  vv (i MOD (CARD V))= vv i)
/\    V SUBSET ball_annulus  /\ 
CARD V =3/\   
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)`,

  (* {{{ proof *)
[
STRIP_TAC
THEN SUBGOAL_THEN`(!i.  (vv:num->real^3) (i MOD 3)= vv i)`ASSUME_TAC;

ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`];

SUBGOAL_THEN`(V:real^3->bool)={v1,v2,v3}`ASSUME_TAC;

ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;

STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`x' MOD 3= 0 \/ x' MOD 3= 1\/ x' MOD 3=2`)
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[];

STRIP_TAC
THEN MP_TAC(SET_RULE`x IN {v1, v2, v3:real^3} ==> x = v1 \/ x= v2 \/ x= v3`)
THEN RESA_TAC;

EXISTS_TAC`0:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 3 = 0`]
THEN SET_TAC[];

EXISTS_TAC`1:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3 = 1/\ ~(1 MOD 3 = 0)`]
THEN SET_TAC[];

EXISTS_TAC`2:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(2 MOD 3 = 1) /\ ~(2 MOD 3 = 0)`]
THEN SET_TAC[];

SUBGOAL_THEN(`~(v1=v2:real^3) /\ ~(v1=v3:real^3) /\ ~(v3=v2:real^3)`)ASSUME_TAC;

STRIP_TAC;

STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DIST_REFL])
THEN REAL_ARITH_TAC;

STRIP_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DIST_REFL])
THEN REAL_ARITH_TAC;

SUBGOAL_THEN`CARD (V:real^3->bool)=3` ASSUME_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY;]
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN ARITH_TAC;

POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN POP_ASSUM(fun th-> 
 POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
THEN ASSUME_TAC th)
THEN ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`]
THEN STRIP_TAC;

MATCH_MP_TAC(SET_RULE`(v1 IN  ball_annulus
/\ v2 IN  ball_annulus /\ v3 IN  ball_annulus)==> {v1, v2, v3} SUBSET ball_annulus  `)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ball_annulus;DIFF;cball;ball;IN_ELIM_THM; REAL_ARITH`~(a< &2)<=> &2<=a`;DIST_0];

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3= 0 \/ x MOD 3= 1\/ x MOD 3=2`)
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[];

MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`0`;`3`][ARITH_RULE`~(3=0)/\ 0 MOD 3=0/\ SUC 0 MOD 3=1/\ ~(1=0)`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{v, w} = {v1, v2} /\ ~(v1=v2) ==>(v=v1 /\ w=v2)\/ (v=v2 /\
 w=v1:real^3)`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`1`;`3`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ SUC 1 MOD 3=2/\ ~(1=0)/\ ~(2=1)/\ ~(2=0)`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{v, w} = {v2, v3} /\ ~(v3=v2) ==>(v=v2 /\ w=v3)\/ (v=v3 /\
 w=v2:real^3)`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`2`;`3`][ARITH_RULE`~(3=0)/\ 2 MOD 3=2/\ SUC 2 MOD 3=0/\ ~(1=0)/\ ~(2=1)/\ ~(2=0)`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{v, w} = {v3, v1} /\ ~(v1=v3) ==>(v=v1 /\ w=v3)\/ (v=v3 /\
 w=v1:real^3)`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
]);;
  (* }}} *)



let ZITHLQN=
prove_by_refinement(`(!s vv. MEM s  s_init_list_v39 /\ vv IN
			 BBs_v39 s ==> 
			 &0 <= taustar_v39 s vv)  ==> JEJTVGB_assume_v39`,

  (* {{{ proof *)
[
REWRITE_TAC[IMP_CONJ]
THEN REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN REPEAT STRIP_TAC;

MP_TAC(ARITH_RULE`4<= CARD(V:real^3->bool) /\ CARD(V:real^3->bool)<= 6
==>  CARD V= 4\/ CARD V=5 \/ CARD V=6 `)
THEN RESA_TAC;

ABBREV_TAC`(s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
         mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd))`
THEN SUBGOAL_THEN 
`s IN
          set_of_list
          (let upperbd = &6 in
           let a_pro =
               (\k p a1 a2 i j.
                    if i MOD k = j MOD k
                    then &0
                    else if {i MOD k, j MOD k} = {0, 1}
                         then p
                         else if j MOD k = SUC i MOD k \/
                                 SUC j MOD k = i MOD k
                              then a1
                              else a2) in
           [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
            (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
                                          (cs_adj 5 (&2) (&2 * h0))
                                          (cs_adj 5 (&2 * h0) upperbd); 
           mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
           (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
                                         (cs_adj 3 (&2) (&2 * h0))
                                         (cs_adj 3 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
           (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
                                         (cs_adj 4 (&2) (&3))
                                         (cs_adj 4 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
           (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
                                              (a_pro 4 (&2 * h0) (&2) sqrt8)
                                              (a_pro 4 sqrt8 (&2 * h0)
                                              upperbd)])` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;]
THEN SET_TAC[];

MP_TAC exists_vv
THEN ASM_REWRITE_TAC[ARITH_RULE`3<=4`]
THEN STRIP_TAC
THEN MP_TAC ZITHLQN_CASE_4
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
THEN ASM_REWRITE_TAC[])
THEN STRIP_TAC
THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;

ABBREV_TAC`(s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
     mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd) )`
THEN SUBGOAL_THEN 
`s IN
          set_of_list
          (let upperbd = &6 in
           let a_pro =
               (\k p a1 a2 i j.
                    if i MOD k = j MOD k
                    then &0
                    else if {i MOD k, j MOD k} = {0, 1}
                         then p
                         else if j MOD k = SUC i MOD k \/
                                 SUC j MOD k = i MOD k
                              then a1
                              else a2) in
           [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
            (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
                                          (cs_adj 5 (&2) (&2 * h0))
                                          (cs_adj 5 (&2 * h0) upperbd); 
           mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
           (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
                                         (cs_adj 3 (&2) (&2 * h0))
                                         (cs_adj 3 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
           (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
                                         (cs_adj 4 (&2) (&3))
                                         (cs_adj 4 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
           (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
                                              (a_pro 4 (&2 * h0) (&2) sqrt8)
                                              (a_pro 4 sqrt8 (&2 * h0)
                                              upperbd)])` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
THEN SET_TAC[];

MP_TAC exists_vv
THEN ASM_REWRITE_TAC[ARITH_RULE`3<=5`]
THEN STRIP_TAC
THEN MP_TAC ZITHLQN_CASE_5
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
THEN ASM_REWRITE_TAC[])
THEN STRIP_TAC
THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;

ABBREV_TAC`(s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
     mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd) )`
THEN SUBGOAL_THEN 
`s IN
          set_of_list
          (let upperbd = &6 in
           let a_pro =
               (\k p a1 a2 i j.
                    if i MOD k = j MOD k
                    then &0
                    else if {i MOD k, j MOD k} = {0, 1}
                         then p
                         else if j MOD k = SUC i MOD k \/
                                 SUC j MOD k = i MOD k
                              then a1
                              else a2) in
           [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
            (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
                                          (cs_adj 5 (&2) (&2 * h0))
                                          (cs_adj 5 (&2 * h0) upperbd); 
           mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
           (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
                                         (cs_adj 3 (&2) (&2 * h0))
                                         (cs_adj 3 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
           (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
                                         (cs_adj 4 (&2) (&3))
                                         (cs_adj 4 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
           (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
                                              (a_pro 4 (&2 * h0) (&2) sqrt8)
                                              (a_pro 4 sqrt8 (&2 * h0)
                                              upperbd)])` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
THEN SET_TAC[];

MP_TAC exists_vv
THEN ASM_REWRITE_TAC[ARITH_RULE`3<=6`]
THEN STRIP_TAC
THEN MP_TAC ZITHLQN_CASE_6
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
THEN ASM_REWRITE_TAC[])
THEN STRIP_TAC
THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(6<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(6=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;

ABBREV_TAC `(vv i = 
if i MOD 3 = 0 then v1 else
if i MOD 3 = 1 then v2 else v3:real^3)`
THEN ABBREV_TAC`V = IMAGE (vv:num->real^3) (:num)`
THEN ABBREV_TAC`  E=  IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num) `
THEN ABBREV_TAC` FF= IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num) `
THEN ABBREV_TAC`(s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
              mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd))`
THEN SUBGOAL_THEN 
`s IN
          set_of_list
          (let upperbd = &6 in
           let a_pro =
               (\k p a1 a2 i j.
                    if i MOD k = j MOD k
                    then &0
                    else if {i MOD k, j MOD k} = {0, 1}
                         then p
                         else if j MOD k = SUC i MOD k \/
                                 SUC j MOD k = i MOD k
                              then a1
                              else a2) in
           [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
            (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
                                          (cs_adj 5 (&2) (&2 * h0))
                                          (cs_adj 5 (&2 * h0) upperbd); 
           mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
           (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
                                         (cs_adj 3 (&2) (&2 * h0))
                                         (cs_adj 3 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
           (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
                                         (cs_adj 4 (&2) (&3))
                                         (cs_adj 4 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
           (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
                                              (a_pro 4 (&2 * h0) (&2) sqrt8)
                                              (a_pro 4 sqrt8 (&2 * h0)
                                              upperbd)])` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
THEN SET_TAC[];

MP_TAC exists_vv3
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MP_TAC ZITHLQN_CASE_3
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
THEN ASM_REWRITE_TAC[])
THEN SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`]
THEN STRIP_TAC
THEN REPLICATE_TAC 22 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`(3<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(6=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th;])
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`0 MOD 3=0/\ 1 MOD 3=1 /\ 2 MOD 3=2/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)`]
THEN REAL_ARITH_TAC;

ABBREV_TAC`(s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
      mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd) )`
THEN SUBGOAL_THEN 
`s IN
          set_of_list
          (let upperbd = &6 in
           let a_pro =
               (\k p a1 a2 i j.
                    if i MOD k = j MOD k
                    then &0
                    else if {i MOD k, j MOD k} = {0, 1}
                         then p
                         else if j MOD k = SUC i MOD k \/
                                 SUC j MOD k = i MOD k
                              then a1
                              else a2) in
           [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
            (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
                                          (cs_adj 5 (&2) (&2 * h0))
                                          (cs_adj 5 (&2 * h0) upperbd); 
           mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
           (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
                                         (cs_adj 3 (&2) (&2 * h0))
                                         (cs_adj 3 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
           (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
                                         (cs_adj 4 (&2) (&3))
                                         (cs_adj 4 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
           (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
                                              (a_pro 4 (&2 * h0) (&2) sqrt8)
                                              (a_pro 4 sqrt8 (&2 * h0)
                                              upperbd)])` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
THEN SET_TAC[];

MP_TAC exists_vv
THEN ASM_REWRITE_TAC[ARITH_RULE`3<=5/\ 5<=6`]
THEN STRIP_TAC
THEN MP_TAC ZITHLQN_CASE_5_sqrt8
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
THEN ASM_REWRITE_TAC[])
THEN STRIP_TAC
THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;

ABBREV_TAC`(s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
      mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd) )`
THEN SUBGOAL_THEN 
`s IN
          set_of_list
          (let upperbd = &6 in
           let a_pro =
               (\k p a1 a2 i j.
                    if i MOD k = j MOD k
                    then &0
                    else if {i MOD k, j MOD k} = {0, 1}
                         then p
                         else if j MOD k = SUC i MOD k \/
                                 SUC j MOD k = i MOD k
                              then a1
                              else a2) in
           [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
            (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
                                          (cs_adj 5 (&2) (&2 * h0))
                                          (cs_adj 5 (&2 * h0) upperbd); 
           mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
           (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
                                         (cs_adj 3 (&2) (&2 * h0))
                                         (cs_adj 3 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
           (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
                                         (cs_adj 4 (&2) (&3))
                                         (cs_adj 4 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
           (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
                                              (a_pro 4 (&2 * h0) (&2) sqrt8)
                                              (a_pro 4 sqrt8 (&2 * h0)
                                              upperbd)])` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
THEN SET_TAC[];

MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN  MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w0:real^3`;`v0:real^3`;`FF:real^3#real^3->bool`;];

MRESA_TAC(GEN_ALL exists_vv_FF)
[`v0:real^3`;`w0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`3<=5 /\ 5<=6`]
THEN STRIP_TAC
THEN MP_TAC ZITHLQN_CASE_5_pro_cs
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;

MRESA_TAC(GEN_ALL exists_vv_FF)
[`w0:real^3`;`v0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`3<=5 /\ 5<=6`]
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`w0:real^3`;`v0:real^3`;`vv:num->real^3`;`s:scs_v39`]
(GEN_ALL ZITHLQN_CASE_5_pro_cs))
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{w, v} = {v0, w0}<=> {w, v} = {w0, v0}`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]
THEN ASSUME_TAC th)
THEN STRIP_TAC
THEN STRIP_TAC
THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;

ABBREV_TAC`(s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
      mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd) )`
THEN SUBGOAL_THEN 
`s IN
          set_of_list
          (let upperbd = &6 in
           let a_pro =
               (\k p a1 a2 i j.
                    if i MOD k = j MOD k
                    then &0
                    else if {i MOD k, j MOD k} = {0, 1}
                         then p
                         else if j MOD k = SUC i MOD k \/
                                 SUC j MOD k = i MOD k
                              then a1
                              else a2) in
           [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
            (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
                                          (cs_adj 5 (&2) (&2 * h0))
                                          (cs_adj 5 (&2 * h0) upperbd); 
           mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
           (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
                                         (cs_adj 3 (&2) (&2 * h0))
                                         (cs_adj 3 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
           (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
                                         (cs_adj 4 (&2) (&3))
                                         (cs_adj 4 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
           (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
                                              (a_pro 4 (&2 * h0) (&2) sqrt8)
                                              (a_pro 4 sqrt8 (&2 * h0)
                                              upperbd)])` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
THEN SET_TAC[];

MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
THEN  MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w0:real^3`;`v0:real^3`;`FF:real^3#real^3->bool`;];

MRESA_TAC(GEN_ALL exists_vv_FF)
[`v0:real^3`;`w0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`3<=4 /\ 4<=6`]
THEN STRIP_TAC
THEN MP_TAC ZITHLQN_CASE_4_pro_cs
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;

MRESA_TAC(GEN_ALL exists_vv_FF)
[`w0:real^3`;`v0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`3<=4 /\ 4<=6`]
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`w0:real^3`;`v0:real^3`;`vv:num->real^3`;`s:scs_v39`]
(GEN_ALL ZITHLQN_CASE_4_pro_cs))
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{w, v} = {v0, w0}<=> {w, v} = {w0, v0}`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]
THEN ASSUME_TAC th)
THEN STRIP_TAC
THEN STRIP_TAC
THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;

ABBREV_TAC`(s=let upperbd = &6 in
  let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
				else (if {i MOD k,j MOD k}={0,1} then p
				      else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
         mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd))`
THEN SUBGOAL_THEN 
`s IN
          set_of_list
          (let upperbd = &6 in
           let a_pro =
               (\k p a1 a2 i j.
                    if i MOD k = j MOD k
                    then &0
                    else if {i MOD k, j MOD k} = {0, 1}
                         then p
                         else if j MOD k = SUC i MOD k \/
                                 SUC j MOD k = i MOD k
                              then a1
                              else a2) in
           [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
            (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
                                          (cs_adj 5 (&2) (&2 * h0))
                                          (cs_adj 5 (&2 * h0) upperbd); 
           mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
           (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
                                         (cs_adj 3 (&2) (&2 * h0))
                                         (cs_adj 3 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
           (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
                                         (cs_adj 4 (&2) (&3))
                                         (cs_adj 4 (&2 * h0) upperbd); 
           mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
           (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
                                              (a_pro 4 (&2 * h0) (&2) sqrt8)
                                              (a_pro 4 sqrt8 (&2 * h0)
                                              upperbd)])` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
THEN SET_TAC[];

MP_TAC exists_vv
THEN ASM_REWRITE_TAC[ARITH_RULE`3<=4/\ 4<=6`]
THEN STRIP_TAC
THEN MP_TAC ZITHLQN_CASE_4_3
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
THEN ASM_REWRITE_TAC[])
THEN STRIP_TAC
THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;

EXPAND_TAC"s"
THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];

ASM_REWRITE_TAC[d_tame]
THEN MP_TAC dsv_scs_init
THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
THEN REAL_ARITH_TAC;
]);;
  (* }}} *)





 end;;


(*
let check_completeness_claimA_concl = 
  Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) 
*)