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


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


module Vasyyau = 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 Aursipd;;
open Cuxvzoz;;
open Rrcwnsj;;
open Tfitskc;;
open Hexagons;;
open Otmtotj;;
open Hijqaha;;
open Cnicgsf;;
open Ardbzye;;
open Aueaheh;;


let WGDHPPI= prove(`!s v.
    is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==>
    CARD { i | i < scs_k_v39 s /\ scs_is_str s v i} <= 1`,
REPEAT RESA_TAC
THEN MRESA_TAC GSXRFWM[`s`;`v`]
THEN MRESAL_TAC Aursipd.AURSIPD[`s`;`v`][ARITH_RULE`3<4`]
THEN DICH_TAC 0
THEN ARITH_TAC);;

(************************************)

let DIST_V_IN_BB_LE_C=prove(`   scs_b_v39 s i (SUC i) <= c/\
  BBs_v39 s v 
==> dist (v i, v (SUC i))<= c`,
REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;dist]
THEN RESA_TAC
THEN THAYTHE_TAC 1[`i`;`SUC i`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;


let arclength_lt_1553 = prove_by_refinement(
  `&2 * arclength (&2) (&2) (&2 * h0) < arclength (&2) (&2)
(sqrt(#15.53))`,
  (* {{{ proof *)
  [
  REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
  GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
  REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
  REWRITE_TAC[arith `x + &2 - &2 = x`];
  REWRITE_TAC[Sphere.h0];
  TYPIFY `#3.9 < sqrt (#15.53) /\ sqrt(#15.53) < #3.95` (C
SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC REAL_LT_RSQRT;
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    MATCH_MP_TAC REAL_LT_LSQRT;
    BY(REAL_ARITH_TAC);
  TYPIFY_GOAL_THEN `&0 < &2 + &2 *  #1.26 - &2 /\  &0 < &2 + &2 - &2 *
 #1.26 /\ &0 < &2 + &2 + &2 *  #1.26 /\ &0 < &2 + sqrt  #15.53 - &2 /\
&0 < &2 + &2 - sqrt  #15.53 /\ &0 < &2 + &2 + sqrt  #15.53 /\ &0 <
sqrt  #15.53 /\ &0 < &2 *  #1.26` (unlist REWRITE_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  MP_TAC (Flyspeck_constants.calc `&2 * (pi / &2 +  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))) < pi / &2 + atn ((sqrt  #15.53 * sqrt  #15.53 - &2
* &2 - &2 * &2) /  sqrt  ((&2 + &2 + sqrt  #15.53) *   (&2 + &2 - sqrt
 #15.53) *   (&2 + sqrt  #15.53 - &2) *   sqrt  #15.53))` );
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)


  let ASSWPOW= prove_by_refinement( `!s v i. 
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
    scs_b_v39 s i (i+1) <= &2 * h0 /\  scs_b_v39 s (i+1) (i+2) <= &2 * h0
    ==>    xrr (norm (v i)) (norm(v(i+2))) (dist(v i,v(i+2))) <= #15.53 `,
[
REWRITE_TAC[IN;GSYM ADD1;ARITH_RULE`i+2=SUC(SUC i)`]
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 ASSUME_TAC(ARITH_RULE`3<4`)
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;

  



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 Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
THEN MRESAL_TAC DIST_V_IN_BB_LE_C[`s`;`v`;`i`;`&2*h0`][dist]
THEN MRESAL_TAC DIST_V_IN_BB_LE_C[`s`;`v`;`SUC i`;`&2*h0`][dist]
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 DICH_TAC (26-18)
THEN DICH_TAC (25-18)
THEN DICH_TAC (24-18)
THEN REWRITE_TAC[Ckqowsa_3_points.in_ball_annulus]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC Trigonometry2.ARCV_INEQUALTY[`vec 0:real^3`;`v i`;`v (SUC (SUC i))`;`v(SUC i)`]
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)
/\ &2 * arclength (&2) (&2) (&2 * h0) < arclength (&2) (&2)
(sqrt(#15.53))
/\ arcV (vec 0) (v i) (v (SUC (SUC i))) <=
      arcV (vec 0) (v i) (v (SUC i)) +
      arcV (vec 0) (v (SUC i)) (v (SUC (SUC i)))
==>arcV (vec 0) (v i) (v (SUC (SUC i))) 
 < arclength (&2) (&2)
(sqrt(#15.53))`)
THEN ASM_SIMP_TAC[arclength_lt_1553]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESAS_TAC Planarity.IMP_NORM_FAN[`v (i+0)`;`v(i+2):real^3`][VECTOR_ARITH`A- vec 0=A:real^3`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 2 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESA_TAC WL_IN_V[`i+0`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`i+2`;`v:num->real^3`]
THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (i+0)`;`v (i+2)`;`V`]
THEN THAYTHES_TAC 0[`v (i+0)`;`v (i+2)`][SET_RULE`a IN {a,b}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 2 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN ASM_TAC
THEN REWRITE_TAC[ARITH_RULE`i+0=i/\ i+2=SUC(SUC i)`]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`u=(v:num->real^3) i`
THEN ABBREV_TAC`w=(v:num->real^3) (SUC (SUC i))`
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
THEN MRESAL_TAC Collect_geom2.NOT_COL_EQ_UPS_X_POS[`vec 0:real^3`;`u`;`w`][dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
THEN MRESAL_TAC arclength_xrr[`norm (u)`;`norm w`;`norm (u-w)`][REAL_ARITH`a*a= a pow 2`]
THEN MRESA_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`u`;`w`]
THEN DICH_TAC (62-45)
THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
THEN MRESAL_TAC arclength_xrr[`&2`;`&2`;`sqrt #15.53`][REAL_ARITH`a*a= a pow 2/\ &0< &2`]
THEN DICH_TAC 0;





  TYPIFY `#3.9 < sqrt (#15.53) /\ sqrt(#15.53) < #3.95` (C
SUBGOAL_THEN ASSUME_TAC);

    GMATCH_SIMP_TAC REAL_LT_RSQRT;
    CONJ_TAC;
      BY(REAL_ARITH_TAC);

    MATCH_MP_TAC REAL_LT_LSQRT;

    BY(REAL_ARITH_TAC);

  TYPIFY_GOAL_THEN `&0 < &2 + &2 *  #1.26 - &2 /\  &0 < &2 + &2 - &2 *
 #1.26 /\ &0 < &2 + &2 + &2 *  #1.26 /\ &0 < &2 + sqrt  #15.53 - &2 /\
&0 < &2 + &2 - sqrt  #15.53 /\ &0 < &2 + &2 + sqrt  #15.53 /\ &0 <
sqrt  #15.53 /\ &0 < &2 *  #1.26` (unlist REWRITE_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
MP_TAC(REAL_ARITH`#3.9 < sqrt #15.53==> &0 < sqrt #15.53`)
THEN RESA_TAC
THEN MRESAL_TAC SQRT_POW2[`#15.53`][REAL_ARITH`&0<= #15.53`]
THEN REWRITE_TAC[ups_x;REAL_ARITH`&0 <
  --(&2 pow 2) * &2 pow 2 - &2 pow 2 * &2 pow 2 - #15.53 * #15.53 +
  &2 * &2 pow 2 * #15.53 +
  &2 * &2 pow 2 * &2 pow 2 +
  &2 * &2 pow 2 * #15.53`]
THEN RESA_TAC
THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`norm u`;`norm w`;`norm (u-w)`][REAL_ARITH`a*a= a pow 2`]
THEN MP_TAC(REAL_ARITH`&0 < xrr (norm u) (norm w) (norm (u-w))/\
xrr (norm u) (norm w) (norm (u-w)) < &16
==> abs (&1 - xrr (norm u) (norm w) (norm (u-w:real^3)) / &8) <= &1`)
THEN RESA_TAC
THEN SUBGOAL_THEN`abs (&1 - xrr (&2) (&2) (sqrt #15.53) / &8) <= &1`ASSUME_TAC
;



ASM_REWRITE_TAC[xrr;REAL_ARITH`a*a= a pow 2`]
THEN REAL_ARITH_TAC;


MRESAL_TAC ACS_MONO_LT_EQ[`&1 - xrr (norm u) (norm w) (norm (u-w)) / &8`;`&1 - xrr (&2) (&2) (sqrt #15.53) / &8`][REAL_ARITH`&1- a/ &8< &1- b/ &8<=> b<a`]
THEN MATCH_MP_TAC(REAL_ARITH`a<=b==>(c<a==>c<=b)`)
;



ASM_REWRITE_TAC[xrr;REAL_ARITH`a*a= a pow 2`]
THEN REAL_ARITH_TAC;

]);;





let YEBWJNG=  prove_by_refinement(
 `main_nonlinear_terminal_v11 ==> 
  (!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ 
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ scs_a_v39 s p (p+1) = &2 
    ==> dist(v p,v(p+1)) = &2)`,
[
REWRITE_TAC[IN;scs_is_str]
THEN REPEAT RESA_TAC
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 ASM_TAC
THEN REPEAT RESA_TAC
THEN MP_TAC Cuxvzoz.CUXVZOZ
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`s:scs_v39`
THEN EXISTS_TAC`FF:real^3#real^3->bool`
THEN EXISTS_TAC`4`
THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
THEN ASM_SIMP_TAC[]
THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MP_TAC SCS_DIAG_A_LE_DIST
THEN RESA_TAC
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v (p+4-1)`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) <= pi
/\ ~(azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) = pi)
==> azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) < pi`)
THEN RESA_TAC
THEN REWRITE_TAC[ADD1]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`p+1`;`4`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v (SUC p+4-1)`]
THEN DICH_TAC (31-8)
THEN REWRITE_TAC[GSYM ADD1]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) <= pi
/\ ~(azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) = pi)
==> azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) < pi`)
THEN RESA_TAC
THEN THAYTHES_TAC(32-26)[`1 * 4 + p`;`p`][MOD_MULT_ADD]
THEN MRESAL_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`p+3`][ARITH_RULE`SUC(i+3)=1*4+i/\ p+4-1=p+3`;GSYM dist]
THEN SUBGOAL_THEN`!i. scs_b_v39 s i (SUC(i)) <= cstab`ASSUME_TAC;

GEN_TAC
THEN THAYTHE_TAC (33-6)[`i`]
THEN DICH_TAC 0
THEN REWRITE_TAC[cstab;h0;ADD1]
THEN REAL_ARITH_TAC;

MP_TAC Axjrpnc.NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN REWRITE_TAC[GSYM dist]
THEN THAYTHES_TAC 0[`p+3`][ARITH_RULE`SUC(i+3)=1*4+i/\ p+4-1=p+3`;GSYM dist]
THEN ONCE_REWRITE_TAC[SET_RULE`A/\B<=> B/\A`]
THEN STRIP_TAC;

THAYTHE_TAC (35-6)[`p`];

DICH_TAC 0
THEN REWRITE_TAC[ADD1]
THEN REAL_ARITH_TAC;

DICH_TAC 1
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;

MRESA_TAC Ardbzye.SCS_DIAG_4_ADD2[`p`]
THEN THAYTHE_TAC (36-5)[`p+1`;`p+3`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DICH_TAC 1
THEN REWRITE_TAC[ADD1;cstab]
THEN REAL_ARITH_TAC]);;

(************************************)


let NOT_MOD_4_CASES=prove(`~(i MOD 4 = (p + 2) MOD 4)<=> i MOD 4 = p MOD 4\/  i MOD 4 = (p + 1) MOD 4
\/ i MOD 4 = (p + 3) MOD 4`,
MRESAL_TAC MOD_ADD_MOD[`p`;`1`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC MOD_ADD_MOD[`p`;`2`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC MOD_ADD_MOD[`p`;`3`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`p MOD 4<4==> p MOD 4=0\/ p MOD 4=1\/ p MOD 4=2\/ p MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN ARITH_TAC);;




let NOT_MOD_4_CASES_3=prove(`~(i MOD 4 = (p + 3) MOD 4)<=> i MOD 4 = p MOD 4\/  i MOD 4 = (p + 1) MOD 4
\/ i MOD 4 = (p + 2) MOD 4`,
MRESAL_TAC MOD_ADD_MOD[`p`;`1`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC MOD_ADD_MOD[`p`;`2`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC MOD_ADD_MOD[`p`;`3`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`p MOD 4<4==> p MOD 4=0\/ p MOD 4=1\/ p MOD 4=2\/ p MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN ARITH_TAC);;




let SCS_STR_CASES_4= prove_by_refinement(`!s v.
    is_scs_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v /\
    ~scs_is_str s v p /\ ~scs_is_str s v (p+1) 
==>  ~scs_is_str s v (p+3)\/  ~scs_is_str s v (p+2)`,
[
REPEAT RESA_TAC
THEN REWRITE_TAC[GSYM DE_MORGAN_THM]
THEN STRIP_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ (4-1) MOD 4= 4-1/\ 1<4`)
THEN MRESAL_TAC MMS_IMP_BBS[`s`;`v`][IN]
THEN SUBGOAL_THEN`(p +3) MOD 4 IN { i | i < scs_k_v39 s /\ scs_is_str s (v:num->real^3) i}`
ASSUME_TAC;

ASM_REWRITE_TAC[IN_ELIM_THM]
THEN ASM_TAC
THEN SIMP_TAC[scs_is_str;DIVISION;]
THEN REPEAT RESA_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3) MOD 4`;`p+3:num`][MOD_REFL]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`SUC((p+3) MOD 4)`;`SUC((p+3) MOD 4)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`SUC(p+3) MOD 4`;`SUC(p+3) `][MOD_REFL;Hypermap.lemma_suc_mod]
THEN MRESA_TAC MOD_ADD_MOD[`p+3`;`4-1`;`4`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p + 3) MOD 4 + 4 - 1`;`((p + 3) MOD 4 + 4 - 1)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`((p + 3) + 4 - 1) MOD 4`;`(p + 3)  + 4 - 1`][MOD_REFL;Hypermap.lemma_suc_mod];


SUBGOAL_THEN`(p +2) MOD 4 IN { i | i < scs_k_v39 s /\ scs_is_str s (v:num->real^3) i}`
ASSUME_TAC;

ASM_REWRITE_TAC[IN_ELIM_THM]
THEN ASM_TAC
THEN SIMP_TAC[scs_is_str;DIVISION;]
THEN REPEAT RESA_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+2) MOD 4`;`p+2:num`][MOD_REFL]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`SUC((p+2) MOD 4)`;`SUC((p+2) MOD 4)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`SUC(p+2) MOD 4`;`SUC(p+2) `][MOD_REFL;Hypermap.lemma_suc_mod]
THEN MRESA_TAC MOD_ADD_MOD[`p+2`;`4-1`;`4`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p + 2) MOD 4 + 4 - 1`;`((p + 2) MOD 4 + 4 - 1)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`((p + 2) + 4 - 1) MOD 4`;`(p + 2)  + 4 - 1`][MOD_REFL;Hypermap.lemma_suc_mod];

MP_TAC(SET_RULE`(p + 3) MOD 4 IN {i | i < scs_k_v39 s /\ scs_is_str s v i}/\
(p + 2) MOD 4 IN {i | i < scs_k_v39 s /\ scs_is_str s v i}
==> {(p + 3) MOD 4 ,(p + 2) MOD 4 } SUBSET {i | i < scs_k_v39 s /\ scs_is_str s v i}`)
THEN RESA_TAC
THEN MRESA_TAC Qknvmlb.SUC_MOD_NOT_EQ[`4`]
THEN DICH_TAC 1
THEN THAYTHEL_TAC 0[`p+2`][ARITH_RULE`SUC(p+2)=p+3`]
THEN MRESA_TAC Planarity.CARD_2_FAN[`(p + 3) MOD 4`;`(p + 2) MOD 4`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`FINITE {i | i < 4 /\ scs_is_str s v i}` ASSUME_TAC;

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

MRESA_TAC CARD_SUBSET[`{(p + 3) MOD 4, (p + 2) MOD 4}`;`{i | i < 4 /\ scs_is_str s v i}`]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC WGDHPPI[`s`;`v`][IN]
THEN DICH_TAC 0
THEN ARITH_TAC]);;




let NEHXMWH_concl=`main_nonlinear_terminal_v11 ==> 
  (!s FF v p.
  IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
  is_scs_v39 s /\
  scs_k_v39 s = 4 /\
  MMs_v39 s v /\
  scs_basic_v39 s /\
  scs_generic v /\
  (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4 * h0 < scs_b_v39 s i j) /\
  (!i. ~(i MOD 4 = (p+2) MOD 4)  ==> interior_angle1 (vec 0) FF (v i) < pi)
  ==> (dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1)))`;;

let NEHXMWH1_concl=`main_nonlinear_terminal_v11 ==> 
  (!s FF v p.
  IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
  is_scs_v39 s /\
  scs_k_v39 s = 4 /\
  MMs_v39 s v /\
  scs_basic_v39 s /\
  scs_generic v /\
  (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4 * h0 < scs_b_v39 s i j) /\
  (!i. ~(i MOD 4 = (p+3) MOD 4)  ==> interior_angle1 (vec 0) FF (v i) < pi)
  ==> (dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1)))`;;



  let TUAPYYU_concl = `
main_nonlinear_terminal_v11 ==>
(!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ 
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    ~scs_is_str s v p /\ ~scs_is_str s v (p+1) 
    ==> dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1))`;;



let TUAPYYU1= prove_by_refinement((mk_imp(NEHXMWH1_concl,mk_imp(NEHXMWH_concl, TUAPYYU_concl))),
[
REWRITE_TAC[IN;scs_is_str]
THEN REPEAT RESA_TAC
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 ASM_TAC
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
THEN ASM_SIMP_TAC[]
THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
THEN MRESAL_TAC SCS_STR_CASES_4[`p`;`s`;`v`][scs_is_str]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MP_TAC SCS_DIAG_A_LE_DIST
THEN RESA_TAC
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v (p+4-1)`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) <= pi
/\ ~(azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) = pi)
==> azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) < pi`)
THEN RESA_TAC
THEN REWRITE_TAC[ADD1]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`p+1`;`4`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v (SUC p+4-1)`]
THEN DICH_TAC (32-9)
THEN REWRITE_TAC[GSYM ADD1]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) <= pi
/\ ~(azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) = pi)
==> azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) < pi`)
THEN RESA_TAC;

DICH_TAC (33)
THEN RESA_TAC
THEN REWRITE_TAC[ADD1]
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`FF:real^3#real^3->bool`
THEN ASM_SIMP_TAC[]
THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
THEN REPEAT RESA_TAC;

THAYTHEL_TAC(32-25)[`i`;`p`][GSYM ADD1];


THAYTHEL_TAC(32-25)[`i`;`p+1`][ADD1]
THEN ASM_REWRITE_TAC[GSYM ADD1];


MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`p+3`;`4`]
THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`(p+3)+4-1`;`v:num->real^3`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v ((p+3)+4-1)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p+3)) (v (SUC (p+3))) (v ((p+3) + 4 - 1)) <= pi
/\ ~(azim (vec 0) (v (p+3)) (v (SUC (p+3))) (v ((p+3) + 4 - 1)) = pi)
==> azim (vec 0) (v (p+3)) (v (SUC ((p+3)))) (v ((p+3) + 4 - 1)) < pi`)
THEN RESA_TAC;

THAYTHEL_TAC(38-25)[`i`;`p+3`][GSYM ADD1];

DICH_TAC (34)
THEN RESA_TAC
THEN REWRITE_TAC[ADD1]
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`FF:real^3#real^3->bool`
THEN ASM_SIMP_TAC[]
THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES_3]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
THEN REPEAT RESA_TAC;

THAYTHEL_TAC(32-25)[`i`;`p`][GSYM ADD1];


THAYTHEL_TAC(32-25)[`i`;`p+1`][ADD1]
THEN ASM_REWRITE_TAC[GSYM ADD1];


MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`p+2`;`4`]
THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`(p+2)+4-1`;`v:num->real^3`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v ((p+2)+4-1)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p+2)) (v (SUC (p+2))) (v ((p+2) + 4 - 1)) <= pi
/\ ~(azim (vec 0) (v (p+2)) (v (SUC (p+2))) (v ((p+2) + 4 - 1)) = pi)
==> azim (vec 0) (v (p+2)) (v (SUC ((p+2)))) (v ((p+2) + 4 - 1)) < pi`)
THEN RESA_TAC;

THAYTHEL_TAC(38-25)[`i`;`p+2`][GSYM ADD1]]);;


let TUAPYYU=prove( TUAPYYU_concl,
STRIP_TAC
THEN MP_TAC TUAPYYU1
THEN RESA_TAC
THEN MP_TAC Jotswix.NEHXMWH
THEN MP_TAC Jotswix.BZQNDMN
THEN ASM_REWRITE_TAC[]);;


(**************************)


let SCS_M_CASES_4_LE_2=prove(`scs_k_v39 s = 4/\ is_scs_v39 s 
==> CARD (scs_M s)<=2`,
REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;scs_M]
THEN RESA_TAC
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC);;



let SCS_M_CASES_4_EQ=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
==> scs_M s={p MOD 4,(p+3)MOD 4}`,
REPEAT STRIP_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 3 MOD 4)`)
THEN MRESAS_TAC Planarity.CARD_2_FAN[`(p+0) MOD 4`;`(p+3) MOD 4`][Ocbicby.MOD_EQ_MOD_SHIFT]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`p+0=p`]
THEN STRIP_TAC
THEN MP_TAC SCS_M_CASES_4_LE_2
THEN RESA_TAC
THEN MP_TAC Jlxfdmj.FINITE_SCS_M
THEN RESA_TAC
THEN MRESA_TAC CARD_SUBSET_LE[`{p MOD 4, (p + 3) MOD 4}`;`scs_M s`]);;

let B_LE_2h0_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
==> scs_b_v39 s (p+1) (p+2)<= &2*h0`,
REPEAT STRIP_TAC
THEN MP_TAC SCS_M_CASES_4_EQ
THEN RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(1 MOD 4 = 3 MOD 4)/\ 1<4`)
THEN SUBGOAL_THEN`~((p+1) MOD 4 IN scs_M s)`ASSUME_TAC
THENL[
ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAL_TAC Qknvmlb.SUC_MOD_NOT_EQ[`4`][ADD1];

DICH_TAC 0
THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
THEN ASM_SIMP_TAC[DIVISION]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1) MOD 4`;`SUC ((p + 1) MOD 4)`;`s`;`p+1`;`SUC ((p + 1) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`SUC (p + 1) MOD 4`;`s`;`p+1`;`SUC (p + 1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+1)=p+2`]
THEN REAL_ARITH_TAC]);;


let B_LE_2h0_2_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
==> scs_b_v39 s (p+2) (p+3)<= &2*h0`,
REPEAT STRIP_TAC
THEN MP_TAC SCS_M_CASES_4_EQ
THEN RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(2 MOD 4 = 3 MOD 4)/\ ~(2 MOD 4 = 0 MOD 4)/\ 1<4`)
THEN SUBGOAL_THEN`~((p+2) MOD 4 IN scs_M s)`ASSUME_TAC
THENL[
ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`0`;`p`][ARITH_RULE`p+0=p`];
DICH_TAC 0
THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
THEN ASM_SIMP_TAC[DIVISION]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2) MOD 4`;`SUC ((p + 2) MOD 4)`;`s`;`p+2`;`SUC ((p + 2) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`SUC (p + 2) MOD 4`;`s`;`p+2`;`SUC (p + 2)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+2)=p+3`]
THEN REAL_ARITH_TAC]);;



let B_LE_2h0_2_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
==> scs_b_v39 s (p+1) (p+2)<= &2*h0 /\ scs_b_v39 s (p+2) (p+3)<= &2*h0`,
SIMP_TAC[B_LE_2h0_2_SCS_M_4;B_LE_2h0_SCS_M_4]);;



let WKZZEEH = prove_by_refinement(`main_nonlinear_terminal_v11 ==> 
  (!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\ 
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ ~scs_is_str s v (p+3) 
    ==> (~(dist(v p,v(p+3)) = cstab /\ dist(v(p),v(p+1)) = cstab)))`,
[STRIP_TAC
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN REWRITE_TAC[DE_MORGAN_THM]
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 ASM_TAC
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
THEN ASM_SIMP_TAC[]
THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN SUBGOAL_THEN`!i. dist((v:num->real^3) i, v(SUC i))<= cstab`ASSUME_TAC
;


REWRITE_TAC[dist]
THEN MATCH_MP_TAC (GEN_ALL Axjrpnc.NORM_V_IN_BB_LE_CSTAB)
THEN EXISTS_TAC`s:scs_v39`
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN REWRITE_TAC[ADD1]
THEN THAYTHE_TAC (18-6)[`i`]
THEN REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC;

THAYTHEL_ASM_TAC 0[`p`][ADD1]
THEN THAYTHEL_TAC 0[`p+3`][ARITH_RULE`SUC(p+3)=1*4+p`]
THEN DICH_TAC 0
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DIST_SYM]
THEN REMOVE_ASSUM_TAC
THEN DICH_TAC 0
THEN MP_TAC Jotswix.JOTSWIX
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`v`;`p`]
THEN DICH_TAC 0
THEN SUBGOAL_THEN`scs_a_v39 s p (p + 1) < cstab`ASSUME_TAC;


THAYTHE_TAC (18-6)[`p`]
THEN REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC;


ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`(!i. ~(i MOD 4 = (p + 2) MOD 4) ==> interior_angle1 (vec 0) FF ((v:num->real^3)i) < pi)`ASSUME_TAC;

REMOVE_ASSUM_TAC
THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES]
THEN REPEAT STRIP_TAC;


MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`i`;`p`][MOD_MULT_ADD]
THEN DICH_TAC(20-7)
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v (p+4-1)`]
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;




MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`i`;`p+1`][MOD_MULT_ADD]
THEN DICH_TAC(20-8)
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (SUC p)`;`v`;`(SUC p)`;`4`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v ((SUC p)+4-1)`]
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;




MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`i`;`p+3`][MOD_MULT_ADD]
THEN DICH_TAC(20-9)
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`(p+3)`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`(p+3)+4-1`;`v:num->real^3`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v ((p+3))`;`v`;`((p+3))`;`4`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v ((p+3))`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v (((p+3))+4-1)`]
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;


REPEAT RESA_TAC
THEN MP_TAC(REAL_ARITH`dist (v p,v (p + 1)) <= cstab/\
dist (v p,v (p + 3)) <= cstab
==> (dist (v p,v (p + 1)) = cstab/\dist (v p,v (p + 3)) = cstab)
\/ dist ((v:num->real^3) p,v (p + 1)) < cstab \/ dist (v p,v (p + 3)) < cstab`)
THEN RESA_TAC;


SUBGOAL_THEN`p MOD 4 IN scs_M s`ASSUME_TAC;


ASM_SIMP_TAC[scs_M;IN_ELIM_THM;DIVISION]
THEN MATCH_MP_TAC(SET_RULE`A==> A\/B`)
THEN DICH_TAC(25-15)
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`p MOD 4`;`SUC(p MOD 4)`]
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`p MOD 4`;`p`][MOD_REFL]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`SUC(p MOD 4)`;`SUC(p MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`SUC p MOD 4`;`SUC p`][MOD_REFL;ADD1;cstab;h0]
THEN REAL_ARITH_TAC
;



SUBGOAL_THEN`(p+3) MOD 4 IN scs_M s`ASSUME_TAC;

REMOVE_ASSUM_TAC
THEN ASM_SIMP_TAC[scs_M;IN_ELIM_THM;DIVISION]
THEN MATCH_MP_TAC(SET_RULE`A==> A\/B`)
THEN DICH_TAC(25-15)
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`(p+3) MOD 4`;`SUC((p+3) MOD 4)`]
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3) MOD 4`;`(p+3)`][MOD_REFL]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`SUC((p+3) MOD 4)`;`SUC((p+3) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+3)=(1*4+p)`;MOD_MULT_ADD]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`p MOD 4`;`p`][MOD_REFL;ADD1;cstab;h0]
THEN REAL_ARITH_TAC
;


MP_TAC(SET_RULE`p MOD 4 IN scs_M s/\
(p + 3) MOD 4 IN scs_M s==>{p MOD 4,(p+3)MOD 4} SUBSET scs_M s`)
THEN RESA_TAC
THEN MP_TAC B_LE_2h0_2_SCS_M_4
THEN RESA_TAC
THEN MRESAL_TAC ASSWPOW[`s`;`v`;`p+1`][IN;ARITH_RULE`(a+1)+1=a+2/\ (a+1)+2=a+3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ONCE_REWRITE_TAC[Ocbicby.xrr_sym]
THEN STRIP_TAC
THEN DICH_TAC(31-21)
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;



DICH_TAC 0
THEN REAL_ARITH_TAC
;

DICH_TAC 0
THEN REAL_ARITH_TAC
;
]);;


(***************************)
let BASIC_IMP_NOT_J=prove(`scs_basic_v39 s==> (!p i. ~scs_J_v39 s p i)`,
REWRITE_TAC[scs_basic]
THEN SET_TAC[]);;

let CONDTION_A_LT_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
==> (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1))`,
REWRITE_TAC[h0;cstab]
THEN REPEAT STRIP_TAC
THEN THAYTHE_TAC 0[`i`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;

let A_EQ2_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
/\ scs_a_v39 s p (p+1) = &2
==>  scs_b_v39 s p (p+1)= &2 * h0`,
REPEAT STRIP_TAC
THEN THAYTHE_TAC 1[`p`]
THEN DICH_TAC 1
THEN ASM_REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;

let A_EQ2h0_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
/\ scs_a_v39 s p (p+1) = &2 * h0
==>  scs_b_v39 s p (p+1)= cstab`,
REPEAT STRIP_TAC
THEN THAYTHE_TAC 1[`p`]
THEN DICH_TAC 1
THEN ASM_REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;


let A_NOT_EQ2_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
/\ ~(scs_a_v39 s p (p+1) = &2 )
==>  scs_a_v39 s p (p+1) = &2* h0 /\ scs_b_v39 s p (p+1)= cstab`,
REPEAT STRIP_TAC
THEN THAYTHE_TAC 1[`p`]);;



let B_LE_2h0_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
/\ scs_b_v39 s p (p+1) <= &2 *h0 
==>  scs_a_v39 s p (p+1) = &2 /\ scs_b_v39 s p (p+1)= &2*h0`,
REPEAT STRIP_TAC
THEN DICH_TAC 0
THEN THAYTHE_TAC 0[`p`]
THEN ASM_REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;


let STR_MOD_EQ=prove(`is_scs_v39 s /\ scs_k_v39 s = k /\ v IN MMs_v39 s
==>
(scs_is_str s v (p MOD k)<=> scs_is_str s v p)`,
REWRITE_TAC[IN;scs_is_str]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MP_TAC Yrtafyh.PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<k==> k-1<k`)
THEN RESA_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`p MOD k`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`SUC(p MOD k)`;`SUC p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL;Yxionxl2.MOD_SUC_MOD]
THEN MRESAS_TAC MOD_ADD_MOD[`p`;`k-1`;`k`][MOD_LT]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p MOD k)+k-1`;` p+k-1`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL;Yxionxl2.MOD_SUC_MOD]);;

let IN_SCS_STR_CASES_4=prove(`
    is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s  /\ scs_is_str s v p==>
p MOD 4 IN {i | i < 4 /\ scs_is_str s v i}`,
REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\1<4/\ 3<4`)
THEN ASM_SIMP_TAC[IN_ELIM_THM;DIVISION]
THEN DICH_TAC 1
THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN]);;


let FINITE_SET_STR=prove(`FINITE {i | i < k /\ scs_is_str s v i}`,
MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN ASM_REWRITE_TAC[FINITE_NUMSEG;IN_ELIM_THM;IN_NUMSEG;SUBSET]
THEN ARITH_TAC);;

let NOT_STR_IN_CASES_4=prove(`!s v.
    is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s  /\ scs_is_str s v p==>
    ~scs_is_str s v (p+1)/\ ~scs_is_str s v (p+2)/\ ~scs_is_str s v (p+3)`,
REPEAT GEN_TAC
THEN STRIP_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
THEN MRESA_TAC WGDHPPI[`s`;`v`]
THEN MP_TAC IN_SCS_STR_CASES_4
THEN RESA_TAC
THEN MRESA_TAC FINITE_SET_STR[`4`;`s`;`v`]
THEN MRESAS_TAC CARD_SUBSET_LE[`{p MOD 4}`;`{i | i < 4 /\ scs_is_str s v i}`][Geomdetail.CARD_SING;SET_RULE`a IN A==> {a} SUBSET A`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(2 MOD 4= 0 MOD 4)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`1`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(1 MOD 4= 0 MOD 4)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`3`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(3 MOD 4= 0 MOD 4)`]
THEN MP_TAC(SET_RULE`{p MOD 4} = {i | i < 4 /\ scs_is_str s v i}/\
~((p + 2) MOD 4 = p MOD 4)/\
~((p + 1) MOD 4 = p MOD 4)/\
~((p + 3) MOD 4 = p MOD 4)
==> ~((p + 1) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})/\
 ~((p + 2) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})/\
~((p + 3) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})`)
THEN RESA_TAC
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[IN_ELIM_THM; DIVISION;STR_MOD_EQ]);;


let NOT_STR_IN_CASES_4_1=prove(`!s v.
         is_scs_v39 s /\
         scs_k_v39 s = 4 /\
         v IN MMs_v39 s /\
         scs_is_str s v (p+1)
         ==> ~scs_is_str s v (p ) /\
             ~scs_is_str s v (p + 2) /\
             ~scs_is_str s v (p + 3)`,
REPEAT GEN_TAC
THEN STRIP_TAC
THEN MRESAL_TAC NOT_STR_IN_CASES_4[`p+1`;`s`;`v`][ARITH_RULE`(p+1)+1=p+2/\ (p+1)+2=p+3/\ (p+1)+3=1*4+p`]
THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][MOD_MULT_ADD]
THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][MOD_MULT_ADD]);;


let PRO_ADD_NOT_IN_SCS_M=prove(`is_scs_v39 s/\ scs_a_v39 s i (i+1) = &2 * h0/\ scs_k_v39 s=k
==> i MOD k IN scs_M s`,
REWRITE_TAC[IN_ELIM_THM;scs_M]
THEN RESA_TAC
THEN MP_TAC Yrtafyh.PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`i MOD k`;`SUC(i MOD k)`;`s`;`i`;`SUC(i MOD k) MOD k`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;DIVISION]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`i`;`SUC i MOD k`;`s`;`i`;`SUC i`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_REWRITE_TAC[ADD1;h0]
THEN REAL_ARITH_TAC);;

let TUAPYYU_IMP_CASES=prove(`
main_nonlinear_terminal_v11 ==>
(!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ 
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    ~scs_is_str s v p /\ ~scs_is_str s v (p+1) 
    ==> dist(v p,v(p+1)) = &2\/ dist(v p,v(p+1)) = &2 * h0 \/ dist(v p,v(p+1)) = cstab)`,
REPEAT STRIP_TAC
THEN MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p`][]
THEN THAYTHE_TAC 3[`p`]);;

let SCS_M_CASES_4_EQ1=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {(p+1) MOD 4,(p+3)MOD 4} SUBSET scs_M s
==> scs_M s={(p+1) MOD 4,(p+3)MOD 4}`,
REPEAT STRIP_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(1 MOD 4 = 3 MOD 4)`)
THEN MRESAS_TAC Planarity.CARD_2_FAN[`(p+1) MOD 4`;`(p+3) MOD 4`][Ocbicby.MOD_EQ_MOD_SHIFT]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`p+1=p+1`]
THEN STRIP_TAC
THEN MP_TAC SCS_M_CASES_4_LE_2
THEN RESA_TAC
THEN MP_TAC Jlxfdmj.FINITE_SCS_M
THEN RESA_TAC
THEN MRESA_TAC CARD_SUBSET_LE[`{(p+1) MOD 4, (p + 3) MOD 4}`;`scs_M s`]);;




let B_LE_2h0_2_SCS_M_4_1=prove(
`scs_k_v39 s = 4/\ is_scs_v39 s /\ {(p+1) MOD 4,(p+3)MOD 4} SUBSET scs_M s
==> scs_b_v39 s (p+2) (p+3)<= &2*h0`,
REPEAT STRIP_TAC
THEN MP_TAC SCS_M_CASES_4_EQ1
THEN RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(2 MOD 4 = 3 MOD 4)/\ ~(2 MOD 4 = 1 MOD 4)/\ 1<4`)
THEN SUBGOAL_THEN`~((p+2) MOD 4 IN scs_M s)`ASSUME_TAC
THENL[

ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`1`;`p`][ARITH_RULE`p+0=p`];

DICH_TAC 0
THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
THEN ASM_SIMP_TAC[DIVISION]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2) MOD 4`;`SUC ((p + 2) MOD 4)`;`s`;`p+2`;`SUC ((p + 2) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`SUC (p + 2) MOD 4`;`s`;`p+2`;`SUC (p + 2)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+2)=p+3`]
THEN REAL_ARITH_TAC]);;


let SCS_A_SYM=prove(`is_scs_v39 s
==> scs_a_v39 s i j= scs_a_v39 s j i`,
REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;dist]
THEN RESA_TAC);;

let SCS_B_SYM=prove(`is_scs_v39 s
==> scs_b_v39 s i j= scs_b_v39 s j i`,
REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;dist]
THEN RESA_TAC);;




(***************************)

let PWEIWBZ= prove_by_refinement(`
main_nonlinear_terminal_v11 ==>
(!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\ 
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    scs_a_v39 s p (p+1) = &2
    ==> dist(v p,v(p+1)) = &2)`,
[REPEAT RESA_TAC
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 ASM_TAC
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)/\ 4-1=3/\ SUC (p + 3)= 1*4+p/\ SUC p= p+1`)
THEN ASM_SIMP_TAC[]
THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MP_TAC Tfitskc.SCS_DIAG_A_LE_DIST
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(~scs_is_str s v p /\ ~scs_is_str s v (p+1))\/ scs_is_str s v p \/ scs_is_str s v (p+1)`)
THEN RESA_TAC;


MP_TAC YEBWJNG
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`s:scs_v39`
THEN ASM_REWRITE_TAC[IN];


MRESAL_TAC NOT_STR_IN_CASES_4[`p`;`s`;`v`][IN]
THEN DICH_TAC 3
THEN ASM_REWRITE_TAC[scs_is_str;]
THEN STRIP_TAC
THEN DICH_TAC(21-13)
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN THAYTHE_TAC 1[`p+3`;`p`]
;


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) (p)) V' E')` ASSUME_TAC;



REPEAT RESA_TAC
;



MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3)+1`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p=(p+3)+1`]
THEN STRIP_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
;

REPEAT RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[]
THEN MATCH_DICH_TAC 1
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
THEN SET_TAC[];


MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN STRIP_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
THEN MP_TAC CONDTION_A_LT_B
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`scs_a_v39 s (p + 3) p <= dist (v (p + 3),v p)
==> scs_a_v39 s (p + 3) p = dist (v (p + 3),v p)\/ scs_a_v39 s (p + 3) p < dist (v (p + 3),(v:num->real^3) p)`)
THEN RESA_TAC
;





SUBGOAL_THEN`dist (v (p + 3),(v:num->real^3) p) < scs_b_v39 s (p + 3) p`
ASSUME_TAC
;

THAYTHE_TAC 1[`p+3`]
THEN DICH_TAC 0
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`((p + 3) +1)`;`s`;`p+3`;`((p + 3)+1) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
;



MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+3`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
;


MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) p))\/ norm (v p)= &2`)
THEN RESA_TAC
;

MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
;

MP_TAC(SET_RULE`(scs_a_v39 s (p+1) (p+2) = &2 )\/ ~((scs_a_v39 s (p+1) (p+2) = &2 ))`)
THEN RESA_TAC;



SUBGOAL_THEN`scs_a_v39 s (p + 3) p < scs_b_v39 s (p + 3) p`
ASSUME_TAC
;

THAYTHE_TAC (45-42)[`p+3`]
THEN DICH_TAC 0
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`((p + 3) +1)`;`s`;`p+3`;`((p + 3)+1) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
;



MP_TAC  YEBWJNG
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN;ARITH_RULE`(p+1)+1=p+2`]
THEN ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3`)
THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
THEN THAYTHE_TAC (49-42)[`p+2`]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN MATCH_DICH_TAC 0
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;



ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3/\ (p+2)+3=1*4+p+1/\ (p+1)+3=1*4+p/\ (p+3)+1=1*4+p/\ (p+3)+3=1*4+p+2/\ (p+3)+2=1*4+p+1`)
THEN MRESA_TAC A_NOT_EQ2_IMP_B[`s`;`p+1`]
THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p+1`][IN;MOD_MULT_ADD]
THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p+1`][IN;MOD_MULT_ADD;MOD_REFL]
THEN THAYTHES_TAC (50-40)[`1 * 4 + p + 1`;`p+1`][MOD_MULT_ADD]
THEN MP_TAC WKZZEEH
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`v`;`p+2`]
THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+1`;`4`;`s`]
THEN MP_TAC(SET_RULE`scs_a_v39 s (p + 3) p = &2 \/ ~(scs_a_v39 s (p + 3) p = &2 )`)
THEN RESA_TAC;

(**********CASES a 3 0 =2********************)

MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN];


MP_TAC Jotswix.LEMMA_PWE1
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a`;scs_is_str]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
THEN MP_TAC Cuxvzoz.CJBDXXN
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
THEN DICH_TAC(58-17)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
THEN THAYTHE_TAC 0[`v (p)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
/\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
 &2 * #1.26 <= #3.01`]
THEN REPEAT STRIP_TAC;



THAYTHES_TAC(60-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN RESA_TAC
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
;




MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
;



MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
THEN REAL_ARITH_TAC;


POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN DICH_TAC 3
THEN RESA_TAC
THEN MP_TAC TUAPYYU_IMP_CASES
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];


(************CASES 2 3= 2**********)

MP_TAC Jotswix.LEMMA_PWE2
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;scs_is_str;h0]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p+2`;`p+2`][MOD_MULT_ADD]
THEN MP_TAC Cuxvzoz.CUXVZOZ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+3`;`v`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`(p+3)`;`4`]
THEN DICH_TAC(60-19)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][]
THEN THAYTHE_TAC 0[`v (p+2)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 3))  (v p) (v (p + 2)) <= pi
/\ ~(azim (vec 0) (v (p + 3))  (v p) (v (p + 2)) = pi)
==> azim (vec 0) (v (p + 3))  ((v:num->real^3) p) (v (p + 2)) < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) p,v (p + 2))`ASSUME_TAC
;




THAYTHES_TAC(62-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) \/
   azim (vec 0) (v p) (rho_node1 FF (v p)) (ivs_rho_node1 FF ((v:num->real^3) p)) < pi)`ASSUME_TAC
;





MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHEL_ASM_TAC(64-37)[`p+0`][]
THEN THAYTHES_TAC(0)[`p+2`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
THEN DICH_TAC 1
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN RESA_TAC
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+3)`;`v(p)`;`v (p+2)`]
;


SUBGOAL_THEN`scs_a_v39 s (p + 3) (1 * 4 + p) = &2`ASSUME_TAC
;



MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
;


SUBGOAL_THEN`scs_b_v39 s (p + 3) (1 * 4 + p) <= &2 * h0`ASSUME_TAC
;



MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;]
THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
THEN REAL_ARITH_TAC
;


ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= #3.01`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN DICH_TAC 0
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN THAYTHEL_ASM_TAC(73-40)[`p+2`][]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`( p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN THAYTHEL_ASM_TAC(1)[`p+3`][h0;cstab]
THEN REAL_ARITH_TAC;

(************CASES 2 3= 2* H0**********)


MP_TAC Jotswix.LEMMA_PWE2
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;scs_is_str;h0]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p+2`;`p+2`][MOD_MULT_ADD]
THEN MP_TAC Cuxvzoz.CUXVZOZ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+3`;`v`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`(p+3)`;`4`]
THEN DICH_TAC(60-19)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][]
THEN THAYTHE_TAC 0[`v (p+2)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 3))  (v p) (v (p + 2)) <= pi
/\ ~(azim (vec 0) (v (p + 3))  (v p) (v (p + 2)) = pi)
==> azim (vec 0) (v (p + 3))  ((v:num->real^3) p) (v (p + 2)) < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) p,v (p + 2))`ASSUME_TAC
;




THAYTHES_TAC(62-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) \/
   azim (vec 0) (v p) (rho_node1 FF (v p)) (ivs_rho_node1 FF ((v:num->real^3) p)) < pi)`ASSUME_TAC
;





MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHEL_ASM_TAC(64-37)[`p+0`][]
THEN THAYTHES_TAC(0)[`p+2`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
THEN DICH_TAC 1
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN RESA_TAC
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+3)`;`v(p)`;`v (p+2)`]
;


SUBGOAL_THEN`scs_a_v39 s (p + 3) (1 * 4 + p) = &2`ASSUME_TAC
;



MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
;


SUBGOAL_THEN`scs_b_v39 s (p + 3) (1 * 4 + p) <= &2 * h0`ASSUME_TAC
;



MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;]
THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
THEN REAL_ARITH_TAC
;


ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= &2 * #1.26 /\ &2 * #1.26 <= #3.01`;h0]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN DICH_TAC 0
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN THAYTHEL_ASM_TAC(73-40)[`p+2`][]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`( p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN THAYTHEL_ASM_TAC(1)[`p+3`][h0;cstab]
THEN REAL_ARITH_TAC;



(*************CASES a 3 0 NOT = 2************)


MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESA_TAC A_NOT_EQ2_IMP_B [`s`;`p+3`]
THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4_1[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
THEN MP_TAC YEBWJNG
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];



MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN];


MP_TAC Jotswix.LEMMA_PWE3
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a`;scs_is_str]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
THEN MP_TAC Cuxvzoz.CJBDXXN
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
;

DICH_TAC(67-17)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
THEN THAYTHE_TAC 0[`v (p)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
/\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
 &2 * #1.26 <= #3.01`]
THEN REPEAT STRIP_TAC;



THAYTHES_TAC(69-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN RESA_TAC
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
THEN ASM_REWRITE_TAC[DIHV_SYM];




MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
;



MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
THEN REAL_ARITH_TAC;



(*************CASES 1 2= cstab **************)


MP_TAC Jotswix.LEMMA_PWE3
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 * #1.26 <= #3.01`;scs_is_str;h0;cstab]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
THEN MP_TAC Cuxvzoz.CJBDXXN
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
;

DICH_TAC(67-17)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
THEN THAYTHE_TAC 0[`v (p)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
/\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
 &2 * #1.26 <= #3.01`]
THEN REPEAT STRIP_TAC;



THAYTHES_TAC(69-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN RESA_TAC
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
THEN ASM_REWRITE_TAC[DIHV_SYM];




MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
;



MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
THEN REAL_ARITH_TAC;


REAL_ARITH_TAC;


REAL_ARITH_TAC;



(*********scs_is_str p+1***********)




MRESAL_TAC NOT_STR_IN_CASES_4_1[`p`;`s`;`v`][IN]
THEN DICH_TAC 3
THEN ASM_REWRITE_TAC[scs_is_str;]
THEN STRIP_TAC
THEN DICH_TAC(21-13)
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN THAYTHE_TAC 1[`p+1`;`(p+2)`]
;


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) (p)) V' E')` ASSUME_TAC;



REPEAT RESA_TAC
;


ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+1)+3= 1*4+p/\ (p+3)+1= 1*4+p/\ (p+3)+2= 1*4+p+1/\ (p+3)+3= 1*4+p+2`)
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN DICH_TAC(32-20)
THEN RESA_TAC
THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v (p+1)`;`v (p+2)`;`(v:num->real^3) (p)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+2)`;`V`]
THEN SUBGOAL_THEN`(!j. ~(v j = v (p)) ==> ~collinear {vec 0, (v:num->real^3) (p ), v j})`ASSUME_TAC
;

REPEAT RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[]
THEN MATCH_DICH_TAC 1
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
THEN SET_TAC[];


MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p`][ARITH_RULE`0+2=2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN STRIP_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 3[`v (p+0)`;`v(p+2)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(0 MOD 4 = 2 MOD 4)`]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN STRIP_TAC
THEN MP_TAC CONDTION_A_LT_B
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`scs_a_v39 s (p+1) (p+2) <= dist (v (p+1),v (p+2))
==> scs_a_v39 s (p+1) (p+2) = dist (v (p+1),v (p+2))\/ scs_a_v39 s  (p+1) (p+2) < dist (v (p+1),(v:num->real^3) (p+2))`)
THEN RESA_TAC
;





SUBGOAL_THEN`dist (v (p + 1),(v:num->real^3) (p+2)) < scs_b_v39 s (p + 1) (p+2)`
ASSUME_TAC
;

THAYTHE_TAC 1[`p+1`]
THEN DICH_TAC 0
;

MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p+1`;`p+2`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MRESA_TAC SCS_A_SYM[`s`;`1*4+p`;`p+1`]
THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;`(p+1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_SIMP_TAC[DIST_SYM];


MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) (p+1)))\/ norm (v (p+1))= &2`)
THEN RESA_TAC
;

MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p+1`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
THEN DICH_TAC 0
THEN MRESA_TAC SCS_A_SYM[`s`;`1*4+p`;`p+1`]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;`(p+1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN ASM_SIMP_TAC[DIST_SYM];







MP_TAC(SET_RULE`(scs_a_v39 s (p+3) (p) = &2 )\/ ~((scs_a_v39 s (p+3) (p) = &2 ))`)
THEN RESA_TAC;



MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][IN;MOD_MULT_ADD]
THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN;MOD_MULT_ADD]
THEN MP_TAC  YEBWJNG
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN;ARITH_RULE`(p+1)+1=p+2`]
THEN THAYTHEL_ASM_TAC (55-42)[`p+1`][]
THEN THAYTHEL_TAC 0[`p+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN THAYTHES_TAC (58-40)[`(1 * 4 + p+1)`;`p+1`][MOD_MULT_ADD]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN MATCH_DICH_TAC 0
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;



ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3/\ (p+2)+3=1*4+p+1/\ (p+1)+3=1*4+p/\ (p+3)+1=1*4+p/\ (p+3)+3=1*4+p+2/\ (p+3)+2=1*4+p+1/\ (p+1)+2=p+3`)
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESA_TAC A_NOT_EQ2_IMP_B[`s`;`p+3`]
THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p+2`][IN;MOD_MULT_ADD]
THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p+2`][IN;MOD_MULT_ADD;MOD_REFL]
THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][IN;MOD_MULT_ADD]
THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN;MOD_MULT_ADD;MOD_REFL]
;

THAYTHES_TAC (59-40)[`1 * 4 + p + 2`;`p+2`][MOD_MULT_ADD]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p+1`;`p+1`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p+3`;`p+3`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MP_TAC WKZZEEH
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`v`;`p+3`]
THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
THEN MP_TAC(SET_RULE`scs_a_v39 s (p + 1) (p+2) = &2 \/ ~(scs_a_v39 s (p + 1) (p+2) = &2 )`)
THEN RESA_TAC;

(**********CASES a 1 2 =2********************)


MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN];






MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MP_TAC Jotswix.LEMMA_PWE2
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[scs_is_str]
THEN STRIP_TAC
THEN MP_TAC Cuxvzoz.CUXVZOZ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
;

DICH_TAC(69-17)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
THEN THAYTHE_TAC 0[`v (p+3)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
/\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3))  < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
 &2 * #1.26 <= #3.01`]
THEN REPEAT STRIP_TAC;



THAYTHES_TAC(71-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;



MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
THEN RESA_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
THEN RESA_TAC
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
;








DICH_TAC 3
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN MP_TAC TUAPYYU_IMP_CASES
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];


(************CASES 2 3= 2**********)


MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MP_TAC Jotswix.LEMMA_PWE1
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;h0]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[scs_is_str]
THEN STRIP_TAC
THEN MP_TAC Cuxvzoz.CJBDXXN
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+2`;`v`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_SIMP_TAC[REAL_ARITH`a<=a`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`(p+2)`;`4`]
;

DICH_TAC(75-18)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][]
THEN THAYTHE_TAC 0[`v (p+1)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) <= pi
/\ ~(azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) = pi)
==> azim (vec 0) (v (p + 2)) (v (p + 3)) ((v:num->real^3) (p + 1)) < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) (p+1),v (p + 3))`ASSUME_TAC
;




THAYTHES_TAC(77-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) \/
   azim (vec 0) ((v:num->real^3) (p + 1)) (rho_node1 FF (v (p + 1)))
   (ivs_rho_node1 FF (v (p + 1))) <
   pi)`ASSUME_TAC
;





MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+1)`;`V`]
THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+3)`;`V`]
THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+2)`;`v(p+3)`;`v (p+1)`]
;


ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= #3.01`]
THEN STRIP_TAC
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN MATCH_DICH_TAC 0
THEN THAYTHEL_ASM_TAC(80-40)[`p+2`][h0;cstab]
THEN REAL_ARITH_TAC;

(************CASES 2 3= 2* H0**********)




MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MP_TAC Jotswix.LEMMA_PWE1
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;h0]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[scs_is_str]
THEN STRIP_TAC
THEN MP_TAC Cuxvzoz.CJBDXXN
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+2`;`v`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_SIMP_TAC[REAL_ARITH`a<=a`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`(p+2)`;`4`]
;

DICH_TAC(75-18)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][]
THEN THAYTHE_TAC 0[`v (p+1)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) <= pi
/\ ~(azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) = pi)
==> azim (vec 0) (v (p + 2)) (v (p + 3)) ((v:num->real^3) (p + 1)) < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) (p+1),v (p + 3))`ASSUME_TAC
;




THAYTHES_TAC(77-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) \/
   azim (vec 0) ((v:num->real^3) (p + 1)) (rho_node1 FF (v (p + 1)))
   (ivs_rho_node1 FF (v (p + 1))) <
   pi)`ASSUME_TAC
;





MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+1)`;`V`]
THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+3)`;`V`]
THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+2)`;`v(p+3)`;`v (p+1)`]
;


ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= &2 * #1.26 /\ &2 * #1.26 <= #3.01`;h0]
THEN STRIP_TAC
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN MATCH_DICH_TAC 0
THEN THAYTHEL_ASM_TAC(80-40)[`p+2`][h0;cstab]
THEN REAL_ARITH_TAC;


(*************CASES a 1 2 NOT = 2************)


MRESA_TAC A_NOT_EQ2_IMP_B [`s`;`p+1`]
THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+1`;`4`;`s`]
THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4_1[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
THEN MP_TAC YEBWJNG
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];



MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN];


MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MP_TAC Jotswix.LEMMA_PWE4
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[scs_is_str;REAL_ARITH`a<=a`]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
;




MP_TAC Cuxvzoz.CUXVZOZ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
;

DICH_TAC(76-17)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
THEN THAYTHE_TAC 0[`v (p+3)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
/\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3))  < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
 &2 * #1.26 <= #3.01`]
THEN REPEAT STRIP_TAC;



THAYTHES_TAC(78-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;



MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
THEN RESA_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
THEN RESA_TAC
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
;



(*************CASES 0 3= cstab **************)



MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MP_TAC Jotswix.LEMMA_PWE4
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[scs_is_str;REAL_ARITH`&2 * #1.26 <= #3.01`;h0;cstab]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
;

MP_TAC Cuxvzoz.CUXVZOZ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[]
THEN REWRITE_TAC[GSYM ADD1]
THEN ASM_REWRITE_TAC[scs_generic]
THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
;

DICH_TAC(76-17)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
THEN THAYTHE_TAC 0[`v (p+3)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
/\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3))  < pi`)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
 &2 * #1.26 <= #3.01`]
THEN REPEAT STRIP_TAC;



THAYTHES_TAC(78-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;



MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
THEN RESA_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
THEN RESA_TAC
THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
;




REAL_ARITH_TAC;

]);;



let h0_CSTAB_LT_4=prove(`&2< &2*h0 /\ cstab< &4/\ &2<= &2*h0 /\ cstab<= &4
/\ &2*h0< &4/\ &2< &4`,
REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;







let VASYYAU= prove_by_refinement(`
main_nonlinear_terminal_v11 ==>
(!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\ 
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    scs_is_str s v p 
    ==> (dist(v p,v (p+1)) = scs_a_v39 s p (p+1) /\ dist(v p,v (p+3)) = scs_a_v39 s p (p+3)))`,
[STRIP_TAC
THEN REPEAT GEN_TAC
THEN STRIP_TAC
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 ASM_TAC
THEN REPLICATE_TAC 11 (RESA_TAC)
THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)/\ 4-1=3/\ SUC (p + 3)= 1*4+p/\ SUC p= p+1`)
THEN ASM_SIMP_TAC[]
THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MP_TAC Tfitskc.SCS_DIAG_A_LE_DIST
THEN RESA_TAC
THEN MP_TAC Jlxfdmj.SCS_A_2
THEN RESA_TAC
THEN THAYTHE_TAC 0[`p`]
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s p (p + 1)
==> scs_a_v39 s p (p+1) = &2\/ &2 < scs_a_v39 s p (p + 1)`)
THEN RESA_TAC;


MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`v`;`p`]
THEN DICH_TAC(20-7)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN STRIP_TAC;


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) (p)) V' E')` ASSUME_TAC;




REPEAT RESA_TAC
;



MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3)+1`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p=(p+3)+1`]
THEN STRIP_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[]
THEN MATCH_DICH_TAC 1
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
THEN SET_TAC[];



MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN STRIP_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
THEN MP_TAC CONDTION_A_LT_B
THEN RESA_TAC;



MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+1`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
THEN DICH_TAC 0
THEN MRESA_TAC SCS_A_SYM[`s`;`p`;`p+1`]
THEN MRESA_TAC SCS_B_SYM[`s`;`p`;`p+1`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN THAYTHE_TAC 2[`p`]
THEN RESA_TAC;

ASSUME_TAC(ARITH_RULE`(p+3)+1=1*4+p/\ (p+1)+1=p+2/\ (p+2)+1=p+3`)
THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
THEN MP_TAC Jlxfdmj.SCS_A_2
THEN RESA_TAC
THEN THAYTHE_TAC 0[`p+3`]
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s (p + 3) p
==> scs_a_v39 s (p+3) p = &2\/ &2 < scs_a_v39 s (p + 3) p`)
THEN RESA_TAC;


MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`v`;`p+3`]
THEN MRESA_TAC SCS_A_SYM[`s`;`p+3`;`p`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DICH_TAC(26-7)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN STRIP_TAC;


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) (p)) V' E')` ASSUME_TAC;




REPEAT RESA_TAC
;



MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[]
THEN MATCH_DICH_TAC 1
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
THEN SET_TAC[];



MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN STRIP_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
THEN MP_TAC CONDTION_A_LT_B
THEN RESA_TAC;



MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+3`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
THEN DICH_TAC 0
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN THAYTHE_TAC 1[`p+3`]
THEN RESA_TAC;


MP_TAC(REAL_ARITH`&2 < scs_a_v39 s p (p + 1)
/\ &2 < scs_a_v39 s (p + 3) p
==> ~(scs_a_v39 s (p + 3) p = &2)/\ ~(scs_a_v39 s p (p + 1)= &2)`)
THEN RESA_TAC
THEN MP_TAC A_NOT_EQ2_IMP_B
THEN RESA_TAC
THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
THEN MRESA_TAC  A_NOT_EQ2_IMP_B[`s`;`p+3`]
THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p`;`4`;`s`]
THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+1`]
THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
THEN MRESAL_TAC NOT_STR_IN_CASES_4[`p`;`s`;`v`][IN]
THEN MP_TAC YEBWJNG
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN]
THEN MP_TAC YEBWJNG
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN]
THEN DICH_TAC (44-13)
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
THEN RESA_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN THAYTHEL_ASM_TAC 1[`p`;`p+1`][]
THEN THAYTHE_TAC 0[`p+3`;`p`];



MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) p))\/ norm (v p)= &2`)
THEN RESA_TAC
;




DICH_TAC(51-7)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN STRIP_TAC;


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) (p)) V' E')` ASSUME_TAC;




REPEAT RESA_TAC
;



MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[]
THEN MATCH_DICH_TAC 1
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
THEN SET_TAC[];



MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN STRIP_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
THEN MP_TAC CONDTION_A_LT_B
THEN RESA_TAC;



MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
;



MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p`][Ckqowsa_3_points.in_ball_annulus;dist]
THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+1`][Ckqowsa_3_points.in_ball_annulus;dist]
THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+2`][Ckqowsa_3_points.in_ball_annulus;dist]
THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+3`][Ckqowsa_3_points.in_ball_annulus;dist]
THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v p`;`v (p+3)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+1)`;`v (p)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+1)`;`v (p+2)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+2)`;`v (p+3)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
THEN MRESA_TAC Trigonometry.KEITDWB[`vec 0:real^3`;`v (p+1)`;`v (p+3)`;`v (p+2)`];




DICH_TAC(68-7)
THEN ASM_REWRITE_TAC[scs_is_str]
THEN STRIP_TAC;




MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[]
THEN MATCH_DICH_TAC 1
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
THEN SET_TAC[];



MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`v p IN aff_gt {vec 0} {v (p + 1), v (p + 3)}
/\ aff_gt {vec 0} {v (p + 1), v (p + 3)} SUBSET aff_ge {vec 0} {v (p + 1), v (p + 3)}
==> (v:num->real^3) p IN aff_ge {vec 0} {v (p + 1), v (p + 3)}`)
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]
THEN RESA_TAC
THEN MRESA_TAC Iunbuig.ARCV_ADD_AFF_GE[`vec 0:real^3`;`v (p+1)`;`v (p+3)`;`v (p)`]
THEN DICH_TAC(79-67)
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[GSYM dist]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASSUME_TAC(h0_CSTAB_LT_4)
THEN MP_TAC(REAL_ARITH`  norm ((v:num->real^3) (p + 1)) <= &2 * h0 /\ &2<= norm (v (p + 1))/\ 
norm ((v:num->real^3) (p + 3)) <= &2 * h0 /\ &2<= norm (v (p + 3))/\ 
norm ((v:num->real^3) (p + 2)) <= &2 * h0 /\ &2<= norm (v (p + 2))/\ 
cstab< &4/\ &2 * h0< &4 /\ &2< &2 *h0
/\ dist (v p,v (p + 1)) <= cstab 
/\ &2* h0<= dist (v p,v (p + 1))
/\ dist (v p,v (p + 3)) <= cstab 
/\ &2* h0<= dist (v p,v (p + 3))
==> norm (v (p + 1)) < &4 /\ &0< norm (v (p + 1))/\
norm (v (p + 3)) < &4 /\ &0< norm (v (p + 3))/\
norm (v (p + 2)) < &4 /\ &0< norm (v (p + 2))/\
 dist (v p,v (p + 1))< &4/\ &2<= dist (v p,v (p + 1))/\ &0<  dist (v p,v (p + 1))/\
 dist (v p,v (p + 3))< &4/\ &2<= dist (v p,v (p + 3))/\ &0<  dist (v p,v (p + 3))/\
 &2< dist (v p,v (p + 1))/\
 &2< dist (v p,v (p + 3))/\
 &0< &2
`)
THEN RESA_TAC
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC
THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p)`;`v (p+1)`][]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
THEN REWRITE_TAC[GSYM dist]
THEN STRIP_TAC
THEN MRESAS_TAC Ocbicby.arclength_xrr[`(&2)`;`(norm (v (p + 1)))`;`(dist (v p,v (p + 1)))`][REAL_ARITH`a*a= a pow 2`]
THEN ONCE_REWRITE_TAC[Arc_properties.arc_sym]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[Arc_properties.arc_sym]
THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p)`;`v (p+3)`][]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
THEN REWRITE_TAC[GSYM dist]
THEN STRIP_TAC
THEN MRESAS_TAC Ocbicby.arclength_xrr[`(&2)`;`(norm (v (p + 3)))`;`(dist (v p,v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p+2)`;`v (p+3)`][]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
THEN REWRITE_TAC[GSYM dist]
THEN STRIP_TAC
THEN MRESAS_TAC Ocbicby.arclength_xrr[`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;`(dist (v (p+2),v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p+1)`;`v (p+2)`][]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
THEN REWRITE_TAC[GSYM dist]
THEN STRIP_TAC
THEN MRESAS_TAC Ocbicby.arclength_xrr[`(norm (v (p + 1)))`;`(norm (v (p + 2)))`;`(dist (v (p+1),v (p + 2)))`][REAL_ARITH`a*a= a pow 2`]
THEN MRESAL_TAC Ocbicby.xrr_increasing[`&2`;`(norm (v (p + 1)))`;`&2`;`(dist (v p,v (p + 1)))`][REAL_ARITH`&0<= &2`]
THEN MRESAL_TAC Ocbicby.xrr_increasing[`&2`;`(norm (v (p + 3)))`;`&2`;`(dist (v (p+3),v (p)))`][REAL_ARITH`&0<= &2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN MRESA_TAC Ocbicby.xrr_sym[`(norm (v (p + 2)))`;`(norm (v (p + 1)))`;`(dist (v (p+1),v (p+2)))`]
THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`(norm (v (p + 2)))`;`(norm (v (p + 1)))`;`(dist (v (p+2),v (p+3)))`][REAL_ARITH`&0<= &2`]
THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;`(dist (v (p+1),v (p+2)))`][REAL_ARITH`&0<= &2`]
THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(&2)`;`(norm (v (p + 1)))`;` (dist (v p,v (p + 1)))`][REAL_ARITH`a*a= a pow 2`]
THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(&2)`;`(norm (v (p + 3)))`;` (dist (v (p+3),v (p)))`][REAL_ARITH`a*a= a pow 2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC
THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(norm (v (p + 1)))`;`(norm (v (p + 2)))`;` (dist (v (p+1),v (p + 2)))`][REAL_ARITH`a*a= a pow 2`]
THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;` (dist (v (p+2),v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
THEN MP_TAC(REAL_ARITH`xrr (&2) (norm ((v:num->real^3) (p + 1))) (&2) <
      xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1)))/\
xrr (&2) (norm (v (p + 3))) (&2) <
      xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p))/\
xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) <=
      xrr (&2) (norm (v (p + 1))) (&2)/\
xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) <=
      xrr (&2) (norm (v (p + 3))) (&2)/\
&0 < xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1)))/\
xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) < &16/\
&0 < xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p))/\
xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p)) < &16/\
&0 < xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2)/\
xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) < &16/\
&0 < xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2)/\
xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) < &16
==> xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) <= &16 /\
      &0 <= xrr (&2) (norm (v (p + 1))) (&2)/\
xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p)) <= &16 /\
      &0 <= xrr (&2) (norm (v (p + 3))) (&2)/\
xrr (&2) (norm (v (p + 1))) (&2) <= &16 /\
      &0 <= xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2)/\
xrr (&2) (norm (v (p + 3))) (&2) <= &16 /\
      &0 <= xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2)
`)
THEN RESA_TAC
THEN MRESAL_TAC ACS_MONO_LT[`&1 - xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) / &8`;`&1 - xrr (&2) (norm (v (p + 1))) (&2) / &8`]
[REAL_ARITH`&1- a/ &8< &1- b/ &8 <=> b<a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
THEN MRESAL_TAC ACS_MONO_LT[`&1 - xrr (&2) (norm (v (p + 3))) (dist (v (p+3),v (p ))) / &8`;`&1 - xrr (&2) (norm (v (p + 3))) (&2) / &8`]
[REAL_ARITH`&1- a/ &8< &1- b/ &8 <=> b<a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
THEN MRESAL_TAC ACS_MONO_LE[`&1 - xrr (&2) (norm (v (p + 1))) (&2) / &8`;`&1 - xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) / &8`]
[REAL_ARITH`&1- a/ &8<= &1- b/ &8 <=> b<=a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
THEN MRESAL_TAC ACS_MONO_LE[`&1 - xrr (&2) (norm (v (p + 3))) (&2) / &8`;`&1 - xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) / &8`]
[REAL_ARITH`&1- a/ &8<= &1- b/ &8 <=> b<=a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;

]);;




 end;;


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