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


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


module Aursipd = struct


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

open Hales_tactic;;

open Appendix;;





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

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;

open Qknvmlb;;
open Odxlstcv2;;

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

open Nuxcoea;;
open Fektyiy;;





let REP_NUMSEG=
prove(`~(k=0) ==> {i | i < k}= 0.. (k-1)`,

REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC);;


let SUM_AZIM_EQ_ANGLE_LE4_FUN=
prove_by_refinement(
` ~(scs_k_v39 s<=3)/\
 BBs_v39 s vv /\
	is_scs_v39 s /\
(vv:num->real^3) (p MOD (scs_k_v39 s))=u /\
IMAGE (vv:num->real^3) (:num)=V/\
 IMAGE (\i. {vv i,(vv:num->real^3) (SUC i)}) (:num)=E/\
 IMAGE (\i. (vv i,(vv:num->real^3) (SUC i))) (:num)=FF
==>
	sum {i | i < scs_k_v39 s}
      (\i. ff((vv:num->real^3) (i+p MOD scs_k_v39 s)) *
           interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) u))
=sum FF (\e. ff(FST e) * azim_in_fan e E)
`,

[
MRESA_TAC (GEN_ALL IN_IMAGE_VV)[`p MOD scs_k_v39 s`;`vv:num->real^3`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;scs_diag;dist]
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN REPEAT RESA_TAC;

REPLICATE_TAC (30-2)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[];

MATCH_MP_TAC SUM_EQ_GENERAL
THEN EXISTS_TAC`(\i. (vv:num->real^3) (i+ p MOD k), vv (SUC i + p MOD k))`
THEN MP_TAC(ARITH_RULE`3<= k  ==>  ~(k=0) /\ 1<k`)
THEN RESA_TAC
THEN STRIP_TAC;

EXPAND_TAC"FF"
THEN REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE]
THEN ASM_REWRITE_TAC[PAIR_EQ]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`(x MOD k + k -p MOD k) MOD k`
THEN ASM_REWRITE_TAC[ARITH_RULE`A-0=A`;PAIR_EQ]
THEN MRESA_TAC DIVISION[`x MOD k + k - p MOD k:num`;`k:num`]
THEN MRESA_TAC DIVISION[`p:num`;`k:num`]
THEN MRESA_TAC MOD_LT[`p MOD k`;`k:num`]
THEN MRESA_TAC MOD_MOD_REFL[`x:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`x MOD k`][ARITH_RULE`1 * k + x MOD k = x MOD k +k`]
THEN MRESA_TAC MOD_ADD_MOD[`x MOD k + k - p MOD k:num`;`p MOD k:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`1<k/\ p MOD k<k ==>(x MOD k+ k- p MOD k) + p MOD k = x MOD k+k /\ (x + p MOD k) + k- p MOD k= x+k`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM(fun th-> MRESA1_TAC th `(x MOD k + k - p MOD k) MOD k + p MOD k:num`
THEN MRESA1_TAC th ` x:num`)
THEN MRESA_TAC MOD_ADD_MOD[`x:num`;`1`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`(x MOD k + k - p MOD k) MOD k + p MOD k`;`1`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`;ARITH_RULE`SUC ((x MOD k + k - p MOD k) MOD k) + p MOD k =  ((x MOD k + k - p MOD k) MOD k + p MOD k)+1`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th `((x MOD k + k - p MOD k) MOD k + p MOD k)+1:num`
THEN MRESA1_TAC th `  x+1:num`)
THEN REWRITE_TAC[ADD1]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC DIVISION[`x:num`;`k:num`]
THEN MRESA_TAC DIVISION[`y' + p MOD k:num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM(fun th-> MRESA1_TAC th `y' + p MOD k:num`)
THEN MP_TAC VV_INJ
THEN ASM_REWRITE_TAC[MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;scs_half_slice_v39;PAIR_EQ;REAL_ARITH`#0.11 < #0.9`;ARITH_RULE`3<=3`;dist]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(y'+ p MOD k) MOD k:num`;`(x MOD k + k)MOD k`])
THEN MRESA_TAC MOD_LT[`y':num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL Hdplygy.MOD_EQ_MOD)[`y':num`;`x MOD k + k- p MOD k`;`p MOD k`;`k:num`][]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[ADD_SYM]
THEN RESA_TAC;

REWRITE_TAC[IN_ELIM_THM;]
THEN REPEAT STRIP_TAC;

EXPAND_TAC"FF"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`x+  p MOD k`
THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ADD1;ARITH_RULE`(x + 1) + p MOD k= (x  + p MOD k)+1`];

MRESAL_TAC(GEN_ALL VV_SUC_EQ_RHO_NODE_PRIME)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`k:num`;`s:scs_v39`;`FF:real^3#real^3->bool`;`u:real^3`;`vv:num->real^3`;`p:num MOD k`]
[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;scs_diag;dist]
THEN SUBGOAL_THEN`(vv:num->real^3) (x + p MOD k) IN V`ASSUME_TAC;

EXPAND_TAC"V"
THEN REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`x+ p MOD k`
THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

REPLICATE_TAC (35-6)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN  MP_TAC Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) (x + p MOD k )`])
THEN REPLICATE_TAC (3) REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC th 
THEN MRESAL1_TAC th`SUC x`[ITER])]);;



let PERIODIC_IMAGE2=
prove(`~(n = 0) /\ periodic f n ==> {f i | i < n} = IMAGE f (:num)`,

STRIP_TAC
THEN MRESA_TAC Oxlzlez.PERIODIC_IMAGE[`f`;`n`]
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN SET_TAC[]);;





let AURSIPD_concl = `!s v.
  3< scs_k_v39 s /\ is_scs_v39 s /\ scs_generic v /\ v IN MMs_v39 s ==>
  3 + CARD { i | i < scs_k_v39 s /\ scs_is_str s v i} <= scs_k_v39 s`;;

let AURSIPD= prove_by_refinement((AURSIPD_concl),
[REWRITE_TAC[IN;scs_is_str;scs_generic]
THEN REPEAT STRIP_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 MATCH_MP_TAC(ARITH_RULE`~(b-3< c) /\ 3<b ==> 3+c <= b:num`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN SUBGOAL_THEN `CARD {i | i < k /\ azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi}<= CARD (0..(k-1))` ASSUME_TAC;


MATCH_MP_TAC CARD_SUBSET
THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN DICH_TAC 8
THEN ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[CARD_NUMSEG]
THEN MP_TAC(ARITH_RULE`3<k==> (k-1+1)-0=k`)
THEN RESA_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN`{i | i < k /\ azim (vec 0:real^3) (v i) (v (SUC i)) (v (i + k - 1)) = pi} SUBSET (0..(k-1))`ASSUME_TAC;



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



ABBREV_TAC`a=CARD {i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`
THEN MP_TAC(ARITH_RULE`3<k/\ k - 3 <
      a /\ a <=   k
==> a=k \/ a =k-1\/ a=k-2`)
THEN RESA_TAC;



MRESAL_TAC SUBSET_CARD_EQ[`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`;`0..(k-1)`][FINITE_NUMSEG;CARD_NUMSEG]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG]
THEN STRIP_TAC
THEN ABBREV_TAC`v0= (v:num->real^3) 0`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`0`;`v`]
THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k:num`]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC Nuxcoea.MMS_IMP_BBPRIME[`s:scs_v39`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`v`]
THEN STRIP_TAC
THEN DICH_TAC 1
THEN REWRITE_TAC[REAL_ARITH`~(a< b)<=> b<=a`;sol_local]
THEN MATCH_MP_TAC (REAL_ARITH`&0< a/\ b= &0==> a<= &2 *a +b`)
THEN REWRITE_TAC[PI_WORKS]
THEN MATCH_MP_TAC SUM_EQ_0
THEN GEN_TAC
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA[`V:real^3->bool`;`FF`;`E`;`x`]
THEN MRESA_TAC Local_lemmas.DETER_RHO_NODE[`V:real^3->bool`;`E`;`FF`;`FST x`;`SND x`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V2[`E`;`FF`;`x`;`V`]
THEN MRESA_TAC Local_lemmas1.LF_AZIM_CYCLE_EQ_IVS_ND[`V`;`E`;`FF`;`FST x`]
THEN DICH_TAC (27-22)
THEN EXPAND_TAC "FF"
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)/\ (k+1)-1=k/\ ~(k=0)/\ 1<k/\ SUC (x' + k - 1) =1 * k + x'`)
THEN RESA_TAC
THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v0`;`v`;` 0`][ARITH_RULE`a+0=a`]
;

DICH_TAC (36-14)
THEN MRESA_TAC DIVISION[`x'`;`k`]
THEN MP_TAC(ARITH_RULE`x'  MOD k < k/\ 3<k==> x' MOD k <= k-1
/\ 0<= x' MOD k `)
THEN RESA_TAC
THEN RESA_TAC
THEN THAYTHEL_TAC 0 [`x' MOD k`][ARITH_RULE`a+1= SUC a/\ a+2= SUC (SUC a)`]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC Yxionxl2.MOD_SUC_MOD[`x'`;`k`]
THEN MRESA_TAC MOD_REFL[`SUC x' `;`k`]
THEN MRESA_TAC MOD_REFL[`x' `;`k`]
THEN MRESA_TAC
CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC ((x') MOD k)`;`v:num->real^3`;`SUC ((x') MOD k) MOD k`]
THEN MRESA_TAC
CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC (x') MOD k`;`v:num->real^3`;`SUC (x')`]
THEN MRESA_TAC WL_IN_V[`x' MOD k`;`v`]
THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
THEN RESA_TAC
THEN THAYTHE_TAC 0[`v (x' MOD k)`]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v (x' MOD k)`;`v`;` x' MOD k`][ARITH_RULE`a+0=a`]
THEN MRESA_TAC
CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`x' MOD k`;`v:num->real^3`;`x'`]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`a+k-1=k-1+a`]
THEN REAL_ARITH_TAC;

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


MP_TAC(SET_RULE`(!i. i < k ==> azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi)
==> {i | i < k /\ azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi}= {i| i<k}`)
THEN RESA_TAC
THEN DICH_TAC 3
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ ~(k=k-1)`)
THEN RESA_TAC
THEN MRESAL_TAC REP_NUMSEG[`k:num`][CARD_NUMSEG]
;

POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[NOT_FORALL_THM;NOT_IMP]
THEN REWRITE_TAC[NOT_IMP]
THEN STRIP_TAC
 THEN SUBGOAL_THEN`{i | i < k /\ azim (vec 0:real^3) (v i) (v (SUC i)) (v (i + k - 1)) = pi} SUBSET (0..(k-1)) DELETE i` ASSUME_TAC;


MATCH_MP_TAC (SET_RULE`A SUBSET B /\ ~(a IN A) ==> A SUBSET B DELETE a`)
THEN ASM_REWRITE_TAC[IN_ELIM_THM];



MRESAL_TAC FINITE_SUBSET[`(0..k - 1) DELETE i`;`(0..k - 1)`][FINITE_NUMSEG;DELETE_SUBSET]
THEN SUBGOAL_THEN`i IN 0..(k-1)`ASSUME_TAC
;

ASM_REWRITE_TAC[IN_NUMSEG]
THEN DICH_TAC 3
THEN DICH_TAC 16
THEN ARITH_TAC;

MRESAL_TAC CARD_DELETE[`i`;`0..(k-1)`][FINITE_NUMSEG]
THEN MRESAL_TAC SUBSET_CARD_EQ[`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`;`(0..(k-1)) DELETE i`][FINITE_NUMSEG;CARD_NUMSEG]
;



POP_ASSUM MP_TAC
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG]
THEN STRIP_TAC
THEN ABBREV_TAC`v0= (v:num->real^3) 0`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`0`;`v`]
THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k:num`]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC Nuxcoea.MMS_IMP_BBPRIME[`s:scs_v39`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`v`]
THEN STRIP_TAC
THEN DICH_TAC 1
THEN REWRITE_TAC[REAL_ARITH`~(a< b)<=> b<=a`;sol_local]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)/\ 0<k /\ ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`0`;`k`]
THEN MRESAL_TAC SUM_AZIM_EQ_ANGLE_LE4_FUN[`V`;`v`;`0`;`s`;`v0`;`FF`;`(\x:real^3. &1)`;` E`][SUM_SUB;REAL_ARITH`&1*a=a`]
THEN MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF
THEN RESA_TAC
THEN ASM_SIMP_TAC[SUM_SUB;SUM_CONST]
THEN REMOVE_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN MP_TAC Local_lemmas.LOFA_IMP_CARD_FF_V_EQ
THEN RESA_TAC
THEN MP_TAC Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
THEN RESA_TAC
THEN MP_TAC REP_NUMSEG
THEN RESA_TAC
THEN MRESAL_TAC SUM_DELETE[`(\i. interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v0))`;`{i|i<k:num}`;`i`][FINITE_NUMSEG;REAL_ARITH`a=b-c<=> b=a+c`]
THEN SUBGOAL_THEN`sum ((0..k - 1) DELETE i)
  (\i. interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v0)-pi) = &0`ASSUME_TAC
;



MATCH_MP_TAC SUM_EQ_0
THEN GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)/\ (k+1)-1=k/\ ~(k=0)/\ 1<k/\ SUC (x + k - 1) =1 * k + x`)
THEN RESA_TAC
THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v0`;`v`;` 0`][ARITH_RULE`a+0=a`]
THEN MRESA_TAC WL_IN_V[`x`;`v`]
THEN THAYTHE_TAC (43-35)[`v x`]
THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v x`;`v`;` x`][ARITH_RULE`a+0=a`]
THEN THAYTHEL_ASM_TAC 0 [`SUC 0`][ITER;I_DEF]
THEN THAYTHEL_TAC 0 [`k-1`][ITER;I_DEF]
THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
THEN RESA_TAC
THEN THAYTHE_TAC 0[`v x`]
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[ARITH_RULE`SUC 0+x= SUC x/\ k-1+x=x+k-1`]
THEN THAYTHE_TAC (45-20)[`x`]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[SUM_SUB;SUM_CONST;CARD_NUMSEG;REAL_ARITH`a-b= &0<=> a=b`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> 1<=k`)
THEN RESA_TAC
THEN MRESA_TAC REAL_OF_NUM_SUB[`1`;`k`]
THEN SYM_ASSUM_TAC
THEN MATCH_MP_TAC(REAL_ARITH`
&0<= interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v0)
==> pi <=
 &2 * pi +
 ((&k - &1) * pi + interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v0)) -
 &k * pi`)
THEN REWRITE_TAC[interior_angle1;azim]
;




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


MP_TAC(SET_RULE`(!i. i < k ==> azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi)
==> {i | i < k /\ azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi}= {i| i<k}`)
THEN RESA_TAC
THEN DICH_TAC 3
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ ~(k=k-2)`)
THEN RESA_TAC
THEN MRESAL_TAC REP_NUMSEG[`k:num`][CARD_NUMSEG]
;

POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[NOT_FORALL_THM;NOT_IMP]
THEN REWRITE_TAC[NOT_IMP]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`(!j. j < k /\ ~(i=j) ==> azim (vec 0) (v j) (v (SUC j)) (v (j + k - 1)) = pi) \/ ~(!j. j < k /\ ~(i=j) ==> azim (vec 0:real^3) (v j) (v (SUC j)) (v (j + k - 1)) = pi)`)
THEN RESA_TAC;



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


REWRITE_TAC[EXTENSION;IN_ELIM_THM;DELETE;IN_NUMSEG]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;


MP_TAC(ARITH_RULE`x<k/\ 3<k==> 0<=x/\ x<= k-1`)
THEN RESA_TAC
THEN STRIP_TAC
THEN DICH_TAC 3
THEN ASM_REWRITE_TAC[];

MP_TAC(ARITH_RULE`x<=k-1/\ 3<k ==> x< k`)
THEN RESA_TAC
THEN MATCH_DICH_TAC 4
THEN ASM_REWRITE_TAC[];


DICH_TAC (17-12)
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC FINITE_SUBSET[`(0..k - 1) DELETE i`;`(0..k - 1)`][FINITE_NUMSEG;DELETE_SUBSET]
THEN SUBGOAL_THEN`i IN 0..(k-1)`ASSUME_TAC
;

ASM_REWRITE_TAC[IN_NUMSEG]
THEN DICH_TAC (17-13)
THEN DICH_TAC 16
THEN ARITH_TAC;

MRESAL_TAC CARD_DELETE[`i`;`0..(k-1)`][FINITE_NUMSEG;CARD_NUMSEG]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ ~(k-1=k-2)`)
THEN RESA_TAC
;



POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[NOT_FORALL_THM;NOT_IMP]
THEN REWRITE_TAC[NOT_IMP]
THEN STRIP_TAC
THEN SUBGOAL_THEN`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi} SUBSET (0..(k-1)) DELETE i DELETE j`ASSUME_TAC;




REWRITE_TAC[SUBSET;DELETE;IN_ELIM_THM;IN_NUMSEG]
THEN GEN_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x<k/\ 3<k==> 0<=x/\ x<=k-1`)
THEN REPEAT RESA_TAC
;


DICH_TAC (23-15)
THEN DICH_TAC(22-19)
THEN ASM_REWRITE_TAC[]
;


DICH_TAC (23-18)
THEN DICH_TAC(22-19)
THEN ASM_REWRITE_TAC[]
;



SUBGOAL_THEN`i IN 0..(k-1)`ASSUME_TAC
;

ASM_REWRITE_TAC[IN_NUMSEG]
THEN DICH_TAC (19-14)
THEN DICH_TAC 18
THEN ARITH_TAC;

SUBGOAL_THEN`j IN ((0..(k-1)) DELETE i)`ASSUME_TAC
;

ASM_REWRITE_TAC[IN_NUMSEG;DELETE;IN_ELIM_THM]
THEN DICH_TAC (19-15)
THEN DICH_TAC 19
THEN ARITH_TAC;

MRESA_TAC FINITE_DELETE[`0..(k-1)`;`i`]
THEN MRESA_TAC FINITE_DELETE[`(0..(k-1)) DELETE i`;`j`]
THEN MRESAL_TAC CARD_DELETE[`i`;`0..(k-1)`][FINITE_NUMSEG]
THEN MRESAL_TAC CARD_DELETE[`j`;`(0..(k-1)) DELETE i`][FINITE_NUMSEG]
THEN MRESAL_TAC SUBSET_CARD_EQ[`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`;`(0..(k-1)) DELETE i DELETE j`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`k-2=k-1-1`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM;EXTENSION;DELETE;IN_NUMSEG]
THEN RESA_TAC;



MP_TAC(ARITH_RULE`~(i=j:num)==> i<j\/ j<i`)
THEN RESA_TAC;







SUBGOAL_THEN`!t:num. t<=j-i ==> coplanar ({v (i+t1)| t1<=t} UNION {vec 0:real^3, (v:num->real^3) i})`ASSUME_TAC
;


INDUCT_TAC
;


REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;]
THEN SUBGOAL_THEN`{v (i + t1) | t1 = 0} = {(v:num->real^3) i}`ASSUME_TAC
;


REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN EXISTS_TAC`0`
THEN REWRITE_TAC[ARITH_RULE`a+0=a`]
;


ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,a}={a,b}`;COPLANAR_2]
;


STRIP_TAC
THEN MP_TAC(ARITH_RULE`SUC t<= j-i==> t<= j-i`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN RESA_TAC
THEN SUBGOAL_THEN`{v (i + t1) | t1 <= SUC t}= {v (i + t1) | t1 <= t} UNION {(v:num->real^3) (i+ SUC t)}`ASSUME_TAC;



REWRITE_TAC[UNION;IN_ELIM_THM;EXTENSION;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;



MP_TAC(ARITH_RULE`t1<= SUC t==> t1<=t\/ t1= SUC t`)
THEN RESA_TAC
;


MATCH_MP_TAC(SET_RULE`A==>A\/B`)
THEN EXISTS_TAC`t1:num`
THEN ASM_REWRITE_TAC[]
;


EXISTS_TAC`t1:num`
THEN DICH_TAC 1
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

EXISTS_TAC`SUC t`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC
;


ASM_REWRITE_TAC[SET_RULE`(a UNION b) UNION c= a UNION b UNION c`]
THEN MP_TAC(ARITH_RULE`t=0 \/ 0<t`)
THEN RESA_TAC
;

REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;]
THEN SUBGOAL_THEN`{v (i + t1) | t1 = 0} = {(v:num->real^3) i}`ASSUME_TAC
;


REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN EXISTS_TAC`0`
THEN REWRITE_TAC[ARITH_RULE`a+0=a`]
;


ASM_REWRITE_TAC[SET_RULE`{a} UNION {b} UNION {c,a}={a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3]
;



MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`i+t-1`;`v`]
THEN MRESA_TAC WL_IN_V[`j`;`v`]
THEN MRESA_TAC WL_IN_V[`i+t:num`;`v`]
THEN MP_TAC(ARITH_RULE`0<t/\ t<=j-i/\ j<k ==> ~(i+t-1=i+t) /\ i+t-1<k/\ i+t<k`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`]
THEN THAYTHE_TAC 0[`i+t-1`;`i+t:num`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (i+t-1)`;`v j`;`V`]
THEN THAYTHEL_TAC 0[`(v:num->real^3) (i+t-1)`;`(v:num->real^3) (i+t)`][SET_RULE`a IN {a,b}`;coplanar]
THEN EXISTS_TAC`vec 0:real^3`
THEN EXISTS_TAC`(v:num->real^3) (i+t-1)`
THEN EXISTS_TAC`(v:num->real^3) (i+t)`
THEN ASM_REWRITE_TAC[UNION;SUBSET;IN_ELIM_THM;]
THEN REPEAT RESA_TAC;


SUBGOAL_THEN`{vec 0, v (i+t-1), v (i + t),v (i + t1)} SUBSET {v (i + t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i}`ASSUME_TAC
;


MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`)
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`]
THEN REPEAT RESA_TAC;

EXISTS_TAC`t-1:num`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

EXISTS_TAC`t1:num`
THEN ASM_REWRITE_TAC[]
;


MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (i+t-1), v (i + t), v (i + t1:num)}`;`{v (i + t1) | t1 <= t:num} UNION {vec 0, v i}`]
THEN MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`]
THEN ASM_REWRITE_TAC[];


POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_SING]
THEN RESA_TAC
THEN MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,D,A,C}`]
THEN MATCH_MP_TAC AZIM_EQ_0_PI_IMP_COPLANAR
THEN MATCH_MP_TAC(SET_RULE`A==> B \/ A`);


MP_TAC(ARITH_RULE`0<t/\ SUC t<= j-i/\ j<k ==>SUC (i + t)= i+ SUC t/\ 0<= i+t/\ 
i+t<=k-1/\ ~(i + t = i)/\ ~(i+t=j)/\ (i + t) + k - 1= (i + t - 1)+k`)
THEN RESA_TAC
THEN THAYTHE_TAC (51-26)[`i+t:num`]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;periodic]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN THAYTHE_TAC (53-33)[`i+t-1`];

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



REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff]
;



MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
;

SUBGOAL_THEN`{vec 0, v (i+t-1), v (i + t),v (i)} SUBSET {v (i + t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i}`ASSUME_TAC
;


MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`)
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`]
THEN REPEAT RESA_TAC;

EXISTS_TAC`t-1:num`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

EXISTS_TAC`0:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`0<=t/\ i+0=i`]
;


MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (i+t-1), v (i + t), v (i:num)}`;`{v (i + t1) | t1 <= t:num} UNION {vec 0, v i}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`]
THEN ASM_REWRITE_TAC[];


SUBGOAL_THEN`!t. t <= i+k-j ==> coplanar ({v (i+k - t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i})`ASSUME_TAC
;

INDUCT_TAC
;



REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;]
THEN SUBGOAL_THEN`{v (i+k - t1) | t1 = 0} = {(v:num->real^3) i}`ASSUME_TAC
;


REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_RULE`a-0=a`]
;

ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (41-4)[`i:num`]
;

EXISTS_TAC`0`
THEN REWRITE_TAC[ARITH_RULE`a-0=a`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (40-4)[`i:num`]
;



ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}= {a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3]
;


STRIP_TAC
THEN MP_TAC(ARITH_RULE`SUC t<= i+k-j==> t<= i+k-j`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN RESA_TAC
;


MP_TAC(ARITH_RULE`t=0\/ 0<t`)
THEN RESA_TAC;


SUBGOAL_THEN`{(v:num->real^3) (i + k - t1) | t1 <= SUC 0} ={v i, v(i+k-1)}`ASSUME_TAC
;


REWRITE_TAC[EXTENSION;ARITH_RULE`t<= SUC 0<=> t=0\/ t=1`;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;


ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic;ARITH_RULE`a- 0=a`]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (45-4)[`i:num`]
THEN SET_TAC[];

SET_TAC[]
;

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


EXISTS_TAC`0`
THEN REWRITE_TAC[ARITH_RULE`a-0=a`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic;ARITH_RULE`a- 0=a`]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (44-4)[`i:num`]
;

EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[]
;


ASM_REWRITE_TAC[SET_RULE`{a,b} UNION {c,a}={a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3]
;

REWRITE_TAC[coplanar]
THEN EXISTS_TAC`vec 0:real^3`
THEN EXISTS_TAC`(v:num->real^3) (i+k-t+1)`
THEN EXISTS_TAC`(v:num->real^3) (i+k-t)`
THEN ASM_REWRITE_TAC[UNION;SUBSET;IN_ELIM_THM;]
THEN REPEAT RESA_TAC
;




MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
;




MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`i+k-t+1`;`v`]
THEN MRESA_TAC WL_IN_V[`i+k-t:num`;`v`]
THEN MP_TAC(ARITH_RULE`3<k/\ SUC t<= i+k-j/\ i<j/\ j<k==> 1<k/\ SUC(i + k - t)=i + k - t +1/\ ~(k=0) `)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`i+k- t+1`;`k`]
THEN MRESA_TAC DIVISION[`i+k- t:num`;`k`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i+k- t:num`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - t+1) MOD k`;`v:num->real^3`;`(i + k - t+1):num`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - t) MOD k`;`v:num->real^3`;`(i + k - t):num`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`]
THEN THAYTHE_TAC 0[`(i+k- t+1) MOD k`;`(i+k-t:num) MOD k`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (i+k- t+1)`;`v (i+k-t:num)`;`V`]
THEN THAYTHEL_TAC 0[`v(i+k- t+1)`;`v(i+k-t:num)`][SET_RULE`a IN {a,b}`;]
;





MP_TAC(ARITH_RULE`t1<= SUC t==> t1<= t\/ t1= SUC t`)
THEN RESA_TAC
;


SUBGOAL_THEN`{vec 0, v (i+k-t+1), v (i+k-t),v (i+k-t1)} SUBSET {v (i+k- t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i}`ASSUME_TAC
;


MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`)
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`]
THEN REPEAT RESA_TAC;

EXISTS_TAC`t-1:num`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
;

DICH_TAC (53-32)
THEN ARITH_TAC;

MP_TAC(ARITH_RULE`0<t/\ t<= i+k-j/\ i<j/\ j<k==> 1<=t/\i+k-t+1=i+(k+1)-t`)
THEN RESA_TAC
THEN MRESA_TAC Ssrnat.subn_subA[`k:num`;`t:num`;`1`]
;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`a<=a:num`]
;



EXISTS_TAC`t1:num`
THEN ASM_REWRITE_TAC[]
;


MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (i + k - t + 1), v (i + k - t), v (i + k - t1)}`;`{v (i + k-t1) | t1 <= t:num} UNION {vec 0, v i}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`]
THEN ASM_REWRITE_TAC[];


ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,D,C,A}`]
THEN MATCH_MP_TAC AZIM_EQ_0_PI_IMP_COPLANAR
THEN MATCH_MP_TAC(SET_RULE`A==> B \/ A`);


THAYTHEL_TAC (53-26)[`(i+k-t) MOD k`][ARITH_RULE`0<=a`]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`(i + k - t) MOD k < k/\ 3<k /\ SUC t <= i + k - j/\ i<j/\ 0<t/\ j<k
==> (i + k - t) MOD k <= k - 1/\ 0<k/\ k-t<k /\ ~(k-t=0)/\ (i + k - t) + k - 1
=1*k+(i+ k - t-1)`)
THEN RESA_TAC
THEN SUBGOAL_THEN`~((i + k - t) MOD k = i)`ASSUME_TAC;


STRIP_TAC
THEN MRESA_TAC MOD_LT[`i`;`k`]
THEN MRESA_TAC MOD_LT[`0`;`k`]
THEN MRESA_TAC MOD_LT[`k-t:num`;`k`]
THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`k-t:num`;`0`;`i`;`k`][ARITH_RULE`a+0=a`]
;

SUBGOAL_THEN`~((i + k - t) MOD k = j)`ASSUME_TAC
;



STRIP_TAC
THEN MP_TAC(ARITH_RULE`(i + k - t) MOD k < k/\ 3<k /\ SUC t <= i + k - j/\ i<j/\ 0<t/\ j<k
==> (j + k - t) + t= j + k - t + t/\ t<=k/\ (j + k - t) + i + k - j= (i + k - t)  + k - j+j/\ j<=k/\ t<k/\ i+k-j<k/\ 1 * k + j= j+k/\ 1 * k + i + k - t=(i + k - t) + k/\ ~(i + k - j = t)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`t`;`k`]
THEN MRESA_TAC MOD_LT[`j`;`k`]
THEN MRESA_TAC MOD_LT[`i+k-j:num`;`k`]
THEN MRESA_TAC SUB_ADD[`k`;`t:num`]
THEN MRESA_TAC SUB_ADD[`k`;`j:num`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k`;`j`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k`;`(i + k - t):num`]
THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`i+k-j:num`;`t:num`;`j+k-t:num`;`k`][ARITH_RULE`a+0=a`];



ASM_REWRITE_TAC[]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`SUC ((i + k - t) MOD k):num`;`v:num->real^3`;`SUC ((i + k - t) MOD k) MOD k`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - t) MOD k + k - 1:num`;`v:num->real^3`;`((i + k - t) MOD k + k - 1) MOD k`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> k-1<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k-1`;`k`]
THEN MRESA_TAC Hypermap.lemma_sub_two_numbers[`k`;`t`;`1`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k`;`i + k - (t + 1)`]
THEN MRESA_TAC MOD_ADD_MOD[`i+k-t:num`;`k-1`;`k`]
THEN REWRITE_TAC[ADD1]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - (t + 1)) MOD k`;`v:num->real^3`;`(i + k - (t + 1))`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod]
THEN RESA_TAC
;




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



REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff]
;



MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
;



MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`i+k-t+1`;`v`]
THEN MRESA_TAC WL_IN_V[`i+k-t:num`;`v`]
THEN MP_TAC(ARITH_RULE`3<k/\ SUC t<= i+k-j/\ i<j/\ j<k==> 1<k/\ SUC(i + k - t)=i + k - t +1/\ ~(k=0) `)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`i+k- t+1`;`k`]
THEN MRESA_TAC DIVISION[`i+k- t:num`;`k`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i+k- t:num`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - t+1) MOD k`;`v:num->real^3`;`(i + k - t+1):num`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - t) MOD k`;`v:num->real^3`;`(i + k - t):num`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`]
THEN THAYTHE_TAC 0[`(i+k- t+1) MOD k`;`(i+k-t:num) MOD k`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (i+k- t+1)`;`v (i+k-t:num)`;`V`]
THEN THAYTHEL_TAC 0[`v(i+k- t+1)`;`v(i+k-t:num)`][SET_RULE`a IN {a,b}`;]
;




SUBGOAL_THEN`{vec 0, v (i + k - t + 1), v (i + k - t),v (i)} SUBSET {v (i+k- t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i}`ASSUME_TAC
;


MATCH_MP_TAC(SET_RULE`{b,c} SUBSET A==> {a,b,c,e} SUBSET A UNION {a,e}`)
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c}<=> a=b\/ a=c`]
THEN REPEAT RESA_TAC;

EXISTS_TAC`t-1:num`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
;

DICH_TAC (52-32)
THEN ARITH_TAC;

MP_TAC(ARITH_RULE`0<t/\ t<= i+k-j/\ i<j/\ j<k==> 1<=t/\i+k-t+1=i+(k+1)-t`)
THEN RESA_TAC
THEN MRESA_TAC Ssrnat.subn_subA[`k:num`;`t:num`;`1`]
;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`a<=a:num`]
;




MRESA_TAC COPLANAR_SUBSET[`{vec 0:real^3, v (i + k - t + 1), v (i + k - t), v i}`;`{(v:num->real^3) (i + k - t1) | t1 <= t} UNION {vec 0:real^3, v i}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`]
THEN ASM_REWRITE_TAC[];



MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC WL_IN_V[`i`;`v`]
THEN MRESA_TAC WL_IN_V[`j:num`;`v`]
THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`]
THEN THAYTHE_TAC 0[`i`;`j`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (i)`;`v (j:num)`;`V`]
THEN THAYTHEL_TAC 0[`v i`;`v j`][SET_RULE`a IN {a, b}`]
THEN SUBGOAL_THEN `coplanar ({vec 0} UNION {(v:num->real^3) (i+t)| t<k})`ASSUME_TAC
;


REWRITE_TAC[coplanar]
THEN EXISTS_TAC`vec 0:real^3`
THEN EXISTS_TAC`(v:num->real^3) i`
THEN EXISTS_TAC`(v:num->real^3) j`
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;UNION;IN_SING]
THEN REPEAT RESA_TAC;


REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff]
;


MP_TAC(ARITH_RULE`t<=j-i\/ j-i<=t:num`)
THEN RESA_TAC
;



MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
THEN THAYTHEL_TAC (39-28)[`j-i:num`][ARITH_RULE`j-i<=j-i:num`]
THEN MATCH_MP_TAC COPLANAR_SUBSET
THEN EXISTS_TAC`({v (i + t1) | t1 | t1 <= j - i} UNION {vec 0, (v:num->real^3) i})`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC(SET_RULE`a IN A/\ d IN A==>{a,b,c,d} SUBSET A UNION {b,c}`)
THEN STRIP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[];


EXISTS_TAC`j-i:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`j-i<=j-i:num/\ i+j-i=j-i+i`]
THEN MP_TAC(ARITH_RULE`i<j==> i<=j:num`)
THEN RESA_TAC
THEN MRESA_TAC SUB_ADD[`j`;`i`];




MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
THEN THAYTHEL_TAC (39-29)[`i+k-j:num`][ARITH_RULE`i+k-j<=i+k-j:num`]
THEN MATCH_MP_TAC COPLANAR_SUBSET
THEN EXISTS_TAC`({v (i + k - t1) | t1 | t1 <= i + k - j} UNION {vec 0, (v:num->real^3) i})`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC(SET_RULE`a IN A/\ d IN A==>{a,b,c,d} SUBSET A UNION {b,c}`)
THEN STRIP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
;


EXISTS_TAC`k-t:num`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`t<k/\ j-i<=t /\ j<k==> t<=k:num/\ k-t<= i+k-j`)
THEN RESA_TAC
THEN MRESA_TAC Ssrnat.subKn[`t`;`k`]
;


EXISTS_TAC`i+k-j:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`i + k - j<=i + k - j:num/\ i+j-i=j-i+i`]
THEN MP_TAC(ARITH_RULE`i<j/\ j<k==> i<=j:num/\ (i+k)-j= i+k-j/\ j<=i+k
/\ (i + k) - (i + k - j)= i + k - (i + k - j)`)
THEN RESA_TAC
THEN MRESA_TAC Ssrnat.subKn[`j:num`;`i+k:num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC BB_TRANS_SUBSET_BB[`s`;`v`;`i`]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)/\ ~(k=0)`)
THEN RESA_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39]
THEN RESA_TAC
THEN ASM_SIMP_TAC[PERIODIC_IMAGE2]
THEN MRESA_TAC TRANS_V[`s`;`i`;`v`]
THEN MRESAL_TAC FEKTYIY[`s`;`v`][IN]
;


(****************j<i****************)




SUBGOAL_THEN`!t:num. t<=i-j ==> coplanar ({v (j+t1)| t1<=t} UNION {vec 0:real^3, (v:num->real^3) j})`ASSUME_TAC
;


INDUCT_TAC
;


REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;]
THEN SUBGOAL_THEN`{v (j + t1) | t1 = 0} = {(v:num->real^3) j}`ASSUME_TAC
;


REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN EXISTS_TAC`0`
THEN REWRITE_TAC[ARITH_RULE`a+0=a`]
;


ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,a}={a,b}`;COPLANAR_2]
;


STRIP_TAC
THEN MP_TAC(ARITH_RULE`SUC t<= i-j==> t<= i-j`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN RESA_TAC
THEN SUBGOAL_THEN`{v (j + t1) | t1 <= SUC t}= {v (j + t1) | t1 <= t} UNION {(v:num->real^3) (j+ SUC t)}`ASSUME_TAC;



REWRITE_TAC[UNION;IN_ELIM_THM;EXTENSION;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;



MP_TAC(ARITH_RULE`t1<= SUC t==> t1<=t\/ t1= SUC t`)
THEN RESA_TAC
;


MATCH_MP_TAC(SET_RULE`A==>A\/B`)
THEN EXISTS_TAC`t1:num`
THEN ASM_REWRITE_TAC[]
;


EXISTS_TAC`t1:num`
THEN DICH_TAC 1
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

EXISTS_TAC`SUC t`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC
;


ASM_REWRITE_TAC[SET_RULE`(a UNION b) UNION c= a UNION b UNION c`]
THEN MP_TAC(ARITH_RULE`t=0 \/ 0<t`)
THEN RESA_TAC
;

REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;]
THEN SUBGOAL_THEN`{v (j + t1) | t1 = 0} = {(v:num->real^3) j}`ASSUME_TAC
;


REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_RULE`a+0=a`]
THEN EXISTS_TAC`0`
THEN REWRITE_TAC[ARITH_RULE`a+0=a`]
;


ASM_REWRITE_TAC[SET_RULE`{a} UNION {b} UNION {c,a}={a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3]
;



MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`j+t-1`;`v`]
THEN MRESA_TAC WL_IN_V[`i`;`v`]
THEN MRESA_TAC WL_IN_V[`j+t:num`;`v`]
THEN MP_TAC(ARITH_RULE`0<t/\ t<=i-j/\ i<k ==> ~(j+t-1=j+t) /\ j+t-1<k/\ j+t<k`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`]
THEN THAYTHE_TAC 0[`j+t-1`;`j+t:num`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (j+t-1)`;`v i`;`V`]
THEN THAYTHEL_TAC 0[`(v:num->real^3) (j+t-1)`;`(v:num->real^3) (j+t)`][SET_RULE`a IN {a,b}`;coplanar]
THEN EXISTS_TAC`vec 0:real^3`
THEN EXISTS_TAC`(v:num->real^3) (j+t-1)`
THEN EXISTS_TAC`(v:num->real^3) (j+t)`
THEN ASM_REWRITE_TAC[UNION;SUBSET;IN_ELIM_THM;]
THEN REPEAT RESA_TAC;


SUBGOAL_THEN`{vec 0, v (j+t-1), v (j + t),v (j + t1)} SUBSET {v (j + t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j}`ASSUME_TAC
;


MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`)
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`]
THEN REPEAT RESA_TAC;

EXISTS_TAC`t-1:num`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

EXISTS_TAC`t1:num`
THEN ASM_REWRITE_TAC[]
;


MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (j+t-1), v (j + t), v (j + t1:num)}`;`{v (j + t1) | t1 <= t:num} UNION {vec 0, v j}`]
THEN MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`]
THEN ASM_REWRITE_TAC[];


POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_SING]
THEN RESA_TAC
THEN MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,D,A,C}`]
THEN MATCH_MP_TAC AZIM_EQ_0_PI_IMP_COPLANAR
THEN MATCH_MP_TAC(SET_RULE`A==> B \/ A`);


MP_TAC(ARITH_RULE`0<t/\ SUC t<= i-j/\ i<k ==>SUC (j + t)= j+ SUC t/\ 0<= j+t/\ 
j+t<=k-1/\ ~(j + t = j)/\ ~(j+t=i)/\ (j + t) + k - 1= (j + t - 1)+k`)
THEN RESA_TAC
THEN THAYTHE_TAC (51-26)[`j+t:num`]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;periodic]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN THAYTHE_TAC (53-33)[`j+t-1`];

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



REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff]
;



MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
;

SUBGOAL_THEN`{vec 0, v (j+t-1), v (j + t),v (j)} SUBSET {v (j + t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j}`ASSUME_TAC
;


MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`)
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`]
THEN REPEAT RESA_TAC;

EXISTS_TAC`t-1:num`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

EXISTS_TAC`0:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`0<=t/\ i+0=i`]
;


MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (j+t-1), v (j + t), v (j:num)}`;`{v (j + t1) | t1 <= t:num} UNION {vec 0, v j}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`]
THEN ASM_REWRITE_TAC[];


SUBGOAL_THEN`!t. t <= j+k-i ==> coplanar ({v (j+k - t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j})`ASSUME_TAC
;

INDUCT_TAC
;



REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;]
THEN SUBGOAL_THEN`{v (j+k - t1) | t1 = 0} = {(v:num->real^3) j}`ASSUME_TAC
;


REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_RULE`a-0=a`]
;

ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (41-4)[`j:num`]
;

EXISTS_TAC`0`
THEN REWRITE_TAC[ARITH_RULE`a-0=a`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (40-4)[`j:num`]
;



ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}= {a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3]
;


STRIP_TAC
THEN MP_TAC(ARITH_RULE`SUC t<= j+k-i==> t<= j+k-i`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN RESA_TAC
;


MP_TAC(ARITH_RULE`t=0\/ 0<t`)
THEN RESA_TAC;


SUBGOAL_THEN`{(v:num->real^3) (j + k - t1) | t1 <= SUC 0} ={v j, v(j+k-1)}`ASSUME_TAC
;


REWRITE_TAC[EXTENSION;ARITH_RULE`t<= SUC 0<=> t=0\/ t=1`;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;


ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic;ARITH_RULE`a- 0=a`]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (45-4)[`j:num`]
THEN SET_TAC[];

SET_TAC[]
;

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


EXISTS_TAC`0`
THEN REWRITE_TAC[ARITH_RULE`a-0=a`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic;ARITH_RULE`a- 0=a`]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (44-4)[`j:num`]
;

EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[]
;


ASM_REWRITE_TAC[SET_RULE`{a,b} UNION {c,a}={a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3]
;

REWRITE_TAC[coplanar]
THEN EXISTS_TAC`vec 0:real^3`
THEN EXISTS_TAC`(v:num->real^3) (j+k-t+1)`
THEN EXISTS_TAC`(v:num->real^3) (j+k-t)`
THEN ASM_REWRITE_TAC[UNION;SUBSET;IN_ELIM_THM;]
THEN REPEAT RESA_TAC
;




MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
;




MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`j+k-t+1`;`v`]
THEN MRESA_TAC WL_IN_V[`j+k-t:num`;`v`]
THEN MP_TAC(ARITH_RULE`3<k/\ SUC t<= j+k-i/\ j<i/\ i<k==> 1<k/\ SUC(j + k - t)=j + k - t +1/\ ~(k=0) `)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`j+k- t+1`;`k`]
THEN MRESA_TAC DIVISION[`j+k- t:num`;`k`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`j+k- t:num`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - t+1) MOD k`;`v:num->real^3`;`(j + k - t+1):num`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - t) MOD k`;`v:num->real^3`;`(j + k - t):num`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`]
THEN THAYTHE_TAC 0[`(j+k- t+1) MOD k`;`(j+k-t:num) MOD k`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (j+k- t+1)`;`v (j+k-t:num)`;`V`]
THEN THAYTHEL_TAC 0[`v(j+k- t+1)`;`v(j+k-t:num)`][SET_RULE`a IN {a,b}`;]
;





MP_TAC(ARITH_RULE`t1<= SUC t==> t1<= t\/ t1= SUC t`)
THEN RESA_TAC
;


SUBGOAL_THEN`{vec 0, v (j+k-t+1), v (j+k-t),v (j+k-t1)} SUBSET {v (j+k- t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j}`ASSUME_TAC
;


MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`)
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`]
THEN REPEAT RESA_TAC;

EXISTS_TAC`t-1:num`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
;

DICH_TAC (53-32)
THEN ARITH_TAC;

MP_TAC(ARITH_RULE`0<t/\ t<= j+k-i/\ j<i/\ i<k==> 1<=t/\j+k-t+1=j+(k+1)-t`)
THEN RESA_TAC
THEN MRESA_TAC Ssrnat.subn_subA[`k:num`;`t:num`;`1`]
;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`a<=a:num`]
;



EXISTS_TAC`t1:num`
THEN ASM_REWRITE_TAC[]
;


MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (j + k - t + 1), v (j + k - t), v (j + k - t1)}`;`{v (j + k-t1) | t1 <= t:num} UNION {vec 0, v j}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`]
THEN ASM_REWRITE_TAC[];


ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,D,C,A}`]
THEN MATCH_MP_TAC AZIM_EQ_0_PI_IMP_COPLANAR
THEN MATCH_MP_TAC(SET_RULE`A==> B \/ A`);


THAYTHEL_TAC (53-26)[`(j+k-t) MOD k`][ARITH_RULE`0<=a`]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`(j + k - t) MOD k < k/\ 3<k /\ SUC t <= j + k - i/\ j<i/\ 0<t/\ i<k
==> (j + k - t) MOD k <= k - 1/\ 0<k/\ k-t<k /\ ~(k-t=0)/\ (j + k - t) + k - 1
=1*k+(j+ k - t-1)`)
THEN RESA_TAC
THEN SUBGOAL_THEN`~((j + k - t) MOD k = j)`ASSUME_TAC;


STRIP_TAC
THEN MRESA_TAC MOD_LT[`j`;`k`]
THEN MRESA_TAC MOD_LT[`0`;`k`]
THEN MRESA_TAC MOD_LT[`k-t:num`;`k`]
THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`k-t:num`;`0`;`j`;`k`][ARITH_RULE`a+0=a`]
;

SUBGOAL_THEN`~((j + k - t) MOD k = i)`ASSUME_TAC
;



STRIP_TAC
THEN MP_TAC(ARITH_RULE`(j + k - t) MOD k < k/\ 3<k /\ SUC t <= j + k - i/\ j<i/\ 0<t/\ i<k
==> (i + k - t) + t= i + k - t + t/\ t<=k/\ (i + k - t) + j + k - i= (j + k - t)  + k - i+i/\ i<=k/\ t<k/\ j+k-i<k/\ 1 * k + i= i+k/\ 1 * k + j + k - t=(j + k - t) + k/\ ~(j + k - i = t)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`t`;`k`]
THEN MRESA_TAC MOD_LT[`i`;`k`]
THEN MRESA_TAC MOD_LT[`j+k-i:num`;`k`]
THEN MRESA_TAC SUB_ADD[`k`;`t:num`]
THEN MRESA_TAC SUB_ADD[`k`;`i:num`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k`;`i`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k`;`(j + k - t):num`]
THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`j+k-i:num`;`t:num`;`i+k-t:num`;`k`][ARITH_RULE`a+0=a`];



ASM_REWRITE_TAC[]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`SUC ((j + k - t) MOD k):num`;`v:num->real^3`;`SUC ((j + k - t) MOD k) MOD k`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - t) MOD k + k - 1:num`;`v:num->real^3`;`((j + k - t) MOD k + k - 1) MOD k`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> k-1<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k-1`;`k`]
THEN MRESA_TAC Hypermap.lemma_sub_two_numbers[`k`;`t`;`1`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k`;`j + k - (t + 1)`]
THEN MRESA_TAC MOD_ADD_MOD[`j+k-t:num`;`k-1`;`k`]
THEN REWRITE_TAC[ADD1]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - (t + 1)) MOD k`;`v:num->real^3`;`(j + k - (t + 1))`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod]
THEN RESA_TAC
;




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



REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff]
;



MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
;



MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`j+k-t+1`;`v`]
THEN MRESA_TAC WL_IN_V[`j+k-t:num`;`v`]
THEN MP_TAC(ARITH_RULE`3<k/\ SUC t<= j+k-i/\ j<i/\ i<k==> 1<k/\ SUC(j + k - t)=j + k - t +1/\ ~(k=0) `)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`j+k- t+1`;`k`]
THEN MRESA_TAC DIVISION[`j+k- t:num`;`k`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN THAYTHE_TAC 0[`j+k- t:num`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - t+1) MOD k`;`v:num->real^3`;`(j + k - t+1):num`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - t) MOD k`;`v:num->real^3`;`(j + k - t):num`]
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[MOD_REFL]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`]
THEN THAYTHE_TAC 0[`(j+k- t+1) MOD k`;`(j+k-t:num) MOD k`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (j+k- t+1)`;`v (j+k-t:num)`;`V`]
THEN THAYTHEL_TAC 0[`v(j+k- t+1)`;`v(j+k-t:num)`][SET_RULE`a IN {a,b}`;]
;




SUBGOAL_THEN`{vec 0, v (j + k - t + 1), v (j + k - t),v (j)} SUBSET {v (j+k- t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j}`ASSUME_TAC
;


MATCH_MP_TAC(SET_RULE`{b,c} SUBSET A==> {a,b,c,e} SUBSET A UNION {a,e}`)
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c}<=> a=b\/ a=c`]
THEN REPEAT RESA_TAC;

EXISTS_TAC`t-1:num`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
;

DICH_TAC (52-32)
THEN ARITH_TAC;

MP_TAC(ARITH_RULE`0<t/\ t<= j+k-i/\ j<i/\ i<k==> 1<=t/\j+k-t+1=j+(k+1)-t`)
THEN RESA_TAC
THEN MRESA_TAC Ssrnat.subn_subA[`k:num`;`t:num`;`1`]
;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`a<=a:num`]
;




MRESA_TAC COPLANAR_SUBSET[`{vec 0:real^3, v (j + k - t + 1), v (j + k - t), v j}`;`{(v:num->real^3) (j + k - t1) | t1 <= t} UNION {vec 0:real^3, v j}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`]
THEN ASM_REWRITE_TAC[];



MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC WL_IN_V[`j`;`v`]
THEN MRESA_TAC WL_IN_V[`i:num`;`v`]
THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`]
THEN THAYTHE_TAC 0[`j`;`i`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (j)`;`v (i:num)`;`V`]
THEN THAYTHEL_TAC 0[`v j`;`v i`][SET_RULE`a IN {a, b}`]
THEN SUBGOAL_THEN `coplanar ({vec 0} UNION {(v:num->real^3) (j+t)| t<k})`ASSUME_TAC
;


REWRITE_TAC[coplanar]
THEN EXISTS_TAC`vec 0:real^3`
THEN EXISTS_TAC`(v:num->real^3) j`
THEN EXISTS_TAC`(v:num->real^3) i`
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;UNION;IN_SING]
THEN REPEAT RESA_TAC;


REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff]
;


MP_TAC(ARITH_RULE`t<=i-j\/ i-j<=t:num`)
THEN RESA_TAC
;



MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
THEN THAYTHEL_TAC (39-28)[`i-j:num`][ARITH_RULE`i-j<=i-j:num`]
THEN MATCH_MP_TAC COPLANAR_SUBSET
THEN EXISTS_TAC`({v (j + t1) | t1 | t1 <= i - j} UNION {vec 0, (v:num->real^3) j})`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC(SET_RULE`a IN A/\ d IN A==>{a,b,c,d} SUBSET A UNION {b,c}`)
THEN STRIP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
;


EXISTS_TAC`t:num`
THEN ASM_REWRITE_TAC[];


EXISTS_TAC`i-j:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`j-i<=j-i:num/\ i+j-i=j-i+i`]
THEN MP_TAC(ARITH_RULE`j<i==> j<=i:num`)
THEN RESA_TAC
THEN MRESA_TAC SUB_ADD[`i`;`j`];




MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull
THEN ASM_REWRITE_TAC[]
THEN THAYTHEL_TAC (39-29)[`j+k-i:num`][ARITH_RULE`i+k-j<=i+k-j:num`]
THEN MATCH_MP_TAC COPLANAR_SUBSET
THEN EXISTS_TAC`({v (j + k - t1) | t1 | t1 <= j + k - i} UNION {vec 0, (v:num->real^3) j})`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC(SET_RULE`a IN A/\ d IN A==>{a,b,c,d} SUBSET A UNION {b,c}`)
THEN STRIP_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
;


EXISTS_TAC`k-t:num`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`t<k/\ i-j<=t /\ i<k==> t<=k:num/\ k-t<= j+k-i`)
THEN RESA_TAC
THEN MRESA_TAC Ssrnat.subKn[`t`;`k`]
;


EXISTS_TAC`j+k-i:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`i + k - j<=i + k - j:num/\ i+j-i=j-i+i`]
THEN MP_TAC(ARITH_RULE`j<i/\ i<k==> j<=i:num/\ (j+k)-i= j+k-i/\ i<=j+k
/\ (j + k) - (j + k - i)= j + k - (j + k - i)`)
THEN RESA_TAC
THEN MRESA_TAC Ssrnat.subKn[`i:num`;`j+k:num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC BB_TRANS_SUBSET_BB[`s`;`v`;`j`]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)/\ ~(k=0)`)
THEN RESA_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39]
THEN RESA_TAC
THEN ASM_SIMP_TAC[PERIODIC_IMAGE2]
THEN MRESA_TAC TRANS_V[`s`;`j`;`v`]
THEN MRESAL_TAC FEKTYIY[`s`;`v`][IN]
;
]);;



 end;;


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