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


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


module Rrcwnsj = 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 BB_VV_FUN_EQ=
prove(`is_scs_v39 s /\ BBs_v39 s vv
   ==> (!i j. vv i = vv j <=> i MOD (scs_k_v39 s) = j MOD (scs_k_v39 s))`,

REPEAT RESA_TAC
THEN EQ_TAC
THENL[
MRESA_TAC W_IN_BB_FUN_EQ[`vv`;`i`;`j`;`s`];
MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`vv`;`j`]]);;
let WL_IN_E=
prove(`{(w:num->real^3) l,w (SUC l)} IN IMAGE (\i. {w i,w (SUC i)}) (:num)`,

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[]);;


let LUNAR_IN_V=
prove(`lunar (v,w) V E==> v IN V/\ w IN V`,

REWRITE_TAC[lunar]
THEN SET_TAC[]);;


let B_LE_2h0_A_EQ2_IN_CASES_6=
prove(
`scs_k_v39 s=6  /\ is_scs_v39 s 
==> !i. 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 GEN_TAC
THEN DICH_TAC (0)
THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
THEN SUBGOAL_THEN`FINITE
      {i | i < 6 /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC
THENL[

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

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


let J_EMPY_CASES_6=
prove(`scs_k_v39 s=6  /\ 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 MP_TAC B_LE_2h0_A_EQ2_IN_CASES_6
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(22-19)[`i`;`x`][]
THEN THAYTHEL_ASM_TAC (24-18)[`i`;`x`][]
THENL[

DICH_TAC (25-18)
THEN RESA_TAC
THEN DICH_TAC 4
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i`;`x`;`s`;`i`;`SUC i`][is_scs_v39]
THEN THAYTHE_TAC (25-19)[`i`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

DICH_TAC (25-18)
THEN RESA_TAC
THEN DICH_TAC 4
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i`;`x`;`s`;`SUC x`;`x`][is_scs_v39]
THEN THAYTHE_TAC (25-19)[`x`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC]);;

let BB_RHO_NODE_IVS=
prove(`scs_k_v39 s = k /\
       vv p1 = u /\
       IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\
       is_scs_v39 s /\
       3<k /\
       BBs_v39 s vv
       ==> rho_node1 FF u = vv (p1+1) /\ ivs_rho_node1 FF u = vv (p1+k-1)`,

STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
THEN RESA_TAC
THEN MP_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME
THEN RESA_TAC
THEN THAYTHEL_ASM_TAC 0[`SUC 0`][ITER;I_DEF;ARITH_RULE`SUC 0+a= a+1`]
THEN THAYTHEL_ASM_TAC 0[`k-1`][ITER;I_DEF;ARITH_RULE`SUC 0+a= a+1`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`vv`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`p1`;`vv`]
THEN MP_TAC Odxlstcv2.CARD_V_EQ_SCS_K1
THEN RESA_TAC
THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
THEN RESA_TAC
THEN THAYTHES_TAC 0[`vv p1`][WL_IN_V;ARITH_RULE`k-1+a=a+k-1`]);;


let BB_F_SUC_PRE=
prove(`is_scs_v39 s /\ BBs_v39 s f ==> f (SUC (i + (scs_k_v39 s) - 1)) = f i`,

STRIP_TAC
THEN MATCH_MP_TAC Oxlzlez.F_SUC_PRE
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;is_scs_v39]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DICH_TAC (23-1)
THEN ARITH_TAC);;

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




let RRCWNSJ = prove_by_refinement(
 RRCWNSJ_concl,
[
STRIP_TAC
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 REPEAT RESA_TAC
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 MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
THEN RESA_TAC
THEN MRESA_TAC LUNAR_IN_V[`E`;`v'`;`w`;`V`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC "V"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN DICH_TAC 5
THEN RESA_TAC
THEN MRESA_TAC Axjrpnc.AXJRPNC[`s`;`v`;`x`;`x'`]
THEN DICH_TAC 1
THEN STRIP_TAC
THEN POP_ASSUM(fun  th->ASSUME_TAC (SYM th))
THEN MP_TAC B_LE_2h0_A_EQ2_IN_CASES_6
THEN RESA_TAC
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`]
THEN THAYTHEL_ASM_TAC 0[`x`][]
THEN THAYTHE_TAC 0[`SUC x`]
THEN SUBGOAL_THEN`norm((v:num->real^3) (SUC x))= &2 \/ norm (v x- v (SUC x))= &2` ASSUME_TAC;

MP_TAC(REAL_ARITH`&2 <= norm (v x - v (SUC x))
/\ &2 <= norm (v (SUC x) - v (SUC (SUC x)))
==> (&2 < norm (v x - v (SUC x))
/\ &2 < norm (v (SUC x) - v (SUC (SUC x))))\/  norm (v x - v (SUC x))= &2
\/  (norm ((v:num->real^3) (SUC x) - v (SUC (SUC x)))= &2) `)
THEN RESA_TAC;

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


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


MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`x:num`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[dist]
THEN THAYTHE_TAC (33-26)[`x`]
THEN DICH_TAC (34-28)
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x`;`i `;`s:scs_v39`;`SUC x`;`x`][is_scs_v39]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC;



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



MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`SUC(SUC x):num`]
THEN THAYTHEL_TAC (34-26)[`SUC(x)`][dist]
THEN DICH_TAC (35-29)
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x`;`i`;`s:scs_v39`;`SUC x`;`SUC(SUC x)`][is_scs_v39]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC;



MP_TAC(ARITH_RULE`~(6=0)`)
THEN RESA_TAC
THEN THAYTHES_TAC (34-9)[`i`;`SUC x`][scs_diag;ADD1;ARITH_RULE`~(6=0)/\ i+1=1+i`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;


MRESA_TAC J_EMPY_CASES_6[`s`;`SUC x`]
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
THEN STRIP_TAC
THEN MRESAL_TAC ODXLSTCv2[`s`;`k`;`v`;`SUC x`][DE_MORGAN_THM;]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC x)) V' E'`
ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC (35-23)
THEN RESA_TAC
THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
THEN REPLICATE_TAC (49-36) (REMOVE_ASSUM_TAC)
THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
THEN RESA_TAC
THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (SUC x)`;`v1`][LET_DEF;LET_END_DEF;]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
THEN ASM_REWRITE_TAC[ADD1]
THEN MP_TAC PI_WORKS
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
;


MP_TAC(REAL_ARITH`norm (v (SUC x)) = &2 \/ ~(norm ((v:num->real^3) (SUC x)) = &2)`)
THEN RESA_TAC
THEN MRESA_TAC J_EMPY_CASES_6[`s`;`SUC x`]
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC x)) V' E'`
ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC (34-23)
THEN RESA_TAC
THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
THEN RESA_TAC
THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (SUC x)`;`v1`][LET_DEF;LET_END_DEF;]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
THEN ASM_REWRITE_TAC[ADD1]
THEN MP_TAC PI_WORKS
THEN REAL_ARITH_TAC;


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

GEN_TAC
THEN STRIP_TAC
THEN THAYTHE_TAC (33-9)[`SUC x`;`i`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC
;




SUBGOAL_THEN`azim (vec 0) (v (SUC x)) (v (SUC (SUC x))) ((v:num->real^3) (SUC x + k - 1)) = pi`ASSUME_TAC
;


DICH_TAC (33-23)
THEN RESA_TAC
THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
THEN RESA_TAC
THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT;interior_angle1;GSYM ivs_rho_node1]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+1)`;`v`;`x+1`;`k`];


SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) (SUC (SUC x)), v (SUC x + k - 1)}`
ASSUME_TAC
;


DICH_TAC (34-23)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(2 MOD 6= 3 MOD 6)/\ ~(2 MOD 6= 0 MOD 6)`)
THEN RESA_TAC
THEN MRESA_TAC Lunar_deform.LOCAL_CONVEX_NOT_COLLINEAR[`FF`;`E`;`V`;`w`;`v'`]
THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`SUC i+k-1=SUC(i+k-1)`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN MATCH_DICH_TAC 1
THEN MRESAS_TAC WL_IN_V[`SUC (SUC x)`;`v:num->real^3`][BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC x)=x+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT];





SUBGOAL_THEN`(v:num->real^3) (SUC x) IN aff_gt {vec 0} {v (SUC (SUC x)), v (SUC x + k - 1)}`
ASSUME_TAC;


DICH_TAC (35-23)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(2 MOD 6= 1 MOD 6)/\ ~(2 MOD 6= 0 MOD 6)/\ ~(6<=3)/\ 3 MOD 6=3`)
THEN RESA_TAC
THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k`]
THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v x`;`v`;`x`]
THEN MRESAS_TAC Local_lemmas.LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT[`E`;`V`;`w`;`FF`;`v'`][BB_VV_FUN_EQ]
THEN DICH_TAC 1
THEN ASM_SIMP_TAC[BB_VV_FUN_EQ;]
THEN ONCE_REWRITE_TAC[ARITH_RULE`i+x=x+i:num`]
THEN REWRITE_TAC[ARITH_RULE`3+x=x+3`]
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN DICH_TAC 1
THEN MRESAL_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;` FF`;`v x`;`v`;`x`;`k`][ARITH_RULE`0< l/\ l<3<=> l=1\/ l=2`;SET_RULE`{v (l + x) | l = 1 \/ l = 2} = {v (1+x), v(2+x)}`;SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;ARITH_RULE`2+x=x+2`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`v (x + 2) IN aff_gt {vec 0, v x} {v (x + 1)}
/\  aff_gt {vec 0, v x} {v (x + 1)} SUBSET aff_ge {vec 0, v x} {v (x + 1)}
==> v (x + 2) IN aff_ge {vec 0, (v:num->real^3) x} {v (x + 1)}`)
THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
THEN STRIP_TAC
THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`k-1+ SUC i=SUC(i+k-1)`]
THEN DICH_TAC(52-34)
THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`SUC i+k-1=SUC(i+k-1)/\ SUC (SUC x)= x+2`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`x`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`x+2`;`v:num->real^3`]
THEN MRESAL_TAC WL_IN_E[`x`;`v:num->real^3`][ADD1]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2[`E`;`V`;`FF`;`v x`]
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN MRESAL_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v x`;`v (x+1)`;`v (x+2)`][ADD1]
THEN MRESA_TAC th3[`vec 0:real^3`;`v x`;`v (x+2)`]
THEN MRESAS_TAC Planarity.POINT_IN_AFF_GE_IMP_IN_EDGE[`vec 0:real^3`;`V`;`E`;`v(x)`;`v (x+1)`;`v (x+2)`][SET_RULE`a IN{b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT;BB_VV_FUN_EQ]
;


MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
THEN GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x:num`]
THEN RESA_TAC
THEN DICH_TAC 1
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
;


MRESAL_TAC IMJXPHRv2[`s`;`k`;`v`;`SUC x`][dist]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE` SUC i+k-1=SUC(i+k-1)`]
THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1)= 1*6+x/\ ~(6=0)`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x:num`;`1*k+x `;`s:scs_v39`;`SUC x:num`;`(1*k+x) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x:num`;`x MOD k `;`s:scs_v39`;`SUC x:num`;`x:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
THEN STRIP_TAC
THEN REWRITE_TAC[GSYM dist]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN SYM_ASSUM_TAC 
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
;


(********CASES 2*****)



SUBGOAL_THEN`norm((v:num->real^3) (x+k-1))= &2 \/ norm (v (x+k-1)- v (x))= &2` ASSUME_TAC;

REPLICATE_TAC 3 REMOVE_ASSUM_TAC
THEN ASSUME_TAC(ARITH_RULE`(x + k - 1) + k - 1=x + k - 1 + k - 1`)
THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
THEN MRESAL_TAC BB_F_SUC_PRE[`s`;`v`;`x+k-1`][]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`]
THEN THAYTHEL_ASM_TAC 0[`x+k-1`][]
THEN THAYTHE_TAC 0[`x+ k-1+k-1`]
THEN MP_TAC(REAL_ARITH`&2 <= norm (v (x+k-1) - v (x))
/\ &2 <= norm (v (x+k-1+k-1) - v (x+k-1))
==> (&2 < norm (v (x+k-1) - v (x))
/\ &2 < norm (v (x+k-1+k-1) - v (x+k-1)))\/  norm (v (x+k-1) - v (x))= &2
\/  (norm ((v:num->real^3) (x+k-1+k-1) - v (x+k-1))= &2) `)
THEN RESA_TAC;

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


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


MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`x:num`]
THEN THAYTHE_TAC (36-26)[`x+k-1`]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1)= 1*6+x/\ ~(6=0)`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1:num`;`1*k+x `;`s:scs_v39`;` x+k-1:num`;`(1*k+x) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1:num`;`x MOD k `;`s:scs_v39`;` x+k-1:num`;`x:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1`;`i `;`s:scs_v39`;` x+k-1`;`x`][is_scs_v39;dist]
THEN RESA_TAC
THEN DICH_TAC (42-31)
;

MP_TAC(SET_RULE`i MOD k= (x+k-1+k-1) MOD k\/ ~(i MOD k= (x+k-1+k-1) MOD k)`)
THEN RESA_TAC;



MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`(x+k-1+k-1):num`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN THAYTHEL_TAC (37-26)[`x+k-1+k-1`][dist]
THEN DICH_TAC 0
THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1+ 6 - 1)= 1*6+(x+ 6 - 1)/\ ~(6=0)`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1+k-1:num`;`1*k+(x+k-1) `;`s:scs_v39`;` x+k-1+k-1:num`;`(1*k+(x+k-1)) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1+k-1:num`;`(x+k-1) MOD k `;`s:scs_v39`;` x+k-1+k-1:num`;`x+k-1:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1`;`i `;`s:scs_v39`;` x+k-1`;`x+k-1+k-1`][is_scs_v39;dist]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC;



MP_TAC(ARITH_RULE`~(6=0)/\  1+(x + 6- 1)= 1*6+x`)
THEN RESA_TAC
THEN THAYTHES_TAC (38-9)[`i`;`x+k-1`][scs_diag;ADD1;ARITH_RULE`~(6=0)/\ i+1=1+i`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_MULT_ADD]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DICH_TAC 0
THEN MP_TAC(ARITH_RULE`x+6-1=1+(x+6-2)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
THEN DICH_TAC 3
THEN MP_TAC(ARITH_RULE`x+6-1+6-1=1*6+(x+6-2)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;


MRESA_TAC J_EMPY_CASES_6[`s`;`x+k-1`]
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
THEN STRIP_TAC
THEN MRESAL_TAC ODXLSTCv2[`s`;`k`;`v`;`x+k-1`][DE_MORGAN_THM;]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (x+k-1)) V' E'`
ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC (38-23)
THEN RESA_TAC
THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
THEN REPLICATE_TAC (52-39) (REMOVE_ASSUM_TAC)
THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
THEN RESA_TAC
THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (x+k-1)`;`v1`][LET_DEF;LET_END_DEF;]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
THEN ASM_REWRITE_TAC[ADD1]
THEN MP_TAC PI_WORKS
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
;


MP_TAC(REAL_ARITH`norm (v (x+k-1)) = &2 \/ ~(norm ((v:num->real^3) (x+k-1)) = &2)`)
THEN RESA_TAC
THEN MRESA_TAC J_EMPY_CASES_6[`s`;`x+k-1`]
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (x+k-1)) V' E'`
ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC (37-23)
THEN RESA_TAC
THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
THEN RESA_TAC
THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (x+k-1)`;`v1`][LET_DEF;LET_END_DEF;]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
THEN ASM_REWRITE_TAC[ADD1]
THEN MP_TAC PI_WORKS
THEN REAL_ARITH_TAC;


SUBGOAL_THEN`(!i. scs_diag k (x+k-1) i
           ==> scs_a_v39 s (x+k-1) i < dist (v (x+k-1),(v:num->real^3) i))`ASSUME_TAC
;

GEN_TAC
THEN STRIP_TAC
THEN THAYTHE_TAC (36-9)[`x+k-1`;`i`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC
;




SUBGOAL_THEN`azim (vec 0) ((v:num->real^3) (x + k - 1)) (v x) (v (x + k - 1+k-1)) = pi`ASSUME_TAC
;


REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
THEN DICH_TAC 0
THEN DICH_TAC(33-23)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]
THEN ASSUME_TAC th)
THEN REWRITE_TAC[]
THEN STRIP_TAC
THEN REPLICATE_TAC (47-34) (REMOVE_ASSUM_TAC)
THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
THEN RESA_TAC
THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT;interior_angle1;GSYM ivs_rho_node1]
THEN MRESAL_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+k-1)`;`v`;`x+k-1`;`k`][ARITH_RULE`(x + k - 1) + 1= SUC (x + k - 1)`];



SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) x, v (x + k - 1 + k - 1)}`
ASSUME_TAC
;


DICH_TAC (37-23)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1+6-1) MOD 6= 3 MOD 6)/\ ~((6-1+6-1) MOD 6= 0 MOD 6)`)
THEN RESA_TAC
THEN MRESA_TAC Lunar_deform.LOCAL_CONVEX_NOT_COLLINEAR[`FF`;`E`;`V`;`w`;`v'`]
THEN MATCH_DICH_TAC 0
THEN MRESAS_TAC WL_IN_V[`x+k-1+k-1`;`v:num->real^3`][BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC x)=x+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT];




SUBGOAL_THEN`(v:num->real^3) (x + k - 1) IN aff_gt {vec 0} {v x, v (x + k - 1 + k - 1)}`
ASSUME_TAC;


DICH_TAC (38-23)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ (0 MOD 6= (3+3) MOD 6)/\ ~(1 MOD 6= 3 MOD 6)/\ ~(6<=3)/\ ~((3+1) MOD 6= (6-1) MOD 6)`)
THEN RESA_TAC
THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k`]
THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v (x+3)`;`v`;`x+3`]
THEN MRESA_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ[`V`;`E`;`w`;`FF`;`v'`]
THEN MRESAS_TAC Local_lemmas.LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT[`E`;`V`;`v'`;`FF`;`w`][BB_VV_FUN_EQ;Local_lemmas.LUNAR_COMM;]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN ASSUME_TAC(SYM th))
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v x`;`v`;`x`;`k`]
THEN DICH_TAC 2
THEN ASM_SIMP_TAC[BB_VV_FUN_EQ;]
THEN ONCE_REWRITE_TAC[ARITH_RULE`i+x+3=x+i+3:num`]
THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
THEN ONCE_REWRITE_TAC[ARITH_RULE`i+3=3+i:num`]
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0< l/\ l<3<=> l=1\/ l=2`;SET_RULE`{v (x + 3 + l) | l = 1 \/ l = 2} = {v (x+3+1), v(x+3+2)}`;SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;ARITH_RULE` 3+2=6-1`]
THEN MP_TAC(ARITH_RULE`x+6-1+6-1= 1*6+(x+3+1)`)
THEN RESA_TAC
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + x + 3 + 1`;`v:num->real^3`;`(1 * k + x + 3 + 1) MOD k:num`][MOD_REFL;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(x + 3 + 1) MOD k`;`v:num->real^3`;`(x + 3 + 1):num`][MOD_REFL;MOD_MULT_ADD]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`v (x + 3+1) IN aff_gt {vec 0, v x} {v (x +k- 1)}
/\  aff_gt {vec 0, v x} {v (x +k- 1)} SUBSET aff_ge {vec 0, v x} {v (x + k-1)}
==> v (x + 3+1) IN aff_ge {vec 0, (v:num->real^3) x} {v (x + k-1)}`)
THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
THEN STRIP_TAC
THEN DICH_TAC (59-37)
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`x+3+1`;`v:num->real^3`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+k-1)`;`v`;`x+k-1`;`k`]
THEN MRESAL_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2[`E`;`V`;`FF`;`v (x+k-1)`][GSYM ADD1]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN MRESAL_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v x`;`v (x+k-1)`;`v (x+3+1)`][ADD1]
THEN MRESAL_TAC WL_IN_E[`x+k-1`;`v:num->real^3`][]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN RESA_TAC
THEN MRESA_TAC th3[`vec 0:real^3`;`v x`;`v (x+3+1)`]
THEN MRESAS_TAC Planarity.POINT_IN_AFF_GE_IMP_IN_EDGE[`vec 0:real^3`;`V`;`E`;`v(x)`;`v (x+k-1)`;`v (x+3+1)`][SET_RULE`a IN{b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT;BB_VV_FUN_EQ];

MRESAL_TAC IMJXPHRv2[`s`;`k`;`v`;`x+k-1`][dist]
;


POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM dist]
THEN DISCH_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DISCH_TAC
;



MRESA_TAC BB_F_SUC_PRE[`s`;`v:num->real^3`;`x`]
THEN MP_TAC Axjrpnc.DIST_LE_2h0_IN_CASES_6
THEN RESA_TAC
THEN THAYTHEL_ASM_TAC 0[`x`][GSYM dist]
THEN THAYTHEL_TAC 0[`x+k-1`][GSYM dist]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC;

SUBGOAL_THEN`      cstab <= dist (v (SUC x),(v:num->real^3) (x + k - 1))`ASSUME_TAC
;

MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(1 MOD 6=6 MOD 6)/\ (x+6-1)+1=x+6/\ ~(1 MOD 6= (6-1) MOD 6)/\ ~(6=0)/\ ~((2) MOD 6= (6-1) MOD 6)`)
THEN RESA_TAC
THEN THAYTHES_TAC (41-10)[`SUC x`;`x+k-1`][scs_diag;ADD1;ARITH_RULE`(i+1)+1= i+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;


DICH_TAC (35-24)
THEN RESA_TAC
THEN MRESAL_TAC JKQEWGV3[`s`;`v`;`v'`;`w`][LET_DEF;LET_END_DEF;];


DICH_TAC 1
THEN STRIP_TAC 
THEN REMOVE_ASSUM_TAC
THEN MP_TAC SYNQIWN
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`v`;`x`;`k`]
THEN DICH_TAC 0
THEN DICH_TAC (35-30)
THEN DICH_TAC (34-29)
THEN RESA_TAC
THEN RESA_TAC
THEN DICH_TAC 2
THEN REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;ADD1]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x)`;`v`;`x`;`k`]
THEN REAL_ARITH_TAC;





]);;





 end;;


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