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


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


module Jcyfmrp = struct


open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





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

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;

open Qknvmlb;;
open Odxlstcv2;;

open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;

open Nuxcoea;;
open Fektyiy;;




let J_EMPY_CASES_A_EQ_2=
prove(`(!i. scs_a_v39 s i (SUC i) = &2)
  /\ is_scs_v39 s 
==>  scs_J_v39 s i= {}`,

STRIP_TAC
THEN MP_TAC(SET_RULE`(?x. scs_J_v39 s i x) \/ (scs_J_v39 s i= {})`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
THEN THAYTHEL_ASM_TAC(21-19)[`i`;`x`][]
THEN THAYTHEL_ASM_TAC (23-18)[`i`;`x`][]
THENL[
DICH_TAC 4 
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i`;`x`;`s`;`i`;`SUC i`][is_scs_v39]
THEN POP_ASSUM MP_TAC
THEN MP_TAC Geomdetail.db_t0_sq8
THEN REWRITE_TAC[sqrt8]
THEN REAL_ARITH_TAC;

DICH_TAC 4
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i`;`x`;`s`;`SUC x`;`x`][is_scs_v39]
THEN POP_ASSUM MP_TAC
THEN MP_TAC Geomdetail.db_t0_sq8
THEN REWRITE_TAC[sqrt8]
THEN REAL_ARITH_TAC]);;
let DIST_EDGE_LE_CSTAB_CASE_LE3=
prove(`3< scs_k_v39 s /\ BBs_v39 s v /\ is_scs_v39 s ==> dist(v i, v (SUC i))<= cstab`,

REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;is_scs_v39]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (24-21)[`i`]
THEN THAYTHE_TAC (24-3)[`i`;`SUC i`]
THEN DICH_TAC 0
THEN DICH_TAC 1
THEN REAL_ARITH_TAC);;

let J_EMPY_CASES_A_EQ_2_V1=
prove(
`scs_a_v39 s i (SUC i) = &2/\ scs_a_v39 s (SUC i) (SUC(SUC i)) = &2
  /\ is_scs_v39 s 
==>  scs_J_v39 s (SUC i)= {}`,

STRIP_TAC
THEN MP_TAC(SET_RULE`(?x. scs_J_v39 s (SUC i) x) \/ (scs_J_v39 s (SUC i)= {})`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
THEN THAYTHEL_ASM_TAC(21-19)[`SUC i`;`x`][]
THEN THAYTHEL_ASM_TAC (23-18)[`SUC i`;`x`][]
THENL[
DICH_TAC 4 
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC i`;`x`;`s`;`SUC i`;`SUC (SUC i)`][is_scs_v39]
THEN POP_ASSUM MP_TAC
THEN MP_TAC Geomdetail.db_t0_sq8
THEN REWRITE_TAC[sqrt8]
THEN REAL_ARITH_TAC;

DICH_TAC 4
THEN MP_TAC(ARITH_RULE`3<= scs_k_v39 s==> ~(scs_k_v39 s= 0)`)
THEN RESA_TAC
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`scs_k_v39 s`;`i`;`x`;`1`][ARITH_RULE`1+x= SUC x`]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`(SUC i)`;`x`;`s`;`SUC i`;`i`][is_scs_v39]
THEN POP_ASSUM MP_TAC
THEN MP_TAC Geomdetail.db_t0_sq8
THEN REWRITE_TAC[sqrt8]
THEN REAL_ARITH_TAC]);;



let SCS_M_LE_1= 
prove_by_refinement(` CARD (scs_M s) <= 1 /\ is_scs_v39 s 
==> ?p. (!i. ~(i MOD scs_k_v39 s=p MOD scs_k_v39 s)==> scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 )`,

[
STRIP_TAC
THEN POP_ASSUM (fun th-> MP_TAC th
THEN ASSUME_TAC th)
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
THEN DICH_TAC (21)
THEN REWRITE_TAC[scs_M]
THEN REWRITE_TAC[ARITH_RULE`a<=1 <=> a= 0\/ a=1`]
THEN SUBGOAL_THEN`FINITE
      {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;

MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..6`
THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN GEN_TAC
THEN DICH_TAC(20-3)
THEN ARITH_TAC;


ABBREV_TAC`k=scs_k_v39 s`
THEN RESA_TAC;

MRESA_TAC CARD_EQ_0[`{i | i < scs_k_v39 s /\
        (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM]
THEN STRIP_TAC
THEN EXISTS_TAC `0`
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
THEN RESA_TAC
THEN THAYTHES_TAC 3[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN THAYTHES_TAC (30-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN REAL_ARITH_TAC;


MRESA_TAC Local_lemmas.FINITE_CARD1_IMP_SINGLETON[`{i | i < k /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN STRIP_TAC
THEN EXISTS_TAC`x:num`
THEN GEN_TAC
THEN STRIP_TAC
THEN THAYTHEL_ASM_TAC 1[`x`][]
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
THEN RESA_TAC
THEN DICH_TAC 5
THEN ASM_SIMP_TAC[MOD_LT]
THEN STRIP_TAC
THEN THAYTHES_TAC 3[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN THAYTHES_TAC (32-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN REAL_ARITH_TAC]);;



let JCYFMRP_concl = `
main_nonlinear_terminal_v11
==>
(!s (v:num->real^3).
  3< scs_k_v39 s/\
  is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
  CARD (scs_M s) <= 1 /\
  (!i. scs_a_v39 s i (SUC i) = &2) /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) ==>
  (?i. dist(v i, v (i+1)) = &2))`;;





let JCYFMRP=prove_by_refinement(  JCYFMRP_concl,
[
MP_TAC Cuxvzoz.CUXVZOZ
THEN STRIP_TAC
THEN STRIP_TAC
THEN REWRITE_TAC[IN;scs_generic]
THEN REPEAT GEN_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`?i. dist (v i,v (i + 1)) = &2\/ ~(?i. dist ((v:num->real^3) i,v (i + 1)) = &2)`)
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
;


EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
;

DICH_TAC 1
THEN DICH_TAC 0
THEN REWRITE_TAC[NOT_EXISTS_THM]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN SUBGOAL_THEN`!i. &2< dist((v:num->real^3) i, v (SUC i))`ASSUME_TAC
;


GEN_TAC
THEN MATCH_MP_TAC(REAL_ARITH`a<=b /\ ~(b= a)==> a<b`)
THEN MP_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2
THEN REWRITE_TAC[GSYM dist]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ADD1];



SUBGOAL_THEN`!i. norm ((v:num->real^3) i)= &2` ASSUME_TAC
;



GEN_TAC
THEN MP_TAC(REAL_ARITH`norm ((v:num->real^3) i)= &2\/ ~(norm ((v:num->real^3) i)= &2)`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN MRESA_TAC J_EMPY_CASES_A_EQ_2[`s`;`i`]
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN DICH_TAC 0
THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_EXISTS_THM]
THEN STRIP_TAC
THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) i) V' E')` ASSUME_TAC;



REPEAT RESA_TAC
;

SUBGOAL_THEN`!i'. ~(i' MOD k = i MOD k) ==> scs_a_v39 s i i' < dist ((v:num->real^3) i,v i')`ASSUME_TAC;



REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`i' MOD k= SUC i MOD k\/ ~(i' MOD k= SUC i MOD k)`)
THEN RESA_TAC
;


MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i'`;`v:num->real^3`;`SUC i:num`]
THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i`;`i' `;`s:scs_v39`;`i`;`SUC i`][]
;



MP_TAC(SET_RULE`SUC i' MOD k= i MOD k\/ ~(SUC i' MOD k= i MOD k)`)
THEN RESA_TAC
;


MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`SUC i':num`]
THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i`;`i' `;`s:scs_v39`;`SUC i'`;`i'`][]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];



THAYTHEL_TAC (27-13)[`i`;`i'`][scs_diag]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;



MRESAL_TAC ODXLSTCv2[`s`;`k`;`v`;`i:num`][]
;



MP_TAC SCS_M_LE_1
THEN RESA_TAC
THEN SUBGOAL_THEN`!i. ~(i MOD k= p MOD k )/\ ~(i MOD k= SUC p MOD k )
==> pi / &2 < azim (vec 0) (v i) (v (SUC i)) ((v:num->real^3) (i + k - 1))`
ASSUME_TAC
;


GEN_TAC
THEN STRIP_TAC
THEN MP_TAC SYNQIWN
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN EXISTS_TAC`s:scs_v39`
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC;



MATCH_MP_TAC(GEN_ALL(REAL_ARITH`a<=b/\ b<=c ==> a<=c`))
THEN EXISTS_TAC`scs_b_v39 s i (SUC i)`
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
THEN REPEAT RESA_TAC
THEN MATCH_DICH_TAC 2
THEN ASM_REWRITE_TAC[];



MATCH_MP_TAC(GEN_ALL(REAL_ARITH`a<=b/\ b<=c ==> a<=c`))
THEN EXISTS_TAC`scs_b_v39 s (i+k-1) (SUC (i+k-1))`
THEN MP_TAC(ARITH_RULE`3<k==> SUC (i + k - 1)= 1*k+i/\ ~(k<=3)/\ ~(k=0)`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
THEN REPEAT RESA_TAC
;



MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i+k-1`;`1*k+i `;`s:scs_v39`;`i+k-1`;`(1*k+i)MOD k`][MOD_REFL;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i+k-1`;`i MOD k `;`s:scs_v39`;`i+k-1`;`i`][MOD_REFL;MOD_MULT_ADD]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];



MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i+k-1`;`1*k+i `;`s:scs_v39`;`i+k-1`;`(1*k+i)MOD k`][MOD_REFL;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i+k-1`;`i MOD k `;`s:scs_v39`;`i+k-1`;`i`][MOD_REFL;MOD_MULT_ADD]
THEN THAYTHE_TAC (28-21)[`i+k-1`]
THEN MATCH_DICH_TAC 0
THEN DICH_TAC (27-22)
THEN ASM_REWRITE_TAC[CONTRAPOS_THM]
THEN STRIP_TAC
THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`i+k-1`;`p`;`k`][MOD_MULT_ADD];



MP_TAC(ARITH_RULE`3<k==> SUC (i + k - 1)= i+ 1*k+0/\ ~(k<=3)/\ ~(k=0)/\ k-1<k
/\ (i+1)+1=i+2 /\ 1<k /\ 2<k/\ 0<k/\ ~(1=k-1)/\ ~(2=k-1)/\ ~(1=0)`)
THEN RESA_TAC
THEN THAYTHES_TAC (31-14)[`SUC i`;`i+k-1`;][scs_diag;ADD1;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT;MOD_MULT_ADD]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;



MP_TAC(SET_RULE` (!i. ~(i MOD k = p MOD k) /\ ~(i MOD k = SUC p MOD k)
          ==> pi<= azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1))) \/ ~(!i. ~(i MOD k = p MOD k) /\ ~(i MOD k = SUC p MOD k)
          ==> pi<= azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1))) `)
THEN RESA_TAC
;





SUBGOAL_THEN`!i. ~(i MOD k = p MOD k) /\ ~(i MOD k = SUC p MOD k)
          ==>  azim (vec 0) (v i) (v (SUC i)) ((v:num->real^3) (i + k - 1))= pi`ASSUME_TAC
;



REPEAT STRIP_TAC
THEN THAYTHE_TAC 2[`i`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`]
THEN MRESA_TAC WL_IN_V[`i`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`i+k-1`;`v:num->real^3`]
THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (i)`;`v`;`i`;`k`]
THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v i`]
THEN THAYTHE_TAC 0[`v (i+k-1)`]
THEN DICH_TAC 0
THEN DICH_TAC (27-22)
THEN REWRITE_TAC[ADD1]
THEN REAL_ARITH_TAC;


SUBGOAL_THEN`(0..(k-1)) DELETE p MOD k DELETE SUC p MOD k SUBSET{i | i < k /\ azim (vec 0) (v i) (v (SUC i)) ((v:num->real^3) (i + k - 1)) = pi}`
ASSUME_TAC
;


REWRITE_TAC[SUBSET;IN_ELIM_THM;DELETE;IN_NUMSEG;]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> (x<=k-1<=> x<k )`)
THEN RESA_TAC
THEN THAYTHES_TAC 5[`x:num`][MOD_LT;];


MP_TAC(ARITH_RULE`3<k==> ~(k=0 )/\ 1<k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`p`;`k`]
THEN MP_TAC(ARITH_RULE`3<k/\ p MOD k< k ==> p MOD k<=k-1/\ (k-1+1)-0=k`)
THEN RESA_TAC
THEN MRESAS_TAC Hypermap.CARD_MINUS_ONE[`0..(k-1)`;`p MOD k`][FINITE_NUMSEG;IN_NUMSEG;ARITH_RULE`0<=a`;CARD_NUMSEG]
THEN MP_TAC(ARITH_RULE`3<k/\ k = CARD ((0..k - 1) DELETE p MOD k) + 1 ==>  CARD ((0..k - 1) DELETE p MOD k) =k-1`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
THEN RESA_TAC
THEN SUBGOAL_THEN`SUC p MOD k IN (0..k - 1) DELETE p MOD k`ASSUME_TAC
;


ASM_REWRITE_TAC[DELETE;IN_ELIM_THM;IN_NUMSEG]
THEN MRESA_TAC DIVISION[`SUC p`;`k`]
THEN MP_TAC(ARITH_RULE`3<k/\ SUC p MOD k< k ==> SUC p MOD k<=k-1/\ 0<= SUC p MOD k/\ 1<k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ];




MRESAS_TAC Hypermap.CARD_MINUS_ONE[`(0..(k-1)) DELETE p MOD k`;`SUC p MOD k`][FINITE_NUMSEG;IN_NUMSEG;ARITH_RULE`0<=a`;CARD_NUMSEG;FINITE_DELETE]
THEN MP_TAC(ARITH_RULE`3<k/\ k - 1 = CARD ((0..k - 1) DELETE p MOD k DELETE SUC p MOD k) + 1 ==>  CARD ((0..k - 1) DELETE p MOD k DELETE SUC p MOD k) =k-2`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
THEN RESA_TAC
;


SUBGOAL_THEN`FINITE
      {i | i < k /\ azim (vec 0) ((v:num->real^3) i) (v (SUC i)) (v (i + k - 1)) = pi}`ASSUME_TAC
;


MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;


MRESA_TAC CARD_SUBSET[`(0..k - 1) DELETE p MOD k DELETE SUC p MOD k`;`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`]
THEN MRESAL_TAC Aursipd.AURSIPD[`s`;`v`][scs_generic;IN;scs_is_str]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DICH_TAC (32-5)
THEN ABBREV_TAC`a= CARD {i | i < k /\ azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi}`
THEN ARITH_TAC;



DICH_TAC 5
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<=b)<=> b<a`]
THEN STRIP_TAC
THEN STRIP_TAC;



DICH_TAC 23
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`FF`;`k`;`i`;`v`][scs_generic;GSYM ADD1];



THAYTHES_TAC (22-14)[`SUC i`;`i+k-1`][Ocbicby.scs_diag_2]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;


STRIP_TAC
;



REPEAT RESA_TAC
THEN THAYTHES_TAC (24-14)[`i'`;`j`][Ocbicby.scs_diag_2]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;



STRIP_TAC;



ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1]
THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v i`;`v`;`i`;`k`][GSYM ADD1];



STRIP_TAC;



ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1]
THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v i`;`v`;`i`;`k`][GSYM ADD1]
THEN THAYTHE_TAC (24-18)[`i`];

STRIP_TAC
;


MATCH_DICH_TAC (22-17)
THEN ASM_REWRITE_TAC[]
;


STRIP_TAC
;

MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`i`]
THEN MRESAS_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i+k-1`][Imjxphr.EQ_W_L_IN_BBS;GSYM dist]
;



MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`i`]
THEN MRESAL_TAC DIST_EDGE_LE_CSTAB_CASE_LE3[`s`;`v`;`i+k-1`][Imjxphr.EQ_W_L_IN_BBS;GSYM dist]
;


]);;





 end;;


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