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


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


module Axjrpnc = 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 DIST_LE_2h0_IN_CASES_6=
prove(`scs_k_v39 s=6 /\ BBs_v39 s v /\ is_scs_v39 s 
==> !i. norm(v i- v (SUC i))<= &2 *h0`,

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 DICH_TAC (27-1)
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`]
THEN STRIP_TAC
THEN THAYTHEL_TAC 1[`i`;`SUC i`][dist]
THEN POP_ASSUM MP_TAC
THEN DICH_TAC(29-24)
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 REAL_ARITH_TAC]);;

let DIST_EDGE_IN_BB_LE_2=
prove(`BBs_v39 s v /\ is_scs_v39 s 
==> &2<= norm(v i- v (SUC i))`,

DISCH_TAC
THEN POP_ASSUM(fun th-> MP_TAC th
THEN ASSUME_TAC th)
THEN REWRITE_TAC[BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;]
THEN STRIP_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN THAYTHE_TAC (24-2)[`i`;`SUC i`]
THEN THAYTHE_TAC (25-17)[`i MOD k`;`SUC i MOD k`]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[DIVISION;Qknvmlb.SUC_MOD_NOT_EQ]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k `;`s:scs_v39`;`i:num`;`SUC i:num`][is_scs_v39;MOD_REFL;ARITH_RULE`~(6=0)`]
THEN DICH_TAC 4
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC);;


let arclength222h0 = 
prove_by_refinement(
  `arclength (&2) (&2) (&2 * h0) < pi / &2`,

  (* {{{ proof *)
  [
  GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1;
  CONJ_TAC;
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
    BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `x + y < x <=> y < &0`];
  ONCE_REWRITE_TAC[GSYM ATN_0];
  MATCH_MP_TAC ATN_MONO_LT;
  REWRITE_TAC[arith `(x / y < &0 <=> &0 < (-- x)/ y)`];
  GMATCH_SIMP_TAC REAL_LT_DIV;
  GMATCH_SIMP_TAC SQRT_POS_LT;
  REWRITE_TAC[Sphere.h0];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)




let is_scs_k_le_3=
prove(`is_scs_v39 s ==> 3<= scs_k_v39 s`,

REWRITE_TAC[BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC);;

let DIST_LE2_BB_CASSE_4= 
prove_by_refinement(`scs_k_v39 s=4 /\ BBs_v39 s v /\ is_scs_v39 s 
==> ?i. norm(v i- v (SUC i))<= &2 *h0`,

[
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 (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;

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;


REWRITE_TAC[ARITH_RULE`a+4<=6 <=> a<= 2`]
THEN SUBGOAL_THEN`{i | i < 4 /\
      (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}SUBSET 0..3` ASSUME_TAC;

ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;

STRIP_TAC
THEN MRESAL_TAC CARD_DIFF[`0..3`;`{i | i < 4 /\
      (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG;CARD_NUMSEG;]
THEN MP_TAC(ARITH_RULE`CARD
      {i | i < 4 /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} <=
      2 /\ CARD
      ((0..3) DIFF
       {i | i < 4 /\
            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}) =
      (3 + 1) -
      0 -
      CARD
      {i | i < 4 /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
==> 0 <CARD
      ((0..3) DIFF
       {i | i < 4 /\
            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))})`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN SYM_ASSUM_TAC
THEN MP_TAC(SET_RULE`(0..3) DIFF
  {i | i < 4 /\
       (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}= {}
\/ ~((0..3) DIFF
  {i | i < 4 /\
       (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} ={})`)
THEN RESA_TAC;

REWRITE_TAC[Oxl_2012.CARD_EMPTY]
THEN ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;DIFF;IN_ELIM_THM;IN_ELIM_THM;IN_NUMSEG]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`a<=3==> a<4`)
THEN RESA_TAC
THEN REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`]
THEN REPEAT RESA_TAC
THEN DICH_TAC (30-1)
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`]
THEN STRIP_TAC
THEN THAYTHEL_TAC 1[`a`;`SUC a`][dist]
THEN EXISTS_TAC`a:num`
THEN POP_ASSUM MP_TAC
THEN DICH_TAC (33-27)
THEN REAL_ARITH_TAC]);;


let NORM_V_IN_BB_LE_CSTAB=
prove(`  (!i. scs_b_v39 s i (SUC i) <= cstab) /\
  BBs_v39 s v 
==> !i. norm (v i- v (SUC i))<= cstab`,

REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;dist]
THEN RESA_TAC
THEN GEN_TAC
THEN THAYTHE_TAC 1[`i`;`SUC i`]
THEN THAYTHE_TAC 5[`i`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;


let arclength_2h0_cstab = 
prove_by_refinement(
  `arclength (&2) (&2) (&2 *h0) + arclength (&2) (&2) cstab < pi`,

  (* {{{ proof *)
  [
  REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
  REWRITE_TAC[GSYM CONJ_ASSOC];
  CONJ_TAC;
    BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
  CONJ_TAC;
    BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `(pi/ &2 + b) + (pi / &2 + d) < pi <=> b + d < &0`];
  REWRITE_TAC[Sphere.h0;Sphere.cstab];
  MP_TAC (Flyspeck_constants.calc `atn (((&2 *  #1.26) * &2 *  #1.26 -
&2 * &2 - &2 * &2) /  sqrt  ((&2 + &2 + &2 *  #1.26) *   (&2 + &2 - &2
*  #1.26) *   (&2 + &2 *  #1.26 - &2) *   (&2 *  #1.26 + &2 - &2))) +
atn (( #3.01 *  #3.01 - &2 * &2 - &2 * &2) /  sqrt  ((&2 + &2 +
#3.01) *   (&2 + &2 -  #3.01) *   (&2 +  #3.01 - &2) *   ( #3.01 + &2
-  &2))) < &0`);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)





let DIST_LE2_BB_CASSE_5 = 
prove_by_refinement(
`scs_k_v39 s=5 /\ BBs_v39 s v /\ is_scs_v39 s 
==> norm(v i- v (SUC i))<= &2 *h0 \/ norm(v (SUC i)- v (SUC (SUC i)))<= &2 *h0 `,

[
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 (0)
THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
THEN SUBGOAL_THEN`FINITE
      {i | i < 5 /\
           (&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..5`
THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;

REWRITE_TAC[ARITH_RULE`a+5<=6 <=> a<= 1`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`norm (v i - v (SUC i)) <= &2 * h0 \/
     norm (v (SUC i) - (v:num->real^3) (SUC (SUC i))) <= &2 * h0 \/ ~(norm (v i - v (SUC i)) <= &2 * h0 \/
     norm (v (SUC i) - v (SUC (SUC i))) <= &2 * h0)`)
THEN RESA_TAC;

DICH_TAC 1
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b) <=> b<a`]
THEN STRIP_TAC
THEN DICH_TAC (24-1)
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`]
THEN STRIP_TAC
THEN DICH_TAC 1
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i`;`SUC i`][dist] THEN MRESAL_TAC th[`SUC i`;`SUC (SUC i)`][dist])
THEN MP_TAC(REAL_ARITH`&2 * h0 < norm (v i - v (SUC i)) /\  norm (v i - v (SUC i))<= scs_b_v39 s i (SUC i) /\  &2 * h0 < norm (v (SUC i) - v (SUC (SUC i))) /\  norm ((v:num->real^3) (SUC i) - v (SUC (SUC i)))<= scs_b_v39 s (SUC i) (SUC (SUC i))
==> &2 * h0< scs_b_v39 s (SUC i) (SUC (SUC i)) /\ &2 * h0< scs_b_v39 s (i) (SUC (i))`)
THEN RESA_TAC
THEN SUBGOAL_THEN`{i MOD 5,SUC i MOD 5} SUBSET {i | i < 5 /\
        (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;

REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {c,b}<=> a= c\/ a= b`]
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];

MRESAL_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD 5:num`;`SUC (i MOD 5) `;`s:scs_v39`;`i:num`;`SUC (i MOD 5) MOD 5:num`][is_scs_v39]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i:num`;`SUC i MOD 5 `;`s:scs_v39`;`i:num`;`SUC i:num`][is_scs_v39]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
THEN RESA_TAC;

ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];

MRESAL_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(SUC i) MOD 5:num`;`SUC ((SUC i) MOD 5) `;`s:scs_v39`;`(SUC i):num`;`SUC ((SUC i) MOD 5) MOD 5:num`][is_scs_v39]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(SUC i):num`;`SUC (SUC i) MOD 5 `;`s:scs_v39`;`(SUC i):num`;`SUC (SUC i):num`][is_scs_v39]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
THEN RESA_TAC;

MRESA_TAC Hypermap.CARD_TWO_ELEMENTS[`i MOD 5`;`SUC i MOD 5`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
THEN STRIP_TAC
THEN MRESA_TAC CARD_SUBSET[`{i MOD 5, SUC i MOD 5}`;`
      {i | i < 5 /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC]);;


let AXJRPNC_concl = `!s (v:num->real^3) i j.
  is_scs_v39 s /\ scs_basic_v39 s /\
  (!i. scs_b_v39 s i (SUC i) <= cstab) /\
  MMs_v39 s v /\
  (lunar (v i,v j) (IMAGE v (:num))
     (IMAGE (\i. {v i, v (SUC i)}) (:num))   ) ==>
  (scs_k_v39 s = 6 /\ v j = v (i + 3))`;;



let  AXJRPNC = prove_by_refinement(
 AXJRPNC_concl,
[
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 Qknvmlb.SCS_K_LE_6
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`k<=6==> k=6\/ k<6`)
THEN RESA_TAC;


MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MP_TAC DIST_LE_2h0_IN_CASES_6
THEN RESA_TAC;


MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<6`]
THEN ASSUME_TAC(ARITH_RULE`3<6/\ ~(6<=3)`)
THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`v:num->real^3`;`IMAGE (v:num->real^3) (:num)`;`k:num`]
THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`]
THEN DICH_TAC(20-16)
THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`]
THEN MP_TAC(ARITH_RULE`i'+1<6/\ ~(i'=0)/\ ~(i'=1)==> i'=2\/ i'=4\/ i'=3`)
THEN RESA_TAC;


STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC
THEN MP_TAC th
THEN REPEAT RESA_TAC)
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v i) (v (SUC i)) <= arclength (&2) (&2) (&2 * h0)
/\ arcV (vec 0) ((v:num->real^3) (SUC i)) (v (SUC (SUC i))) <=
      arclength (&2) (&2) (&2 * h0)
/\ arclength (&2) (&2) (&2 * h0)< pi/ &2
==>arcV (vec 0) (v (i)) (v ((SUC i)))+ arcV (vec 0) (v (SUC i)) (v (SUC (SUC i))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength222h0]
THEN STRIP_TAC
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_FF[`i`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC i`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v i, v (SUC i)`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC i), v (SUC (SUC i))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v i`;`v (SUC(SUC i))`;`v (SUC i)`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(2+i)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`2+i= SUC(SUC i)`;]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (SUC (SUC i))}`];




STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC
THEN MP_TAC th
THEN REPEAT RESA_TAC)
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`4+i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (4+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (4+i))`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(4+i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (4+i)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (4+i)`;`v (SUC (4+i))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (4+i))`;`v (SUC(SUC (4+i)))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (4+i)) (v (SUC (4+i))) <= arclength (&2) (&2) (&2 * h0)
/\ arcV (vec 0) ((v:num->real^3) (SUC (4+i))) (v (SUC (SUC (4+i)))) <=
      arclength (&2) (&2) (&2 * h0)
/\ arclength (&2) (&2) (&2 * h0)< pi/ &2
==>arcV (vec 0) (v ((4+i))) (v ((SUC (4+i))))+ arcV (vec 0) (v (SUC (4+i))) (v (SUC (SUC (4+i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength222h0]
THEN STRIP_TAC
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_FF[`(4+i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (4+i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (4+i), v (SUC (4+i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (4+i)), v (SUC (SUC (4+i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (4+i)`;`v (SUC(SUC (4+i)))`;`v (SUC (4+i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(4+i))= 1*6+i`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*6+i):num`;`v:num->real^3`;`(1*6+i) MOD k`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(6=0)`]
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`6`;`i`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(6=0)`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(4+i)`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ARITH_RULE`2+i= SUC(SUC i)`;]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (4+i)}`]
;

ONCE_REWRITE_TAC[ARITH_RULE`3+i=i+3`]
THEN REWRITE_TAC[];



MP_TAC is_scs_k_le_3
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k/\ k<6==> k=3\/ (3<k/\ k=4)\/ (3<k/\ k=5)`)
THEN RESA_TAC;



MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAL_TAC Jkqewgv.IS_SCS_NOT_COLLINEAR_BBs_CASE_3[`s`;`v`][IN]
THEN DICH_TAC 8
THEN REWRITE_TAC[lunar]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`i:num`;`v:num->real^3`;`i MOD k`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(3=0)`]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`j:num`;`v:num->real^3`;`j MOD k`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(3=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`i MOD 3< 3==> i MOD 3= 0\/ i MOD 3= 1\/ i MOD 3=2`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(3=0)`]
THEN RESA_TAC 
THEN MP_TAC(ARITH_RULE`j MOD 3< 3==> j MOD 3= 0\/ j MOD 3= 1\/ j MOD 3=2`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(3=0)`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C} ={A,C,B}`]
THEN ASM_REWRITE_TAC[]
;





MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<6`]
THEN ASSUME_TAC(ARITH_RULE`3<4/\ ~(4<=3)`)
THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`v:num->real^3`;`IMAGE (v:num->real^3) (:num)`;`k:num`]
THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`]
THEN DICH_TAC(22-18)
THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`]
THEN MP_TAC(ARITH_RULE`i'+1<4/\ ~(i'=0)/\ ~(i'=1)==> i'=2`)
THEN RESA_TAC;




MP_TAC DIST_LE2_BB_CASSE_4
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`i`;`v`]
THEN MRESA_TAC Localization.LOFA_IMP_LT_CARD_SET_V_ALT[`V`;`E`;`FF`;`v i`]
THEN MRESA_TAC WL_IN_V[`i''`;`v`]
THEN POP_ASSUM MP_TAC
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN RESA_TAC
THEN MRESA_TAC Nuxcoea.W_IN_BB_FUN_EQ[`v:num->real^3`;`i'':num`;`n+i:num`;`s`]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i''`;`n+i:num`;`k`][ARITH_RULE`~(4=0)`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`SUC i'':num`;`v:num->real^3`;`SUC (n+i)`]
THEN MP_TAC(ARITH_RULE`n<4==> n=0\/ n=1\/ n=2\/ n=3`)
THEN RESA_TAC;





REWRITE_TAC[ARITH_RULE`0+a=a`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`SUC i`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (&2 * h0)
/\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
      arclength (&2) (&2) (cstab)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
;





REWRITE_TAC[ARITH_RULE`1+a=SUC a`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (cstab)
/\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
       arclength (&2) (&2) (&2 * h0)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
;



REWRITE_TAC[ARITH_RULE`0+a=a`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+i))`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+i)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+i)`;`v (SUC (2+i))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`SUC (2+i)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+i))`;`v (SUC(SUC (2+i)))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (2+i)) (v (SUC (2+i))) <= arclength (&2) (&2) (&2 * h0)
/\ arcV (vec 0) ((v:num->real^3) (SUC (2+i))) (v (SUC (SUC (2+i)))) <=
      arclength (&2) (&2) (cstab)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((2+i))) (v ((SUC (2+i))))+ arcV (vec 0) (v (SUC (2+i))) (v (SUC (SUC (2+i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(2+i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (2+i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (2+i), v (SUC (2+i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (2+i)), v (SUC (SUC (2+i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (2+i)`;`v (SUC(SUC (2+i)))`;`v (SUC (2+i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
THEN DICH_TAC 3
THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*4+i):num`;`v:num->real^3`;`(1*4+i) MOD k`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`4`;`i`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC;




REWRITE_TAC[ARITH_RULE`3+i=SUC(2+i)`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+i))`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+i)`]
THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`(2+i)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+i)`;`v (SUC (2+i))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+i))`;`v (SUC(SUC (2+i)))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (2+i)) (v (SUC (2+i))) <= arclength (&2) (&2) (cstab)
/\ arcV (vec 0) ((v:num->real^3) (SUC (2+i))) (v (SUC (SUC (2+i)))) <=
      arclength (&2) (&2) (&2 * h0)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((2+i))) (v ((SUC (2+i))))+ arcV (vec 0) (v (SUC (2+i))) (v (SUC (SUC (2+i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(2+i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (2+i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (2+i), v (SUC (2+i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (2+i)), v (SUC (SUC (2+i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (2+i)`;`v (SUC(SUC (2+i)))`;`v (SUC (2+i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
THEN DICH_TAC 3
THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*4+i):num`;`v:num->real^3`;`(1*4+i) MOD k`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`4`;`i`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC;






MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<5`]
THEN ASSUME_TAC(ARITH_RULE`3<5/\ ~(5<=3)`)
THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`v:num->real^3`;`IMAGE (v:num->real^3) (:num)`;`k:num`]
THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`]
THEN DICH_TAC(22-18)
THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`]
THEN MP_TAC(ARITH_RULE`i'+1<5/\ ~(i'=0)/\ ~(i'=1)==> i'=2\/ i'=3`)
THEN RESA_TAC;




MP_TAC DIST_LE2_BB_CASSE_5
THEN RESA_TAC
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
;






REWRITE_TAC[ARITH_RULE`0+a=a`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`SUC i`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (&2 * h0)
/\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
      arclength (&2) (&2) (cstab)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
;






REWRITE_TAC[ARITH_RULE`1+a=SUC a`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (cstab)
/\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
       arclength (&2) (&2) (&2 * h0)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
;






MRESA_TAC DIST_LE2_BB_CASSE_5[`s`;`v`;`3+i`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
;





REWRITE_TAC[ARITH_RULE`0+a=a`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(3+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (3+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (3+i))`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(3+i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (3+i)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (3+i)`;`v (SUC (3+i))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`SUC (3+i)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (3+i))`;`v (SUC(SUC (3+i)))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (3+i)) (v (SUC (3+i))) <= arclength (&2) (&2) (&2 * h0)
/\ arcV (vec 0) ((v:num->real^3) (SUC (3+i))) (v (SUC (SUC (3+i)))) <=
      arclength (&2) (&2) (cstab)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((3+i))) (v ((SUC (3+i))))+ arcV (vec 0) (v (SUC (3+i))) (v (SUC (SUC (3+i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(3+i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (3+i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (3+i), v (SUC (3+i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (3+i)), v (SUC (SUC (3+i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (3+i)`;`v (SUC(SUC (3+i)))`;`v (SUC (3+i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(3+i))= 1*5+i`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (3+i)}`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*5+i):num`;`v:num->real^3`;`(1*5+i) MOD k`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN DICH_TAC 5
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC;




REWRITE_TAC[ARITH_RULE`0+a=a`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(3+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (3+i)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (3+i))`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(3+i)`]
THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (3+i)`]
THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`(3+i)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (3+i)`;`v (SUC (3+i))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (3+i))`;`v (SUC(SUC (3+i)))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (3+i)) (v (SUC (3+i))) <= arclength (&2) (&2)  (cstab)
/\ arcV (vec 0) ((v:num->real^3) (SUC (3+i))) (v (SUC (SUC (3+i)))) <=
      arclength (&2) (&2) (&2 * h0)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((3+i))) (v ((SUC (3+i))))+ arcV (vec 0) (v (SUC (3+i))) (v (SUC (SUC (3+i)))) 
 < pi`)
THEN ASM_SIMP_TAC[arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(3+i)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (3+i)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (3+i), v (SUC (3+i))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (3+i)), v (SUC (SUC (3+i)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (3+i)`;`v (SUC(SUC (3+i)))`;`v (SUC (3+i))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(3+i))= 1*5+i`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (3+i)}`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*5+i):num`;`v:num->real^3`;`(1*5+i) MOD k`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN DICH_TAC 5
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC;


]);;


 end;;


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