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


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


module Yxionxl2 = 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;;

let IN_SYM_0=
prove(`a IN A ==> (-- a) IN  IMAGE (\x:real^N. -- x) A`,

REWRITE_TAC[IMAGE;IN_ELIM_THM;VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN SET_TAC[]);;


let SUBSET_SYM_0=
prove(`A SUBSET B ==> IMAGE (\x. -- x) A SUBSET IMAGE (\x:real^N. -- x) B`,

REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM;VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN ASM_TAC
THEN SET_TAC[]);;
let SET_EQ_SYM_0=
prove(`A = B ==> IMAGE (\x. -- x) A = IMAGE (\x:real^N. -- x) B`,

REWRITE_TAC[EXTENSION]
THEN REPEAT RESA_TAC
THEN EQ_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN ASM_TAC
THEN SET_TAC[]);;

let IMAGE_V_SYM_0=
prove(`IMAGE (\i. --(vv:num->real^N) i) (:num)= IMAGE (\x. -- x) (IMAGE vv (:num))`,

REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THENL[
EXISTS_TAC`(vv:num->real^N) x'`
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`x'':num`
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]]);;


let UNIONS_IMAGE_FAN_SYM_0=
prove_by_refinement(`UNIONS (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))
= IMAGE (\x:real^N. -- x) (UNIONS (IMAGE (\i. {vv i, vv (SUC i)}) (:num)))`,

[REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[UNIONS;IMAGE;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;

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

EXISTS_TAC`(vv:num->real^N) x'`
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN EXISTS_TAC`{(vv:num->real^N) x', vv (SUC x')}`
THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];

EXISTS_TAC`(vv:num->real^N) (SUC x')`
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN EXISTS_TAC`{(vv:num->real^N) x', vv (SUC x')}`
THEN ASM_REWRITE_TAC[SET_RULE`a IN {b,a}`]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];
REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
THEN RESA_TAC;
EXISTS_TAC`{--(vv:num->real^N) x', --vv (SUC x')}`
THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`{--(vv:num->real^N) x', --vv (SUC x')}`
THEN ASM_REWRITE_TAC[SET_RULE`a IN {b,a}`]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[]]);;

let FINITE_SYM_0=
prove(`FINITE A ==> FINITE (IMAGE (\x:real^N. -- x) A)`,

SIMP_TAC[FINITE_IMAGE]);;
let CARD_SYM_0=
prove(`FINITE A ==> CARD (IMAGE (\x:real^N. -- x) A)= CARD A`,

STRIP_TAC
THEN MATCH_MP_TAC CARD_IMAGE_INJ
THEN RESA_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]);;

let ELEMENT2_SYM_0=
prove(`{--a, --b}= IMAGE (\x:real^N. --x) {a,b}`,

REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION;SET_RULE`a IN{b,c} <=> a=b\/ a=c`]
THEN GEN_TAC
THEN EQ_TAC
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN SET_TAC[]);;

let GRAPH_SYM_0=
prove(`graph (IMAGE (\i. {(vv:num->real^N) i, vv (SUC i)}) (:num))
==> 
graph (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))`,

REWRITE_TAC[GRAPH;HAS_SIZE;IMAGE;IN_ELIM_THM]
THEN STRIP_TAC
THEN GEN_TAC
THEN RESA_TAC
THEN SUBGOAL_THEN `(?x'. x' IN (:num) /\ {(vv:num->real^N) x, vv (SUC x)} = {vv x', vv (SUC x')})`ASSUME_TAC
THENL[
EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN
 MRESA_TAC th1[`{(vv:num->real^N) x, vv (SUC x)}`])
THEN ASM_SIMP_TAC[ELEMENT2_SYM_0;FINITE_SYM_0;CARD_SYM_0]]);;

let NOT_SUBSET_EMPTY_SYM_0=
prove(`~(A SUBSET {})
==> ~(IMAGE (\x:real^N. --x) A SUBSET {})`,

REWRITE_TAC[SET_RULE`~(A SUBSET {}) <=> ?a. a IN A`]
THEN RESA_TAC
THEN EXISTS_TAC`-- a:real^N`
THEN ASM_SIMP_TAC[IN_SYM_0]);;

let NOT_EMPTY_SYM_0=
prove(`~(A ={})
==> ~(IMAGE (\x:real^N. --x) A = {})`,

REWRITE_TAC[SET_RULE`~(A = {}) <=> ?a. a IN A`]
THEN RESA_TAC
THEN EXISTS_TAC`-- a:real^N`
THEN ASM_SIMP_TAC[IN_SYM_0]);;

let REFL_SYM_0=
prove(`IMAGE (\x:real^N. --x) (IMAGE (\x. --x) A) =A`,

REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`-- -- A=A:real^N`]
THEN EXISTS_TAC`--x:real^N`
THEN ASM_SIMP_TAC[VECTOR_ARITH`-- -- A=A:real^N`]
THEN EXISTS_TAC`x:real^N`
THEN ASM_REWRITE_TAC[]);;

let IMAGE_E_SYM_0=
prove(`e IN IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)
==> IMAGE (\x:real^N. --x) e IN IMAGE (\i. {vv i, vv (SUC i)}) (:num)`,

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`(-- --a=a:real^N)`]
THENL[
 EXISTS_TAC`-- (vv:num->real^N) x`
THEN ASM_SIMP_TAC[VECTOR_ARITH`(-- --a=a:real^N)`];
 EXISTS_TAC`-- (vv:num->real^N) (SUC x)`
THEN ASM_SIMP_TAC[VECTOR_ARITH`(-- --a=a:real^N)`]]);;

let COLLINEAR_SYM_0=
prove(`(collinear e) ==> (collinear (IMAGE (\x:real^N. --x) e))`,

REWRITE_TAC[collinear;IMAGE;IN_ELIM_THM]
THEN RESA_TAC
THEN EXISTS_TAC`--u:real^N`
THEN REPEAT RESA_TAC
THEN ASM_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`x':real^N`;`x'':real^N`])
THEN EXISTS_TAC`c:real`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`c % --u = --(c % u)/\ -- a - -- b= --(a-b:real^N)`]);;



let UNION_SYM_0=
prove(`IMAGE (\x:real^N. --x) (s UNION e) = (IMAGE (\x:real^N. --x) s) UNION (IMAGE (\x:real^N. --x) e)`,

SIMP_TAC[IMAGE_UNION]);;

let VEC0_SYM_0=
prove(`IMAGE (\x:real^N. --x) {vec 0}= {vec 0}`,

REWRITE_TAC[IMAGE;IN_ELIM_THM;IN_SING;VECTOR_ARITH`-- vec 0=vec 0`;EXTENSION]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;IN_SING;VECTOR_ARITH`-- vec 0=vec 0`;EXTENSION]
THEN EXISTS_TAC`vec 0:real^N`
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;IN_SING;VECTOR_ARITH`-- vec 0=vec 0`;EXTENSION]);;

let VEC0_UNION_SYM_0=
prove(`IMAGE (\x:real^N. --x) ({vec 0} UNION e) = {vec 0} UNION (IMAGE (\x:real^N. --x) e)`,

ASM_SIMP_TAC[UNION_SYM_0;VEC0_SYM_0]);;

let NOT_COLLINEAR_SYM_0=
prove(`~(collinear e) ==> ~(collinear (IMAGE (\x:real^N. --x) e))`,

REPEAT STRIP_TAC
THEN MRESA_TAC(GEN_ALL COLLINEAR_SYM_0)[`IMAGE (\x:real^N. --x) (e:real^N->bool)`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[REFL_SYM_0]);;

let VEC0_NOT_COLLINEAR_SYM_0=
prove(`~(collinear ({vec 0} UNION e)) ==> ~(collinear ({vec 0} UNION (IMAGE (\x:real^N. --x) e)))`,

REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL NOT_COLLINEAR_SYM_0)[`{vec 0} UNION (e:real^N->bool)`]
[VEC0_UNION_SYM_0]);;

let IMAGE_E_UNION_V_SYM_0=
prove(`e IN
      IMAGE (\i. {--vv i, --vv (SUC i)}) (:num) UNION
      {{v} | v IN IMAGE (\i. --vv i) (:num)}
==> IMAGE (\x:real^N. --x) e IN IMAGE (\i. {vv i, vv (SUC i)}) (:num) UNION
          {{v} | v IN IMAGE vv (:num)}`,

REWRITE_TAC[UNION;IN_ELIM_THM]
THEN MATCH_MP_TAC(SET_RULE`(A==>A1)/\ (B==>B1)==> (A\/B==> A1\/B1)`)
THEN ASM_SIMP_TAC[IMAGE_E_SYM_0]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN RESA_TAC
THEN REWRITE_TAC[IN_SING]
THEN EXISTS_TAC`(vv:num->real^N) x`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THENL[
EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[];
REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`-- -- A=A:real^N`]
THEN EXISTS_TAC`-- (vv:num->real^N) x`
THEN ASM_SIMP_TAC[VECTOR_ARITH`-- -- A=A:real^N`]]);;
let LINAER_SYM_0=
prove(`linear (\x:real^N. --x)`,

ASM_SIMP_TAC[VECTOR_ARITH`--(x+y)= -- x+ -- y:real^N`;linear]
THEN VECTOR_ARITH_TAC);;

let AFF_GE_COMMUTATIVE_SYM_0=
prove(`aff_ge (IMAGE (\x. --x) e1) (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_ge e1 e)`,

MATCH_MP_TAC AFF_GE_INJECTIVE_LINEAR_IMAGE
THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- x= -- y==> x=y:real^N`;LINAER_SYM_0]);;


let AFF_GE_VEC0_SYM_0=
prove(`aff_ge {vec 0} (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_ge {vec 0} e)`,

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM VEC0_SYM_0]
THEN ASM_SIMP_TAC[AFF_GE_COMMUTATIVE_SYM_0]);;


let AFF_GT_COMMUTATIVE_SYM_0=
prove(`aff_gt (IMAGE (\x. --x) e1) (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_gt e1 e)`,

MATCH_MP_TAC AFF_GT_INJECTIVE_LINEAR_IMAGE
THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- x= -- y==> x=y:real^N`;LINAER_SYM_0]);;


let AFF_GT_VEC0_SYM_0=
prove(`aff_gt {vec 0} (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_gt {vec 0} e)`,

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM VEC0_SYM_0]
THEN ASM_SIMP_TAC[AFF_GT_COMMUTATIVE_SYM_0]);;


let AFF_LE_COMMUTATIVE_SYM_0=
prove(`aff_le (IMAGE (\x. --x) e1) (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_le e1 e)`,

MATCH_MP_TAC AFF_LE_INJECTIVE_LINEAR_IMAGE
THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- x= -- y==> x=y:real^N`;LINAER_SYM_0]);;


let AFF_LE_VEC0_SYM_0=
prove(`aff_le {vec 0} (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_le {vec 0} e)`,

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM VEC0_SYM_0]
THEN ASM_SIMP_TAC[AFF_LE_COMMUTATIVE_SYM_0]);;

let AFF_LT_COMMUTATIVE_SYM_0=
prove(`aff_lt (IMAGE (\x. --x) e1) (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_lt e1 e)`,

MATCH_MP_TAC AFF_LT_INJECTIVE_LINEAR_IMAGE
THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- x= -- y==> x=y:real^N`;LINAER_SYM_0]);;


let AFF_LT_VEC0_SYM_0=
prove(`aff_lt {vec 0} (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_lt {vec 0} e)`,

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM VEC0_SYM_0]
THEN ASM_SIMP_TAC[AFF_LT_COMMUTATIVE_SYM_0]);;

let INTER_SYM_0=
prove(`IMAGE (\x:real^N. --x) (e1 INTER e2) =IMAGE (\x. --x) e1 INTER IMAGE (\x. --x) e2`,

MATCH_MP_TAC IMAGE_INTER_INJ
THEN ASM_REWRITE_TAC[]
THEN VECTOR_ARITH_TAC);;

let FAN_SYM_0=
prove_by_refinement(`FAN
      (vec 0, IMAGE (vv:num->real^3) (:num),
       IMAGE (\i. {vv i, vv (SUC i)}) (:num))
==> FAN
      (vec 0, IMAGE (\i. -- vv i) (:num),
       IMAGE (\i. {-- vv i, -- vv (SUC i)}) (:num))`,

[REWRITE_TAC[FAN;fan1;fan2;fan6;fan7]
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[UNIONS_IMAGE_FAN_SYM_0;IMAGE_V_SYM_0;SUBSET_SYM_0];

ASM_SIMP_TAC[GRAPH_SYM_0];

ASM_SIMP_TAC[IMAGE_V_SYM_0;FINITE_SYM_0];

POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[IMAGE_V_SYM_0;SUBSET_SYM_0;NOT_SUBSET_EMPTY_SYM_0];

POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[IMAGE_V_SYM_0;SUBSET_SYM_0;NOT_SUBSET_EMPTY_SYM_0]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL IN_SYM_0)[`vec 0:real^3`;`IMAGE (\x:real^3. --x) (IMAGE (vv:num->real^3) (:num))`][VECTOR_ARITH`-- vec 0= vec 0`;REFL_SYM_0];

POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL IMAGE_E_SYM_0)[`e:real^3->bool`;`vv:num->real^3`]
THEN REPLICATE_TAC (10-7)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC th[`IMAGE (\x:real^3. --x) e`])
THEN MRESAL_TAC(GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`IMAGE (\x:real^3. --x) e`][REFL_SYM_0];

MRESA_TAC (GEN_ALL IMAGE_E_UNION_V_SYM_0)[`e1:real^3->bool`;`vv:num->real^3`]
THEN MRESA_TAC (GEN_ALL IMAGE_E_UNION_V_SYM_0)[`e2:real^3->bool`;`vv:num->real^3`]
THEN REPLICATE_TAC (12-8)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`IMAGE (\x:real^3. --x) e1`;`IMAGE (\x:real^3. --x) e2`][])
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[AFF_GE_VEC0_SYM_0;GSYM INTER_SYM_0]
THEN MRESAL_TAC(GEN_ALL SET_EQ_SYM_0)[`IMAGE (\x:real^3. --x) (aff_ge {vec 0} e1 INTER aff_ge {vec 0} e2)`;`IMAGE (\x:real^3. --x) (aff_ge {vec 0} (e1 INTER e2))`][REFL_SYM_0]]);;





let OPP_SUC_MOD=
prove(`~(k=0)==>k - SUC ((k - SUC (x MOD k)) MOD k) = x MOD k`
,

RESA_TAC
THEN MRESA_TAC DIVISION[`k- SUC(x MOD k)`;`k:num`]
THEN MRESA_TAC DIVISION[`x:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`x MOD k < k ==> k- SUC(x MOD k)<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k- SUC(x MOD k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`x MOD k < k /\ (k - SUC (x MOD k)) MOD k < k
==> (k - SUC ((k - SUC (x MOD k)) MOD k) = x MOD k)
<=> k -SUC( x MOD k) = (k - SUC (x MOD k)) MOD k`)
THEN RESA_TAC);;


let OPP_IMAGE_V_EQ=
prove(`periodic vv k/\ ~(k=0)
==>
IMAGE (\i. vv (k - SUC (i MOD k))) (:num)= IMAGE vv (:num)`,


REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`k - SUC (x' MOD k)`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];
RESA_TAC
THEN EXISTS_TAC`k- SUC(x' MOD k)`
THEN ASM_SIMP_TAC[OPP_SUC_MOD;SET_RULE`(a:num)IN (:num)`;PERIODIC_PROPERTY]]);;

let MOD_SUC_MOD=
prove(`1<k==> SUC (x MOD k) MOD k= SUC x MOD k`,

STRIP_TAC
THEN REWRITE_TAC[ADD1]
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_ADD_MOD[`x:num`;`1:num`;`k:num`]);;
let SUC_MOD_EQ_MOD_SUC=
prove(`1<k==>(k - SUC (x MOD k)) MOD k =(k - SUC x MOD k) MOD k`,

STRIP_TAC
THEN REWRITE_TAC[ADD1]
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)/\ k - (k - 1 + 1)=0/\ k - 1 + 1=k/\ k-k=0/\ 0<k/\ k-0=k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_ADD_MOD[`x:num`;`1:num`;`k:num`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MRESA_TAC MOD_LT[`0`;`k:num`]
THEN MRESA_TAC DIVISION[`x:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`0:num`][ARITH_RULE`1*k+0=k`]
THEN MP_TAC(ARITH_RULE`x MOD k< k/\ 1<k==> x MOD k= k-1\/ x MOD k +1< k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`x MOD k +1`;`k:num`]);;




let OPP_IMAGE_E_EQ=
prove(`periodic (vv:num->real^3) k/\ 1<k
==>
IMAGE (\i. {vv (k - SUC (i MOD k)), vv (k - SUC (SUC i MOD k))}) (:num)
=IMAGE (\i. {vv i, vv (SUC i)}) (:num)`,

ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD]
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`]
THEN MRESA_TAC th[`k - SUC x' MOD k`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC];
RESA_TAC
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`]
THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k<k ==> SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]
THEN MRESA_TAC th[`SUC x'`])
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]]);;
let OPP_IMAGE_F_EQ=
prove(`periodic (vv:num->real^3) k/\ 1<k
==>
IMAGE (\i.  vv (k - SUC (SUC i MOD k)),vv (k - SUC (i MOD k))) (:num)
=IMAGE (\i. vv i, vv (SUC i)) (:num)`,

ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD]
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`]
THEN MRESA_TAC th[`k - SUC x' MOD k`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC];
RESA_TAC
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`]
THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k<k ==> SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]
THEN MRESA_TAC th[`SUC x'`])
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]]);;

let OPP_IMAGE_F_EQ2=
prove(`periodic (vv:num->real^3) k/\ 1<k
==>
IMAGE (\i.  vv (k - SUC (i MOD k)),vv (k - SUC (SUC i MOD k))) (:num)
=IMAGE (\i. vv (SUC i),vv i ) (:num)`,

ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD]
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`]
THEN MRESA_TAC th[`k - SUC x' MOD k`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC];
RESA_TAC
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`]
THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k<k ==> SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]
THEN MRESA_TAC th[`SUC x'`])
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]]);;

let BALL_ANNULUS_SYM_0=
prove(`-- v IN ball_annulus <=> v IN ball_annulus`,

ASM_SIMP_TAC[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- A= -- A/\ -- --A=A`;NORM_NEG]);;

let DIST_SYM_0=
prove(`dist(-- a, -- b)= dist(a,b:real^N)`,

ASM_SIMP_TAC[dist;VECTOR_ARITH`--a - --b= --(a-b):real^N`;NORM_NEG]);;

let OPP_FAN_SYM_0=
prove(` 3<=k /\ 
periodic vv k /\
FAN
      (vec 0, IMAGE (vv:num->real^3) (:num),
       IMAGE (\i. {vv i, vv (SUC i)}) (:num))
==> FAN
 (vec 0,IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
  IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num))`,

STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL OPP_IMAGE_E_EQ)[`k:num`;`vv:num->real^3`]
THEN MRESA_TAC(GEN_ALL OPP_IMAGE_V_EQ)[`k:num`;`vv:num->real^3`]
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[FAN_SYM_0]);;


let ORD_PAIRS_E_VV=
prove(`ord_pairs (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
=IMAGE (\i. vv i, vv (SUC i)) (:num) UNION IMAGE (\i.  vv (SUC i),vv i) (:num)
`,

ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[ord_pairs;IMAGE;IN_ELIM_THM;UNION;SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN SET_TAC[]);;

let SELF_PAIR_EMPTY_VV=
prove(`self_pairs (IMAGE (\i. {(vv:num->real^N) i, vv (SUC i)}) (:num)) (IMAGE vv (:num))={}`,

REWRITE_TAC[SET_RULE`A={}<=> ~(?a. a IN A)`;self_pairs;IN_ELIM_THM;EE;IMAGE]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM (fun th-> STRIP_TAC
THEN MP_TAC th
THEN ASM_REWRITE_TAC[])
THEN EXISTS_TAC`(vv:num->real^N) (SUC x)`
THEN EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[]);;

let DART_OF_HYP_VV=
prove(`darts_of_hyp (IMAGE (\i. {(vv:num->real^N) i, vv (SUC i)}) (:num)) (IMAGE vv (:num))
= IMAGE (\i. vv i, vv (SUC i)) (:num) UNION IMAGE (\i.  vv (SUC i),vv i) (:num)`,

ASM_SIMP_TAC[darts_of_hyp;SELF_PAIR_EMPTY_VV;ORD_PAIRS_E_VV]
THEN SET_TAC[]);;

let PAIR_FUN_SYM_0=
prove(`IMAGE (\i. -- vv1 i, -- vv2 i) (:num)
= IMAGE(\(x:real^N,y:real^N). --x, --y) (IMAGE (\i. vv1 i, vv2 i) (:num))`,

REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THENL[
EXISTS_TAC` (vv1 :num->real^N) x', (vv2 :num->real^N) x'`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`x'':num`
THEN ASM_REWRITE_TAC[]]);;

let IN_PAIR_SYM_0=
prove(`a IN A==>  (\(x:real^N,y:real^N). --x, --y) a IN IMAGE(\(x:real^N,y:real^N). --x, --y) A`,

ASM_SIMP_TAC[FUN_IN_IMAGE]);;
let ID_SYM_0_PRIME=
prove(`(\(x:real^N,y). --x,--y) ((\(x,y). --x,--y) (a:real^N,b:real^N))
= (a,b)` ,

ASM_REWRITE_TAC[VECTOR_ARITH`-- -- a= a:real^N`]);;

let ID_SYM_0=
prove(`(\(x:real^N,y). --x,--y) ((\(x,y). --x,--y) x)
= (x:real^N#real^N)`,

MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- -- a= a:real^N`]);;

let ID_PAIR_SYM_0=
prove(`IMAGE (\(x,y):real^N#real^N. --x,--y) (IMAGE (\(x,y). --x,--y) A)=A`,

REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN ASM_SIMP_TAC[ID_SYM_0]
THEN 
EXISTS_TAC`(\(x,y):real^N#real^N. --x,--y) x`
THEN ASM_SIMP_TAC[ID_SYM_0] 
THEN EXISTS_TAC`x:real^N#real^N`
THEN ASM_REWRITE_TAC[]);;

let IN_EQ_PAIR_SYM_0=
prove(`  (\(x:real^N,y:real^N). --x, --y) a IN IMAGE(\(x:real^N,y:real^N). --x, --y) A<=> a IN A`,

EQ_TAC
THENL[
STRIP_TAC
THEN MRESAL_TAC (GEN_ALL IN_PAIR_SYM_0)[`(\(x:real^N,y:real^N). --x,--y) a`;`IMAGE(\(x:real^N,y:real^N). --x, --y) A`][ID_PAIR_SYM_0;ID_SYM_0];
ASM_SIMP_TAC[FUN_IN_IMAGE];]);;


let FST_SND_PAIR_SYM_0=
prove(`FST ((\(x,y):real^N#real^N. --x,--y) x)= -- FST x
/\ SND ((\(x,y):real^N#real^N. --x,--y) x)= -- SND x`,

MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN REWRITE_TAC[]);;

let EQ_SET_PAIR_SYM_0=
prove(`IMAGE (\(x,y):real^N#real^N. --x,--y) A =IMAGE (\(x,y). --x,--y) B <=> A=B`,

EQ_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN SIMP_TAC[EXTENSION;IN_EQ_PAIR_SYM_0]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[` (\(x,y):real^N#real^N. --x,--y) x:real^N#real^N`][IN_EQ_PAIR_SYM_0]));;

let EE_SYM_0=
prove_by_refinement(`EE (--a) (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))
= IMAGE(\x:real^N. --x)(EE (a) (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
)`,

[REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[EE;IMAGE;IN_ELIM_THM;SET_RULE`{a,b}={c,d}<=> (a=c/\b=d)\/ (a=d/\ b=c)`;VECTOR_ARITH`--a= --b<=> a=b:real^N`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;
EXISTS_TAC`(vv:num->real^N) (SUC x')`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`(vv:num->real^N) (x')`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`(x'':num)`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`(x'':num)`
THEN ASM_REWRITE_TAC[]]);;
let EMPTY_EQ_SYM_0=
prove(`
(IMAGE (\x:real^N. --x) A = {})
<=> (A ={})`,

EQ_TAC
THENL[
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM]
THEN ASM_SIMP_TAC[NOT_EMPTY_SYM_0];
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM]
THEN MRESAL_TAC (GEN_ALL NOT_EMPTY_SYM_0)[`IMAGE (\x. --x) (A:real^N->bool)`][REFL_SYM_0];]);;

let EE_EXPAND_BB_VV=
prove_by_refinement(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==> EE (vv i) E= {vv (SUC i),vv (i+k-1)}`,

[
REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN ASM_TAC
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[convex_local_fan]
THEN STRIP_TAC
THEN SUBGOAL_THEN`(vv:num->real^3) i IN V` ASSUME_TAC;
EXPAND_TAC"V"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`];
MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`(vv:num->real^3) i`]
THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<k`)
THEN RESA_TAC
THEN MP_TAC Odxlstcv2.CARD_V_EQ_SCS_K1
THEN ASM_REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan]
THEN RESA_TAC
THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) i`])
THEN 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`;`(vv:num->real^3) i:real^3`;`vv:num->real^3`;`i:num`]
[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`SUC 0`][ITER;ARITH_RULE`SUC 0 +i= SUC i`] THEN MRESA_TAC th[`k-1`])
THEN REWRITE_TAC[ARITH_RULE`k-1+i= i+k-1`]]);;




let AZIM_CYCLE1_SYM_0=
prove(`
scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
azim_cycle (IMAGE (\x. --x) (EE (vv i) E)) (vec 0) (--vv i) (--vv (SUC i)) =
 --azim_cycle (EE (vv i) E) (vec 0) (vv i) (vv (SUC i))`,

RESA_TAC
THEN MP_TAC EE_EXPAND_BB_VV
THEN RESA_TAC
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]);;


let AZIM_CYCLE2_SYM_0=
prove(`
scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
azim_cycle (IMAGE (\x. --x) (EE (vv i) E)) (vec 0) (--vv i) (--vv (i + k-1)) =
 --azim_cycle (EE (vv i) E) (vec 0) (vv i) (vv (i+k-1))`,

RESA_TAC
THEN MP_TAC EE_EXPAND_BB_VV
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]);;



let IVS_AZIM_CYCLE_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
/\ x IN darts_of_hyp E V
==> ivs_azim_cycle
       (EE (--SND x) (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))
       (vec 0)
       (--SND x)
       (--FST x)
= -- ivs_azim_cycle (EE (SND x) E) (vec 0) (SND x) (FST x)`,

[
RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN EXPAND_TAC"FF"
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM;IMAGE]
THEN REWRITE_TAC[IN_ELIM_THM]
THEN RESA_TAC;
MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`]
THEN ASM_SIMP_TAC[EE_SYM_0]
THEN SUBGOAL_THEN`vv (SUC x' + k - 1) = (vv:num->real^3) x'`ASSUME_TAC;

MP_TAC(ARITH_RULE`~(k<=3)==> SUC x' + k - 1= x' +k`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;periodic]
THEN REPEAT RESA_TAC;

ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0];

MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`x':num`;`k:num`]
THEN ASM_SIMP_TAC[EE_SYM_0]
THEN ASM_SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]]);;

let ff_FUN_COMMUTATIVE_SYM_0=
prove(` 
scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==> (!x. ff_of_hyp
 (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))
 ((\(x,y). --x,--y) x) =
 (\(x,y). --x,--y) (ff_of_hyp (vec 0,V,E) x))
`,

RESA_TAC
THEN GEN_TAC
THEN ASM_SIMP_TAC[ff_of_hyp2;DART_OF_HYP_VV;PAIR_FUN_SYM_0;IN_EQ_PAIR_SYM_0;GSYM IMAGE_UNION;FST_SND_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`x IN darts_of_hyp (E:(real^3->bool)->bool) V \/ ~(x IN darts_of_hyp E V)`)
THEN RESA_TAC
THENL[
POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN RESA_TAC
THEN MP_TAC IVS_AZIM_CYCLE_SYM_0
THEN RESA_TAC;

POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN RESA_TAC]);;
let FUN_COMMUTATIVE=
prove(`(!x. f(g x)= g(f1 x))
==> !n x. (f POWER n) (g x) = g((f1 POWER n) x)`,

STRIP_TAC
THEN INDUCT_TAC
THENL[
ASM_REWRITE_TAC[POWER;I_DEF];
ASM_REWRITE_TAC[POWER;o_DEF]]);;

let ff_POWER_COMMUTATIVE_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==> 
!n x. (ff_of_hyp
   (vec 0,
    IMAGE (\i. --vv i) (:num),
    IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)) POWER
   n)
  ((\(x,y). --x,--y) x)
= (\(x,y). --x,--y) ( (ff_of_hyp (vec 0,IMAGE vv (:num),IMAGE (\i. {vv i, vv (SUC i)}) (:num)) POWER
   n)
  x)
`,

RESA_TAC
THEN MATCH_MP_TAC FUN_COMMUTATIVE
THEN MATCH_MP_TAC ff_FUN_COMMUTATIVE_SYM_0
THEN ASM_REWRITE_TAC[]);;


let FACE_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
face
 (hypermap
 (HYP
 (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))
 ((\(x,y). --x,--y) x) =
 IMAGE (\(x,y). --x,--y) (face (hypermap (HYP (vec 0,V,E))) x)`,

STRIP_TAC
THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;]
THEN REPEAT RESA_TAC
THEN MP_TAC FAN_SYM_0
THEN RESA_TAC
THEN REWRITE_TAC[face]
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;]
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;]
THEN GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV)[IMAGE]
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THENL[
EXISTS_TAC`(ff_of_hyp (vec 0,V,E) POWER n) x`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`n:num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`n:num`
THEN ASM_REWRITE_TAC[]]);;



let OPP_IMAGE_V_EQ_NEG=
prove(`periodic vv k/\ ~(k=0)
==>
IMAGE (\i. -- (vv:num->real^3) (k - SUC (i MOD k))) (:num)= IMAGE (\i. -- vv i) (:num)`,


REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`k - SUC (x' MOD k)`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];
RESA_TAC
THEN EXISTS_TAC`k- SUC(x' MOD k)`
THEN ASM_SIMP_TAC[OPP_SUC_MOD;SET_RULE`(a:num)IN (:num)`;PERIODIC_PROPERTY]]);;


let OPP_IMAGE_E_EQ_NEG=
prove(`periodic (vv:num->real^3) k/\ 1<k
==>
IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)
=IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)`,

ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD]
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`]
THEN MRESA_TAC th[`k - SUC x' MOD k`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC];
RESA_TAC
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`]
THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k<k ==> SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]
THEN MRESA_TAC th[`SUC x'`])
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]]);;

let OPP_IMAGE_F_EQ_NEG=
prove(`periodic (vv:num->real^3) k/\ 1<k
==>
IMAGE (\i.  --vv (k - SUC (SUC i MOD k)),--vv (k - SUC (i MOD k))) (:num)
=IMAGE (\i. --vv i, --vv (SUC i)) (:num)`,

ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD]
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`]
THEN MRESA_TAC th[`k - SUC x' MOD k`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC];
RESA_TAC
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`]
THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k<k ==> SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]
THEN MRESA_TAC th[`SUC x'`])
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]]);;


let OPP_IMAGE_F_EQ2_NEG=
prove(`periodic (vv:num->real^3) k/\ 1<k
==>
IMAGE (\i.  --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num)
=IMAGE (\i. --vv (SUC i),--vv i ) (:num)`,

ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD]
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`]
THEN MRESA_TAC th[`k - SUC x' MOD k`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC];
RESA_TAC
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)
THEN RESA_TAC
THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))`
THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`]
THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k<k ==> SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`]
THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`]
THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]
THEN MRESA_TAC th[`SUC x'`])
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]]);;



let CARD_PAIR_SYM_0=
prove(`FINITE s ==> CARD (IMAGE (\(x,y):real^N#real^N. --x,--y) s) =CARD s`,

STRIP_TAC
THEN MATCH_MP_TAC CARD_IMAGE_INJ
THEN RESA_TAC
THEN RESA_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`;PAIR_EQ]
THEN MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN MP_TAC(SET_RULE`y=(FST (y:real^N#real^N),SND (y:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`;PAIR_EQ]
THEN ASM_REWRITE_TAC[GSYM PAIR_EQ]
THEN RESA_TAC);;



let FACE_ALL_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
(!x. face
 (hypermap
 (HYP
 (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))
 ((\(x,y). --x,--y) x) =
 IMAGE (\(x,y). --x,--y) (face (hypermap (HYP (vec 0,V,E))) x))`,

REPEAT STRIP_TAC
THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;]
THEN REPEAT RESA_TAC
THEN MP_TAC FAN_SYM_0
THEN RESA_TAC
THEN REWRITE_TAC[face]
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;]
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;]
THEN GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV)[IMAGE]
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THENL[
EXISTS_TAC`(ff_of_hyp (vec 0,V,E) POWER n) x`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`n:num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`n:num`
THEN ASM_REWRITE_TAC[]]);;



let AZIM_CYCLE_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
/\ x IN darts_of_hyp E V
==> azim_cycle
       (EE (--SND x) (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))
       (vec 0)
       (--SND x)
       (--FST x)
= -- azim_cycle (EE (SND x) E) (vec 0) (SND x) (FST x)`,

[RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN EXPAND_TAC"FF"
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM;IMAGE]
THEN REWRITE_TAC[IN_ELIM_THM]
THEN RESA_TAC;

MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`]
THEN ASM_SIMP_TAC[EE_SYM_0]
THEN SUBGOAL_THEN`vv (SUC x' + k - 1) = (vv:num->real^3) x'`ASSUME_TAC;

MP_TAC(ARITH_RULE`~(k<=3)==> SUC x' + k - 1= x' +k`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;periodic]
THEN REPEAT RESA_TAC;

ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0];

MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`x':num`;`k:num`]
THEN ASM_SIMP_TAC[EE_SYM_0]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]
]);;




let FST_SND_EQ_PAIR_SYM_0=
prove(`(\(x,y):real^N#real^N. --x,--y)x= --FST x,--SND x`,

 MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN REWRITE_TAC[]);;


let SYM_AZIM_CYCLE_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
/\ x IN darts_of_hyp E V
==> azim_cycle
       (EE (--FST x) (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))
       (vec 0)
       (--FST x)
       (--SND x)
= -- azim_cycle (EE (FST x) E) (vec 0) (FST x) (SND x)`,

[RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN EXPAND_TAC"FF"
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM;IMAGE]
THEN REWRITE_TAC[IN_ELIM_THM]
THEN RESA_TAC;

MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`x':num`;`k:num`]
THEN ASM_SIMP_TAC[EE_SYM_0]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0];
MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`]
THEN ASM_SIMP_TAC[EE_SYM_0]
THEN SUBGOAL_THEN`vv (SUC x' + k - 1) = (vv:num->real^3) x'`ASSUME_TAC;


MP_TAC(ARITH_RULE`~(k<=3)==> SUC x' + k - 1= x' +k`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;periodic]
THEN REPEAT RESA_TAC;

ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0];
]);;

let NODE_MAP_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
(!x. (node_map
 (hypermap
 (HYP
 (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
((\(x,y). --x,--y) x)
= (\(x,y). --x,--y) (node_map (hypermap (HYP (vec 0,V,E))) x))`,

STRIP_TAC
THEN GEN_TAC
THEN POP_ASSUM(fun th->
MP_TAC th
THEN ASSUME_TAC th
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;]
THEN REPEAT RESA_TAC
)
THEN ASM_TAC
THEN REPEAT RESA_TAC
THEN MP_TAC FAN_SYM_0
THEN RESA_TAC
THEN ASM_SIMP_TAC[Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;FUN_EQ_THM]
THEN MP_TAC(SET_RULE`x=(FST (x:real^3#real^3),SND (x:real^3#real^3))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN ASM_SIMP_TAC[nn_of_hyp;]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN STRIP_TAC
THEN ASM_SIMP_TAC[ff_of_hyp2;DART_OF_HYP_VV;PAIR_FUN_SYM_0;IN_EQ_PAIR_SYM_0;GSYM IMAGE_UNION;FST_SND_PAIR_SYM_0;Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP]
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN ASM_SIMP_TAC[GSYM FST_SND_EQ_PAIR_SYM_0;IN_EQ_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`x IN FF UNION IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num)
\/ ~(x IN FF UNION IMAGE (\i. vv (SUC i),vv i) (:num))`)
THEN RESA_TAC
THEN MP_TAC SYM_AZIM_CYCLE_SYM_0
THEN RESA_TAC);;


let IMAGE_NODE_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
(!A. IMAGE (node_map
 (hypermap
 (HYP
 (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
(IMAGE (\(x,y). --x,--y) A)
= IMAGE (\(x,y). --x,--y) (IMAGE (node_map (hypermap (HYP (vec 0,V,E)))) A))`,

RESA_TAC
THEN GEN_TAC
THEN ONCE_REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THENL[
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o  DEPTH_CONV)[IMAGE;IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MP_TAC NODE_MAP_SYM_0
THEN RESA_TAC
THEN EXISTS_TAC`node_map (hypermap (HYP (vec 0,V,E))) x''`
THEN ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`x'':real^3#real^3`
THEN ASM_REWRITE_TAC[];

POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o  DEPTH_CONV)[IMAGE;IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MP_TAC NODE_MAP_SYM_0
THEN RESA_TAC
THEN EXISTS_TAC`(\(x,y):real^3#real^3. --x,--y) x''`
THEN ASM_REWRITE_TAC[]
THEN ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`x'':real^3#real^3`
THEN ASM_REWRITE_TAC[]]);;


let COMMUTATIVE_POINT_PAIR_0=
prove(`(\(x,y):real^N#real^N. --x,--y) a= b <=> a= (\(x,y). --x,--y) b `,

EQ_TAC
THENL[
STRIP_TAC
THEN MRESA_TAC(GEN_ALL ID_SYM_0)[`a:real^N#real^N`];
STRIP_TAC
THEN MRESA_TAC(GEN_ALL ID_SYM_0)[`b:real^N#real^N`]]);;

let EDGE_MAP_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
(!x. (edge_map
 (hypermap
 (HYP
 (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
((\(x,y). --x,--y) x)
= (\(x,y). --x,--y) (edge_map (hypermap (HYP (vec 0,V,E))) x))`,

STRIP_TAC
THEN GEN_TAC
THEN POP_ASSUM(fun th->
MP_TAC th
THEN ASSUME_TAC th
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;]
THEN REPEAT RESA_TAC
)
THEN ASM_TAC
THEN REPEAT RESA_TAC
THEN MP_TAC FAN_SYM_0
THEN RESA_TAC
THEN ASM_SIMP_TAC[Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;FUN_EQ_THM]
THEN MP_TAC(SET_RULE`x=(FST (x:real^3#real^3),SND (x:real^3#real^3))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN ASM_SIMP_TAC[ee_of_hyp;]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN STRIP_TAC
THEN ASM_SIMP_TAC[ff_of_hyp2;DART_OF_HYP_VV;PAIR_FUN_SYM_0;IN_EQ_PAIR_SYM_0;GSYM IMAGE_UNION;FST_SND_PAIR_SYM_0;Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP]
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN ASM_SIMP_TAC[GSYM FST_SND_EQ_PAIR_SYM_0;IN_EQ_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`x IN FF UNION IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num)
\/ ~(x IN FF UNION IMAGE (\i. vv (SUC i),vv i) (:num))`)
THEN RESA_TAC);;


let EDGE_POWER_MAP_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
(!n x. (edge_map
 (hypermap
 (HYP
 (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))) POWER n)
((\(x,y). --x,--y) x)
= (\(x,y). --x,--y) ((edge_map (hypermap (HYP (vec 0,V,E))) POWER n) x))`,

RESA_TAC
THEN MATCH_MP_TAC FUN_COMMUTATIVE
THEN MATCH_MP_TAC EDGE_MAP_SYM_0
THEN ASM_REWRITE_TAC[]);;

let NODE_POWER_MAP_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==>
(!n x. (node_map
 (hypermap
 (HYP
 (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))) POWER n)
((\(x,y). --x,--y) x)
= (\(x,y). --x,--y) ((node_map (hypermap (HYP (vec 0,V,E))) POWER n) x))`,

RESA_TAC
THEN MATCH_MP_TAC FUN_COMMUTATIVE
THEN MATCH_MP_TAC NODE_MAP_SYM_0
THEN ASM_REWRITE_TAC[]);;




let LOCAL_FAN_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==> local_fan
 (IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
  IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num),
  IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--vv (k - SUC (i MOD k))) (:num))`,

[


STRIP_TAC
THEN POP_ASSUM(fun th-> 
MP_TAC th
THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<=k/\ 1<k`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[local_fan;LET_DEF;LET_END_DEF;OPP_FAN_SYM_0]
THEN ASSUME_TAC th)
;


REPLICATE_TAC (16-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (15-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC (SYM th))
THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (vv:num->real^3) (:num)`][DART_OF_HYP_VV]
THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN MP_TAC OPP_FAN_SYM_0
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`][DART_OF_HYP_VV]
THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN ASM_SIMP_TAC[IN_ELIM_THM;PAIR_FUN_SYM_0;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2]
THEN GEN_REWRITE_TAC(RAND_CONV o LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`(\(x:real^3,y:real^3). --x,--y) x`
THEN ASM_SIMP_TAC[UNION;IN_ELIM_THM;IN_PAIR_SYM_0;]
THEN MP_TAC FACE_SYM_0
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG]
;




REPLICATE_TAC (16-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (15-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC (SYM th))
THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (vv:num->real^3) (:num)`][DART_OF_HYP_VV]
THEN MP_TAC OPP_FAN_SYM_0
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`][DART_OF_HYP_VV] 
THEN ASM_SIMP_TAC[IN_ELIM_THM;PAIR_FUN_SYM_0;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2]
THEN GEN_REWRITE_TAC(RAND_CONV o LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[dih2k]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN REPEAT STRIP_TAC;




MRESA_TAC Hypermap.node_map_and_darts[`hypermap
      (HYP
      (vec 0,
       IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i.  (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`]
THEN REPLICATE_TAC (28-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[SYM th]);




ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC
THEN MP_TAC FACE_ALL_SYM_0
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y):real^3#real^3. --x,--y) x'`][ID_SYM_0])
THEN MP_TAC IMAGE_NODE_SYM_0
THEN RESA_TAC
THEN ASM_SIMP_TAC[GSYM IMAGE_UNION]
THEN MRESA_TAC (GEN_ALL IN_EQ_PAIR_SYM_0)[`x':real^3#real^3`;`IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)))
      (:num) UNION
      IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--(vv:num->real^3) (k - SUC (i MOD k)))
      (:num)`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;ID_PAIR_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B= B UNION A`]
THEN STRIP_TAC
THEN REPLICATE_TAC (28-13)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN MRESA_TAC th[`((\(x,y):real^3#real^3. --x,--y) x')`]
)
THEN SET_TAC[]
;



REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x.
          ITER n
          (ff_of_hyp
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))
          (x) =
          (\(x,y). --x,--y) (ITER n (ff_of_hyp (vec 0,V,E)) ((\(x,y). --x,--y) x))`
ASSUME_TAC;



REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;


MP_TAC FAN_SYM_0
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;]
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][]
THEN MRESA_TAC Hypermap.node_map_and_darts[`hypermap
      (HYP
      (vec 0,
       IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i.  (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (39-14)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;




REPLICATE_TAC (43-39)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);



REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC EDGE_POWER_MAP_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x. ITER n
          (edge_map
          (hypermap
          (HYP
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
          (x) =
          (\(x,y). --x,--y)
          (ITER n (edge_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))`
ASSUME_TAC;



REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;


ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (26-15)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;



REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);






REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC NODE_POWER_MAP_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x. ITER n
          (node_map
          (hypermap
          (HYP
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
          (x) =
          (\(x,y). --x,--y)
          (ITER n (node_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))`
ASSUME_TAC;



REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;


ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (26-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;



REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);





(*******)
MRESA_TAC Hypermap.node_map_and_darts[`hypermap
      (HYP
      (vec 0,
       IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i.  (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`]
THEN REPLICATE_TAC (28-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[SYM th]);




ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC
THEN MP_TAC FACE_ALL_SYM_0
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y):real^3#real^3. --x,--y) x'`][ID_SYM_0])
THEN MP_TAC IMAGE_NODE_SYM_0
THEN RESA_TAC
THEN ASM_SIMP_TAC[GSYM IMAGE_UNION]
THEN MRESA_TAC (GEN_ALL IN_EQ_PAIR_SYM_0)[`x':real^3#real^3`;`IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)))
      (:num) UNION
      IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--(vv:num->real^3) (k - SUC (i MOD k)))
      (:num)`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;ID_PAIR_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B= B UNION A`]
THEN STRIP_TAC
THEN REPLICATE_TAC (28-13)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN MRESA_TAC th[`((\(x,y):real^3#real^3. --x,--y) x')`]
)
THEN SET_TAC[]
;



REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x.
          ITER n
          (ff_of_hyp
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))
          (x) =
          (\(x,y). --x,--y) (ITER n (ff_of_hyp (vec 0,V,E)) ((\(x,y). --x,--y) x))`
ASSUME_TAC;



REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;


MP_TAC FAN_SYM_0
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;]
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][]
THEN MRESA_TAC Hypermap.node_map_and_darts[`hypermap
      (HYP
      (vec 0,
       IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i.  (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (39-14)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;




REPLICATE_TAC (43-39)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);



REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC EDGE_POWER_MAP_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x. ITER n
          (edge_map
          (hypermap
          (HYP
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
          (x) =
          (\(x,y). --x,--y)
          (ITER n (edge_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))`
ASSUME_TAC;



REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;


ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (26-15)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;



REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);






REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC NODE_POWER_MAP_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x. ITER n
          (node_map
          (hypermap
          (HYP
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
          (x) =
          (\(x,y). --x,--y)
          (ITER n (node_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))`
ASSUME_TAC;



REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;


ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (26-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;



REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);




]);;




let POINT_IN_AFF_LT_SYM_0=
prove(` DISJOINT {vec 0,v1} {w2}
==> 
-- w2 IN aff_lt {vec 0,v1} {w2}`,

STRIP_TAC
THEN ASM_SIMP_TAC[AFF_LT_2_1;IN_ELIM_THM]
THEN EXISTS_TAC`&2`
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`-- &1`
THEN REWRITE_TAC[REAL_ARITH`-- &1< &0/\ &2 + &0 + -- &1 = &1`]
THEN VECTOR_ARITH_TAC);;

let COLLINEAR_POINT_SYM_0=
prove(`~collinear {vec 0, v1, w1} ==> ~collinear {vec 0, v1, --w1}`,

REWRITE_TAC[COLLINEAR_LEMMA;IMAGE;IN_ELIM_THM;VECTOR_ARITH`-- a= vec 0<=> a= vec 0`]
THEN RESA_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MP_TAC th 
THEN ASM_REWRITE_TAC[])
THEN MATCH_MP_TAC(SET_RULE`A==> B\/C\/A`)
THEN EXISTS_TAC`--c:real`
THEN POP_ASSUM MP_TAC
THEN VECTOR_ARITH_TAC);;

let AZIM_EQ_PI_POINT_SYM_0=
prove(`~collinear {vec 0, v1, w1:real^3}
==> azim (vec 0) v1  w1 (--w1) = pi`,

STRIP_TAC
THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`v1:real^3`;`w1:real^3`]
THEN ASM_SIMP_TAC[AZIM_EQ_PI]
THEN MRESAL_TAC (GEN_ALL POINT_IN_AFF_LT_SYM_0)[`v1:real^3`;`-- w1:real^3`][VECTOR_ARITH`-- --A=A:real^3`]
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_SIMP_TAC[Fan.th3a]);;


let SUM_AZIM_SYM_0=
prove(`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2}
/\ azim (vec 0) v1 w1 w2<= pi
==>  azim (vec 0) v1 w1 w2 + azim (vec 0) v1  w2 (--w1) = pi `,

REPEAT STRIP_TAC
THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`v1:real^3`;`w1:real^3`]
THEN MRESA_TAC(GEN_ALL AZIM_EQ_PI_POINT_SYM_0)[`v1:real^3`;`w1:real^3`]
THEN MRESA_TAC Fan.sum4_azim_fan[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`;`--w1:real^3`]);;


let SUM_AZIM_SYM_0=
prove(`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2}
/\ azim (vec 0) v1 w1 w2<= pi
==>  azim (vec 0) v1 w1 w2 + azim (vec 0) v1  w2 (--w1) = pi `,

REPEAT STRIP_TAC
THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`v1:real^3`;`w1:real^3`]
THEN MRESA_TAC(GEN_ALL AZIM_EQ_PI_POINT_SYM_0)[`v1:real^3`;`w1:real^3`]
THEN MRESA_TAC Fan.sum4_azim_fan[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`;`--w1:real^3`]);;



let AZIM_EQ_LE_SYM_0=
prove(`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2}
/\ azim (vec 0) v1 w1 w2<= pi
==>  azim (vec 0) v1  (--w1) (--w2)=azim (vec 0) v1 w1 w2   `,

STRIP_TAC
THEN MP_TAC SUM_AZIM_SYM_0
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) v1 w1 w2/\ azim (vec 0) v1 w1 w2 + azim (vec 0) v1 w2 (--w1) = pi
==>  azim (vec 0) v1 w2 (--w1) <= pi`)
THEN ASM_SIMP_TAC[azim]
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`v1:real^3`;`w1:real^3`]
THEN MRESA_TAC (GEN_ALL SUM_AZIM_SYM_0)[`v1:real^3`;`--w1:real^3`;`w2:real^3`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;

let AZIM_LE_PI_SYM_0=
prove(`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2}
/\ azim (vec 0) v1 w1 w2<= pi
==>   azim (vec 0) v1  (--w1) (--w2) <= pi`,

REPEAT STRIP_TAC
THEN MP_TAC AZIM_EQ_LE_SYM_0
THEN RESA_TAC);;



let EQUI_FF_SYM_0=
prove(`!(x:real^N#real^N). (SND x, FST x)IN IMAGE (\i. vv (SUC i),vv i) (:num) <=> x IN IMAGE (\i. vv i,vv (SUC i)) (:num)`,

REWRITE_TAC[IMAGE;IN_ELIM_THM;PAIR_EQ]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THENL[
EXISTS_TAC`x':num`
THEN ASM_SIMP_TAC[]
THEN MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN REWRITE_TAC[PAIR_EQ]
THEN ASM_SIMP_TAC[];
POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN REWRITE_TAC[PAIR_EQ]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`x':num`
THEN ASM_SIMP_TAC[]]);;


let CARD_EQUI_FF_SYM_0=
prove(`FINITE (IMAGE (\i. vv i,vv (SUC i)) (:num))
==>
CARD (IMAGE (\i. (vv:num->real^N) (SUC i),vv i) (:num))= CARD (IMAGE (\i. vv i,vv (SUC i)) (:num))`,

STRIP_TAC
THEN MATCH_MP_TAC CARD_IMAGE_INJ_EQ
THEN EXISTS_TAC`(\(x:real^N#real^N). (SND x, FST x))`
THEN ASM_REWRITE_TAC[EQUI_FF_SYM_0;EXISTS_UNIQUE]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`SND (y:real^N#real^N),FST (y:real^N#real^N)`
THEN MRESA_TAC( GEN_ALL EQUI_FF_SYM_0)[`vv:num->real^N`;`SND (y:real^N#real^N),FST (y:real^N#real^N)`]
THEN REPEAT RESA_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]));;

let FF_OF_HYP_ITER_VV=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv 
==> !n.
(ITER n (ff_of_hyp (vec 0,V,E)) ) (vv (SUC i),vv i)= vv (SUC(n*(k-1)+i)),vv (n*(k-1)+i)`,

STRIP_TAC
THEN INDUCT_TAC
THENL[
REWRITE_TAC[ITER;I_DEF;ARITH_RULE`0 *B+A=A`];
ASM_REWRITE_TAC[ITER]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;ff_of_hyp;]
THEN REPEAT RESA_TAC
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN SUBGOAL_THEN`vv (SUC (n *(k-1)+ i)),(vv:num->real^3) (n *(k-1)+ i) IN
     FF UNION IMAGE (\i. vv (SUC i),vv i) (:num)`ASSUME_TAC
THENL[
REWRITE_TAC[UNION;IN_ELIM_THM]
THEN MATCH_MP_TAC(SET_RULE`A==> B\/A`)
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`n *(k-1)+i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`~(k<=3)==> SUC (SUC n * (k - 1) + i) =(n*(k-1)+i) +k /\ (n * (k - 1) + i) + k - 1 =SUC n * (k - 1) + i`)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`(n * (k - 1) + i)`;`k:num`]
[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;ff_of_hyp;]
THEN SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET]
THEN ASM_TAC
THEN REWRITE_TAC[periodic]
THEN REPEAT RESA_TAC]]);;


let DUAL_EXISTS_MOD0=
prove(` ~(k=0) ==> ?n. (n*(k-1)) MOD k= b MOD k `,

STRIP_TAC
THEN EXISTS_TAC`k- b MOD k`
THEN MRESA_TAC DIVISION[`b:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`~(k=0)/\ b MOD k<k==> b MOD k<=k/\ 1 <= k- b MOD k /\ 0<k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[LEFT_SUB_DISTRIB;ARITH_RULE`a *1=a`;Ssrnat.subn_subA]
THEN MRESAL_TAC Ssrnat.leq_pmul2l[`k:num`;`1:num`;`k- b MOD k`][ARITH_RULE`k*1=k`;MULT_SYM]
THEN MP_TAC(ARITH_RULE`k <= k * (k - b MOD k) ==> (k * (k - b MOD k) + b MOD k) - k = k * (k - b MOD k) - k *1+ b MOD k`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[GSYM LEFT_SUB_DISTRIB]
THEN ONCE_REWRITE_TAC[MULT_SYM]
THEN MRESA_TAC MOD_MULT_ADD[`k-b MOD k-1`;`k:num`;`b MOD k`]
THEN ASM_SIMP_TAC[MOD_MOD_REFL]);;


let DUAL_EXISTS_MOD_LE=
prove(` ~(k=0)/\ a MOD k<= b MOD k ==> ?n. (n*(k-1) +a) MOD k= b MOD k `,

REPEAT STRIP_TAC
THEN MRESA_TAC(GEN_ALL DUAL_EXISTS_MOD0)[`b MOD k- a MOD k`;`k:num`]
THEN EXISTS_TAC`n:num`
THEN MRESA_TAC DIVISION[`b:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`a MOD k<= b MOD k /\ b MOD k<k ==> b MOD k - a MOD k< k/\ (b MOD k- a MOD k) + a MOD k= b MOD k `)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`b MOD k- a MOD k`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`n*(k-1)`;`a:num`;`k:num`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[MOD_MOD_REFL]);;
let DUAL_EXISTS_MOD_GE=
prove(` ~(k=0)/\ b MOD k<= a MOD k ==> ?n. (n*(k-1) +a) MOD k= b MOD k `,

REPEAT STRIP_TAC
THEN MRESA_TAC(GEN_ALL DUAL_EXISTS_MOD0)[`b MOD k +k- a MOD k`;`k:num`]
THEN EXISTS_TAC`n:num`
THEN MRESA_TAC DIVISION[`a:num`;`k:num`]
THEN MRESA_TAC MOD_LT[`a MOD k`;`k:num`]
THEN MP_TAC(ARITH_RULE`a MOD k<k==>(b MOD k + k - a MOD k) + a MOD k= 1* k+  b MOD k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1:num`;`k:num`;`b MOD k`]
THEN MRESA_TAC MOD_ADD_MOD[`b MOD k + k - a MOD k`;`a MOD k:num`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`n*(k-1)`;`a:num`;`k:num`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[MOD_MOD_REFL]);;

let DUAL_EXISTS_MOD=
prove(` ~(k=0) ==> ?n. (n*(k-1) +a) MOD k= b MOD k `,

STRIP_TAC
THEN MP_TAC(ARITH_RULE`a MOD k<= b MOD k\/ b MOD k<= a MOD k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[DUAL_EXISTS_MOD_GE;DUAL_EXISTS_MOD_LE]);;


let FACE_DUAL_SYM_0=
prove(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ x IN FF /\ SND x,FST x = v1 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv 
==>
IMAGE (\i. vv (SUC i),vv i) (:num) = face (hypermap (HYP (vec 0,V,E))) v1`,

STRIP_TAC
THEN POP_ASSUM(fun th-> 
MP_TAC th
THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<=k/\ 1<k/\ ~(k=0)`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[local_fan;face;LET_DEF;LET_END_DEF;OPP_FAN_SYM_0;orbit_map]
THEN ASSUME_TAC th)
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN ASM_TAC
THEN REPLICATE_TAC (16-12)(STRIP_TAC)
THEN EXPAND_TAC"FF"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION;Wrgcvdr_cizmrrh.POWER_TO_ITER;]
THEN REPEAT RESA_TAC
THEN EQ_TAC
THENL[
REPEAT STRIP_TAC
THEN EXPAND_TAC"v1"
THEN MRESA_TAC(GEN_ALL FF_OF_HYP_ITER_VV)
[`FF:real^3#real^3->bool`;`s:scs_v39`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`k:num`;`x'':num`;]
THEN MRESA_TAC (GEN_ALL DUAL_EXISTS_MOD)[`x'':num`;`x'''':num`;`k:num`]
THEN EXISTS_TAC`n:num`
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x'''':num`]
THEN MRESA_TAC th[`n *(k-1) + x''`]
THEN MRESA_TAC th[`SUC x'''':num`]
THEN MRESA_TAC th[`SUC(n *(k-1) + x'')`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ADD1])
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`(n * (k - 1) + x'')`;`1`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`(x''''):num`;`1`;`k:num`]
THEN ARITH_TAC;
RESA_TAC
THEN EXPAND_TAC"v1"
THEN MRESA_TAC(GEN_ALL FF_OF_HYP_ITER_VV)
[`FF:real^3#real^3->bool`;`s:scs_v39`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`k:num`;`x'':num`;]
THEN EXISTS_TAC`n * (k - 1) + x'':num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`]]);;



let LOCAL_FAN_DUAL_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv  
==> local_fan
 (IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
  IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num),
  IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num))`,

[STRIP_TAC
THEN POP_ASSUM(fun th-> 
MP_TAC th
THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<=k/\ 1<k`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[local_fan;LET_DEF;LET_END_DEF;OPP_FAN_SYM_0]
THEN ASSUME_TAC th)
;

REPLICATE_TAC (16-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (15-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC (SYM th))
THEN REPEAT STRIP_TAC
THEN MRESA_TAC face_refl[`hypermap (HYP (vec 0,(V:real^3->bool),(E:(real^3->bool)->bool)))`;`x:real^3#real^3`]
THEN ABBREV_TAC`v1=(SND (x:real^3#real^3),FST (x:real^3#real^3))`
THEN MP_TAC OPP_FAN_SYM_0
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`][DART_OF_HYP_VV]
THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN ASM_SIMP_TAC[IN_ELIM_THM;PAIR_FUN_SYM_0;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2]
THEN REPEAT RESA_TAC
;



EXISTS_TAC`(\(x:real^3,y:real^3). --x,--y) v1`
THEN ASM_SIMP_TAC[UNION;IN_ELIM_THM;IN_PAIR_SYM_0; IN_EQ_PAIR_SYM_0]
THEN MP_TAC FACE_SYM_0
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;]
;


MATCH_MP_TAC(SET_RULE`A==> A\/B`)
THEN EXPAND_TAC"v1"
THEN SIMP_TAC[EQUI_FF_SYM_0]
THEN ASM_SIMP_TAC[];




MP_TAC FACE_ALL_SYM_0
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC
THEN ASM_SIMP_TAC[EQ_SET_PAIR_SYM_0;]
THEN MP_TAC FACE_DUAL_SYM_0
THEN RESA_TAC
;



REPLICATE_TAC (16-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (15-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC (SYM th))
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (vv:num->real^3) (:num)`][DART_OF_HYP_VV]
THEN MP_TAC OPP_FAN_SYM_0
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`][DART_OF_HYP_VV] 
THEN ASM_SIMP_TAC[IN_ELIM_THM;PAIR_FUN_SYM_0;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`)
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[dih2k]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN REPEAT STRIP_TAC;





MRESA_TAC Hypermap.node_map_and_darts[`hypermap
      (HYP
      (vec 0,
       IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i.  (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`IMAGE (\i. vv (SUC i),vv i) (:num) SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num)`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`]
THEN MRESA_TAC (GEN_ALL CARD_EQUI_FF_SYM_0)[`vv:num->real^3`]
THEN REPLICATE_TAC (31-12)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[SYM th]);





ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC
THEN MP_TAC FACE_ALL_SYM_0
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y):real^3#real^3. --x,--y) x'`][ID_SYM_0])
THEN MP_TAC IMAGE_NODE_SYM_0
THEN RESA_TAC
THEN ASM_SIMP_TAC[GSYM IMAGE_UNION]
THEN MRESA_TAC (GEN_ALL IN_EQ_PAIR_SYM_0)[`x':real^3#real^3`;`IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)))
      (:num) UNION
      IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--(vv:num->real^3) (k - SUC (i MOD k)))
      (:num)`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;ID_PAIR_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B= B UNION A`]
THEN STRIP_TAC
THEN REPLICATE_TAC (28-13)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN MRESA_TAC th[`((\(x,y):real^3#real^3. --x,--y) x')`]
)
THEN SET_TAC[]
;


REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x.
          ITER n
          (ff_of_hyp
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))
          (x) =
          (\(x,y). --x,--y) (ITER n (ff_of_hyp (vec 0,V,E)) ((\(x,y). --x,--y) x))`
ASSUME_TAC;



REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;



SUBGOAL_THEN`CARD (IMAGE (\(x,y). --x,--y) (IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num))) = CARD (FF:real^3#real^3->bool)`ASSUME_TAC
;


MRESA_TAC Hypermap.node_map_and_darts[`hypermap
      (HYP
      (vec 0,
       IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i.  (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`IMAGE (\i. vv (SUC i),vv i) (:num) SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num)`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`]
THEN MRESA_TAC (GEN_ALL CARD_EQUI_FF_SYM_0)[`vv:num->real^3`]
;




MP_TAC FAN_SYM_0
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;]
THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][]
THEN MRESA_TAC Hypermap.node_map_and_darts[`hypermap
      (HYP
      (vec 0,
       IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i.  (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0]
THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`)
THEN RESA_TAC
THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`]
THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (40-14)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;


REPLICATE_TAC (43-39)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);


REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC EDGE_POWER_MAP_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x. ITER n
          (edge_map
          (hypermap
          (HYP
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
          (x) =
          (\(x,y). --x,--y)
          (ITER n (edge_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))`
ASSUME_TAC;


REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;

ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (26-15)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;


REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);





REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN MP_TAC NODE_POWER_MAP_SYM_0
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER]
THEN RESA_TAC
THEN SUBGOAL_THEN `!n x. ITER n
          (node_map
          (hypermap
          (HYP
          (vec 0,
           IMAGE (\i. --vv i) (:num),
           IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))))
          (x) =
          (\(x,y). --x,--y)
          (ITER n (node_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))`
ASSUME_TAC;


REPEAT GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0])
;

ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0]
THEN REPLICATE_TAC (26-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF]
THEN REPEAT RESA_TAC;


REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC(ISPEC `i:num` th))
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]);

]);;


let AZIM_NEG_FIRST_PI=
prove_by_refinement(
`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2}
/\ &0<azim (vec 0) v1 w1 w2
==>    azim (vec 0) (--v1)  w1 w2 =  &2 *pi- azim (vec 0) v1 w1 w2`,

[STRIP_TAC
THEN MATCH_MP_TAC AZIM_UNIQUE
THEN MRESA_TAC Fan.properties_coordinate[`vec 0:real^3`;`v1:real^3`;`w1:real^3`]
THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`w2:real^3`]
THEN MRESA_TAC azim[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`e1_fan (vec 0:real^3) v1 w1`;`e2_fan (vec 0:real^3) v1 w1`;`e3_fan (vec 0:real^3) v1 w1`])
THEN EXISTS_TAC`--h1:real`
THEN EXISTS_TAC`--h2:real`
THEN EXISTS_TAC`r1:real`
THEN EXISTS_TAC`r2:real`
THEN EXISTS_TAC`e1_fan (vec 0:real^3) v1 w1`
THEN EXISTS_TAC`--e2_fan (vec 0:real^3) v1 w1`
THEN EXISTS_TAC`-- e3_fan (vec 0:real^3) v1 w1`
THEN EXISTS_TAC`&2 * pi- psi`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= A-B<=> B<=A`;REAL_ARITH`A-B< A<=> &0<B`]
THEN STRIP_TAC;
MATCH_MP_TAC(REAL_ARITH`a<b==> a<=b`)
THEN ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_TAC
THEN REWRITE_TAC[orthonormal]
THEN REPEAT DISCH_TAC
THEN ASM_REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH`-- -- A=A/\ -- &0= &0`;CROSS_RNEG]
THEN ONCE_REWRITE_TAC[DOT_SYM]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DOT_SYM];
ASM_REWRITE_TAC[VECTOR_ARITH`(-- A= vec 0:real^3<=> A= vec 0)/\ A- vec 0=A`;dist;NORM_NEG]
THEN STRIP_TAC;
ASM_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(-- A= vec 0:real^3<=> A= vec 0)/\ A- vec 0=A`;dist;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % --b= -- c <=> a % b=c:real^3`];
REWRITE_TAC[SIN_SUB;COS_SUB]
THEN MRESAL_TAC SIN_PERIODIC[`&0`][REAL_ARITH`&0+A=A`]
THEN MRESAL_TAC COS_PERIODIC[`&0`][REAL_ARITH`&0+A=A `;SIN_0;COS_0]
THEN STRIP_TAC;
VECTOR_ARITH_TAC;
REWRITE_TAC[REAL_ARITH`A-B+A-C=(A+A)-(B+C)`;SIN_SUB;COS_SUB]
THEN MRESAL_TAC SIN_PERIODIC[`&2 *pi`][REAL_ARITH`&0+A=A`]
THEN MRESAL_TAC COS_PERIODIC[`&2 *pi`][REAL_ARITH`&0+A=A `;SIN_0;COS_0]
THEN VECTOR_ARITH_TAC]);;



let AZIM_COMPL_NEG=
prove(`~collinear {vec 0, v1, w1:real^3} /\ ~collinear {vec 0, v1, w2}
==>    azim (vec 0) (--v1)  w1 w2 = azim (vec 0) v1 w2 w1`,

REPEAT STRIP_TAC
THEN MRESA_TAC AZIM_COMPL[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`]
THEN MRESA_TAC azim[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`]
THEN MP_TAC(REAL_ARITH`&0 <= azim (vec 0) v1 w1 w2
==> azim (vec 0) v1 w1 w2 = &0 \/ (&0 < azim (vec 0) v1 w1 (w2:real^3)/\ ~(azim (vec 0) v1 w1 w2 = &0))`)
THEN RESA_TAC
THENL[
POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`w1:real^3`;`v1:real^3`]
THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`w2:real^3`;`v1:real^3`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN RESA_TAC
THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`w2:real^3`]
THEN MRESA_TAC th3[`vec 0:real^3`;`-- v1:real^3`;`w2:real^3`]THEN ASM_SIMP_TAC[AZIM_EQ_0;AFF_GT_2_1;IN_ELIM_THM]
THEN RESA_TAC
THEN EXISTS_TAC`t1+ &2 * t2`
THEN EXISTS_TAC`-- t2:real`
THEN EXISTS_TAC`t3:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`(t1 + &2 * t2) + --t2 + t3= t1+t2+t3`]
THEN VECTOR_ARITH_TAC;
ASM_SIMP_TAC[AZIM_NEG_FIRST_PI]]);;


let REMOVE_NEG_AZIM1_SYM_0=
prove_by_refinement(`~collinear {vec 0, v1, w1:real^3} /\ ~collinear {vec 0, v1, w2}
==>    azim (vec 0) v1  (--w1) (--w2) =  azim (vec 0) v1 w1 w2`,

[STRIP_TAC
THEN MATCH_MP_TAC AZIM_UNIQUE
THEN MRESA_TAC Fan.properties_coordinate[`vec 0:real^3`;`v1:real^3`;`w1:real^3`]
THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`w2:real^3`]
THEN MRESA_TAC azim[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`]
THEN POP_ASSUM (fun th-> MRESAL_TAC th[`e1_fan (vec 0:real^3) v1 w1`;`e2_fan (vec 0:real^3) v1 w1`;`e3_fan (vec 0:real^3) v1 w1`][VECTOR_ARITH`A- vec 0=A`])
THEN EXISTS_TAC`--h1:real`
THEN EXISTS_TAC`--h2:real`
THEN EXISTS_TAC`r1:real`
THEN EXISTS_TAC`r2:real`
THEN EXISTS_TAC`--e1_fan (vec 0:real^3) v1 w1`
THEN EXISTS_TAC`--e2_fan (vec 0:real^3) v1 w1`
THEN EXISTS_TAC`e3_fan (vec 0:real^3) v1 w1`
THEN EXISTS_TAC`psi:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= A-B<=> B<=A`;REAL_ARITH`A-B< A<=> &0<B`;VECTOR_ARITH`A- vec 0=A`]
THEN STRIP_TAC;
ASM_TAC
THEN REWRITE_TAC[orthonormal]
THEN REPEAT DISCH_TAC
THEN ASM_REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH`-- -- A=A/\ -- &0= &0`;CROSS_RNEG;CROSS_LNEG]
THEN ONCE_REWRITE_TAC[DOT_SYM]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DOT_SYM];
ASM_REWRITE_TAC[VECTOR_ARITH`--w1 =
 (r1 * cos psi) % --e1_fan (vec 0) v1 w1 +
 (r1 * sin psi) % --e2_fan (vec 0) v1 w1 +
 --h1 % v1 <=> w1 =
 (r1 * cos psi) % e1_fan (vec 0) v1 w1 +
 (r1 * sin psi) % e2_fan (vec 0) v1 w1 +
 h1 % v1:real^3`]
THEN ASM_REWRITE_TAC[VECTOR_ARITH`--w2 =
 (r2 * cos (psi + azim (vec 0) v1 w1 w2)) % --e1_fan (vec 0) v1 w1 +
 (r2 * sin (psi + azim (vec 0) v1 w1 w2)) % --e2_fan (vec 0) v1 w1 +
 --h2 % v1<=> 
w2 =
 (r2 * cos (psi + azim (vec 0) v1 w1 w2)) % e1_fan (vec 0) v1 w1 +
 (r2 * sin (psi + azim (vec 0) v1 w1 w2)) % e2_fan (vec 0) v1 w1 +
 h2 % v1`]
THEN RESA_TAC;
REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN SET_TAC[];
REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;


let AZIM_NEG=
prove(`~collinear {vec 0, v1, w1:real^3} /\ ~collinear {vec 0, v1, w2}
==>    azim (vec 0) (--v1)  (--w1) (--w2) =  azim (vec 0) v1 w2 w1`,

STRIP_TAC
THEN MRESA_TAC (GEN_ALL COLLINEAR_POINT_SYM_0)[`w1:real^3`;`v1:real^3`]
THEN MRESA_TAC (GEN_ALL COLLINEAR_POINT_SYM_0)[`w2:real^3`;`v1:real^3`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL REMOVE_NEG_AZIM1_SYM_0)[`-- v1:real^3`;`w1:real^3`;` w2:real^3`]
THEN ASM_SIMP_TAC[AZIM_COMPL_NEG]);;


let FST_SND_NEG_PAIR_SYM_0=
prove(`--SND ((\(x,y):real^N#real^N. --x,--y) x)= SND x/\ --FST ((\(x,y):real^N#real^N. --x,--y) x)= FST x`,

MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN REWRITE_TAC[VECTOR_ARITH`-- -- A=A:real^N`]);;





let CONVEX_LOCAL_FAN_SYM_0=
prove_by_refinement(` scs_k_v39 s=k /\
  IMAGE vv (:num) = V /\
       IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
       IMAGE (\i. vv i,vv (SUC i)) (:num) = FF 
/\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv
==> convex_local_fan
 (IMAGE (\i. --vv (k - SUC (i MOD k))) (:num),
  IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num),
  IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num))`,

[REWRITE_TAC[convex_local_fan]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)/\ 1<k`)
THEN RESA_TAC
THEN MP_TAC LOCAL_FAN_DUAL_SYM_0
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;]
THEN REPLICATE_TAC (10) RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_E_EQ;OPP_IMAGE_F_EQ2]
THEN ASM_SIMP_TAC[PAIR_FUN_SYM_0;IMAGE_E_SYM_0;IMAGE_V_SYM_0;OPP_IMAGE_E_EQ;OPP_IMAGE_F_EQ2]
THEN REPEAT STRIP_TAC;
MRESAL_TAC (GEN_ALL IN_PAIR_SYM_0)[` (x:real^3#real^3)`;`IMAGE (\(x,y). --x,--y)
      (IMAGE (\i. (vv:num->real^3) (SUC i),vv (i)) (:num))`][ID_PAIR_SYM_0]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)
[`IMAGE (\x:real^3. --x) V`;`IMAGE (\(x,y):real^3#real^3. --x,--y) (IMAGE (\i. vv (SUC i),vv i) (:num))`;`IMAGE (\i. {-- (vv:num->real^3) i, --vv (SUC i)}) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:real^3#real^3`])
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM PAIR_FUN_SYM_0]
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[EE_SYM_0]
THEN RESA_TAC
THEN ASM_SIMP_TAC[EE_SYM_0;EE_EXPAND_BB_VV]
THEN MRESAL_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`;]
[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x' +k-1`]
THEN MRESA_TAC th[`x':num`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MP_TAC(ARITH_RULE`~(k<=3) ==> SUC x' + k - 1= 1 *k + x'/\ ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`x':num`]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0;GSYM Local_lemmas.SIN_AZIM_POS_PI_LT;Polar_fan.SIN_AZIM_MUTUAL_CROSS;DOT_RNEG;]
THEN SUBGOAL_THEN `((vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))) IN FF` ASSUME_TAC;
EXPAND_TAC"FF"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`SUC x':num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];
REPLICATE_TAC (19-10)(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))`])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)
[`V:real^3->bool`;` (IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num))`;`IMAGE (\i. { (vv:num->real^3) i, vv (SUC i)}) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))`])
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th->  MRESA_TAC th[`x':num `]
THEN MRESA_TAC th[`1*k+ x' `])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0;GSYM Local_lemmas.SIN_AZIM_POS_PI_LT;Polar_fan.SIN_AZIM_MUTUAL_CROSS;DOT_RNEG;CROSS_RNEG;CROSS_LNEG;]
THEN REPEAT STRIP_TAC
THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
THEN REWRITE_TAC[CROSS_TRIPLE;DOT_LNEG]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;DOT_LNEG]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[wedge_in_fan_ge2]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM PAIR_FUN_SYM_0]
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[EE_SYM_0]
THEN RESA_TAC
THEN ASM_SIMP_TAC[EE_SYM_0;EE_EXPAND_BB_VV]
THEN MRESAL_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`;]
[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x' +k-1`]
THEN MRESA_TAC th[`x':num`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MP_TAC(ARITH_RULE`~(k<=3) ==> SUC x' + k - 1= 1 *k + x'/\ ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`x':num`]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0;GSYM Local_lemmas.SIN_AZIM_POS_PI_LT;Polar_fan.SIN_AZIM_MUTUAL_CROSS;DOT_RNEG;]
THEN SUBGOAL_THEN `((vv:num->real^3) (SUC x')) IN V` ASSUME_TAC;

EXPAND_TAC"V"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`SUC x':num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th->  MRESA_TAC th[`x':num `]
THEN MRESA_TAC th[`1 *k +x'`])
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`FF:real^3#real^3->bool`;`V:real^3->bool`;`(vv:num->real^3) (SUC x')`;`E:(real^3->bool)->bool`;]
THEN MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_FINITE_EE)[`vec 0:real^3`;`V:real^3->bool`;`(vv:num->real^3) (SUC x')`;`E:(real^3->bool)->bool`;]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_SIMP_TAC[ELEMENT2_SYM_0;CARD_SYM_0;ARITH_RULE`2>1`]
THEN SUBGOAL_THEN `((vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))) IN FF` ASSUME_TAC;

EXPAND_TAC"FF"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`SUC x':num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

REPLICATE_TAC (25-10)(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))`])
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;wedge_in_fan_ge2;ARITH_RULE`2>1`;wedge_ge;azim;SUBSET;IN_ELIM_THM;IMAGE]
THEN REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`collinear {(vec 0),(--(vv:num->real^3) (SUC x')),-- x''' }\/ ~(collinear {(vec 0),(--(vv:num->real^3) (SUC x')),-- x''' })`)
THEN RESA_TAC;

ASM_SIMP_TAC[AZIM_DEGENERATE;azim];

MRESAL_TAC (GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`{--(vv:num->real^3) (SUC x'), --x'''}`][ELEMENT2_SYM_0;REFL_SYM_0]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[GSYM ELEMENT2_SYM_0;SET_RULE`{A} UNION {B,C}={A,B,C}`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`collinear {(vec 0),(--(vv:num->real^3) (SUC x')),(--vv (1 * k + x')) }\/ ~(collinear {(vec 0),(--(vv:num->real^3) (SUC x')),(--vv (1 * k + x')) })`)
THEN RESA_TAC;

ASM_SIMP_TAC[AZIM_DEGENERATE;azim;]
THEN REAL_ARITH_TAC;

MRESAL_TAC (GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`{--(vv:num->real^3) (SUC x'), (--vv (1 * k + x'))}`][ELEMENT2_SYM_0;REFL_SYM_0]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[GSYM ELEMENT2_SYM_0;SET_RULE`{A} UNION {B,C}={A,B,C}`]
THEN STRIP_TAC
THEN REPLICATE_TAC (32-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`x''':real^3`])
THEN ASM_SIMP_TAC[AZIM_NEG]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`(vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC (SUC x'))`]
THEN ASM_SIMP_TAC[AZIM_NEG]
THEN MRESA_TAC Fan.sum4_azim_fan[`vec 0:real^3`;`(vv:num->real^3) (SUC x')`;`(vv:num->real^3) (SUC(SUC x'))`;`x''':real^3`;`(vv:num->real^3) (x')`]
THEN REWRITE_TAC[REAL_ARITH`a<=b+a<=> &0<=b`;azim]]);;


let PEROPP_IN_BB_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBs_v39 s vv /\ ~(k<=3)
==> BBs_v39 (scs_opp_v39 s) (\i. -- peropp vv k i)`,

[REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;scs_opp_v39;PAIR_EQ;LET_DEF;LET_END_DEF;BBs_v39;scs_v39_explicit;peropp2;peropp;is_scs_v39]
THEN STRIP_TAC
THEN ASM_TAC
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
THEN RESA_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[BALL_ANNULUS_SYM_0]
THEN MRESA_TAC (GEN_ALL OPP_IMAGE_V_EQ)[`k:num`;`vv:num->real^3`]
THEN POP_ASSUM(fun th->
ASM_TAC 
THEN REWRITE_TAC[SYM th]
THEN REPEAT STRIP_TAC)
THEN REPLICATE_TAC (29-21)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MATCH_MP_TAC(SET_RULE`a IN A ==> (A SUBSET B==> a IN B)`)
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`];

ASM_TAC
THEN REWRITE_TAC[periodic;peropp;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`];

ASM_SIMP_TAC[DIST_SYM_0];

ASM_SIMP_TAC[DIST_SYM_0];

MRESA_TAC (GEN_ALL CONVEX_LOCAL_FAN_SYM_0)[`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (\i. (vv:num->real^3) i,vv (SUC i)) (:num)`;`s:scs_v39`;`(vv:num->real^3)`;`k:num`]
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[scs_arrow_v39;IN_SING;scs_opp_v39;PAIR_EQ;LET_DEF;LET_END_DEF;BBs_v39;scs_v39_explicit;peropp2;peropp;is_scs_v39]]);;




let NO_IS_EAR=
prove(`~(scs_k_v39 s<=3)==> ~(is_ear_v39 s)`,

REWRITE_TAC[is_ear_v39]
THEN ARITH_TAC);;
let NO_IS_EAR_SCS_OPP=
prove(`~(scs_k_v39 s<=3)==> ~(is_ear_v39 (scs_opp_v39 s))`,

REWRITE_TAC[is_ear_v39;LET_DEF;LET_END_DEF;scs_opp_v39;scs_v39_explicit]
THEN ARITH_TAC);;


let DSV_EQ_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBs_v39 s vv /\ ~(k<=3)
==> dsv_v39 (scs_opp_v39 s) (\i. --peropp vv k i) = dsv_v39 s vv`,

[STRIP_TAC
THEN ASM_SIMP_TAC[dsv_v39;NO_IS_EAR_SCS_OPP;NO_IS_EAR;LET_DEF;LET_END_DEF;scs_opp_v39;scs_v39_explicit;peropp2;DIST_SYM_0;peropp]
THEN MATCH_MP_TAC(REAL_ARITH`a=b==> c+ #0.1 * -- &1 *a= c+ #0.1 * -- &1 *b`)
THEN MATCH_MP_TAC SUM_EQ_GENERAL
THEN EXISTS_TAC`(\j. k - SUC(SUC(j MOD k) MOD k))`
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT RESA_TAC;

REWRITE_TAC[EXISTS_UNIQUE]
THEN MP_TAC(ARITH_RULE`~(k<=3)==> k-1<k/\ ~(k=0)/\ 1<k/\ SUC(k-1)=k/\ k-k=0/\ 1*k+0=k/\0<k/\ SUC 0=1`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`y<k==> y=k-1\/ SUC y<k`)
THEN RESA_TAC;

EXISTS_TAC`k-1`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN MRESA_TAC MOD_LT[`0`;`k:num`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`0`]
THEN REPLICATE_TAC (17-5)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`scs_J_v39 s (k-1)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k:num`])
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC DIVISION[`SUC(y' MOD k)`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC (y' MOD k) MOD k < k /\ 1<k /\ k - SUC (SUC (y' MOD k) MOD k) = k - 1
==> SUC (y' MOD k) MOD k = 0`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`~(k<=3)==> 1+k-1=k`)
THEN RESA_TAC
THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`y' MOD k`;`k-1`;`1`;`k:num`][GSYM ADD1;ARITH_RULE`1+A=A+1`]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC MOD_LT[`y':num`;`k:num`];

EXISTS_TAC`k- SUC(SUC y)`
THEN MP_TAC(ARITH_RULE`SUC y<k/\ ~(k<=3)==> k - SUC (SUC y) < k/\ SUC (k - SUC (SUC y))= k - SUC y/\ k - SUC y<k/\ k - (k - SUC y)= SUC y /\ (k - SUC (k - SUC y))=y`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k - SUC(SUC y)`;`k:num`]
THEN MRESA_TAC MOD_LT[`k - (SUC y)`;`k:num`]
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC MOD_LT[`y':num`;`k:num`]
THEN MP_TAC(ARITH_RULE`y'<k==> y'=k-1\/ SUC y'<k`)
THEN RESA_TAC;

MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`0`]
THEN MRESA_TAC MOD_LT[`0`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC y<k==> ~(k-1=y)`)
THEN RESA_TAC;

MRESA_TAC MOD_LT[`SUC y':num`;`k:num`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`SUC y'<k /\ SUC y<k/\ k - SUC (SUC y') = y ==> y' = k - SUC (SUC y)`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE`~(k<=3)==> k-1<k/\ ~(k=0)/\ 1<k/\ SUC(k-1)=k/\ k-k=0/\ 1*k+0=k/\0<k/\ SUC 0=1`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC(x MOD k)`;`k:num`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

MP_TAC(ARITH_RULE`~(k<=3)==> k-1<k/\ ~(k=0)/\ 1<k/\ SUC(k-1)=k/\ k-k=0/\ 1*k+0=k/\0<k/\ SUC 0=1`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC x`;`k:num`]
THEN MP_TAC(ARITH_RULE`~(k<=3)/\ SUC x MOD k<k ==> k-1<k/\ ~(k=0)/\ 1<k/\ SUC(k-1)=k/\ k-k=0/\ 1*k+0=k/\0<k/\ SUC 0=1/\ SUC (k - SUC (SUC x MOD k))= k- SUC x MOD k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`x:num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (36-24)(POP_ASSUM MP_TAC) 
THEN POP_ASSUM(fun th-> 
REPEAT DISCH_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`x<k==>x=k-1\/ SUC x<k`)
THEN RESA_TAC;

MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`0`]
THEN MRESA_TAC MOD_LT[`0`;`k:num`]
THEN REWRITE_TAC[ARITH_RULE`k-0=k`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`scs_J_v39 s (k-1)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k:num`]);

MRESA_TAC MOD_LT[`SUC x`;`k:num`];

MP_TAC(ARITH_RULE`~(k<=3)==> k-1<k/\ ~(k=0)/\ 1<k/\ SUC(k-1)=k/\ k-k=0/\ 1*k+0=k/\0<k/\ SUC 0=1`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC x`;`k:num`]
THEN MP_TAC(ARITH_RULE`~(k<=3)/\ SUC x MOD k<k ==> k-1<k/\ ~(k=0)/\ 1<k/\ SUC(k-1)=k/\ k-k=0/\ 1*k+0=k/\0<k/\ SUC 0=1/\ SUC (k - SUC (SUC x MOD k))= k- SUC x MOD k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`x:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`x<k==>x=k-1\/ SUC x<k`)
THEN RESA_TAC;

MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`0`]
THEN MRESA_TAC MOD_LT[`0`;`k:num`]
THEN REWRITE_TAC[ARITH_RULE`k-0=k`]
THEN ASM_TAC
THEN REWRITE_TAC[BBprime_v39;BBs_v39;periodic2;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k:num`])
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DIST_SYM]
THEN REWRITE_TAC[];

MRESA_TAC MOD_LT[`SUC x`;`k:num`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DIST_SYM]
THEN REWRITE_TAC[]]);;


let SUM_PAIR_SYM_0=
prove(`sum (IMAGE (\(x,y):real^N#real^N. --x,--y) s) f= sum s (f o ((\(x,y). --x,--y)))`,

MATCH_MP_TAC SUM_IMAGE
THEN REPEAT GEN_TAC
THEN MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN MP_TAC(SET_RULE`y=(FST (y:real^N#real^N),SND (y:real^N#real^N))`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`;PAIR_EQ]
THEN ASM_REWRITE_TAC[GSYM PAIR_EQ]
THEN RESA_TAC);;


let TAUSTAR_EQ_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBs_v39 s vv /\ ~(k<=3)
==> taustar_v39 (scs_opp_v39 s) (\i. --peropp vv k i) = taustar_v39 s vv`,

[STRIP_TAC
THEN MP_TAC DSV_EQ_SYM_0
THEN RESA_TAC
THEN 
ASM_REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF;scs_opp_v39;scs_v39_explicit]
THEN MATCH_MP_TAC (REAL_ARITH`C=A==>A-B=C-B`)
THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<=k/\ 1<k/\0<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[tau_fun;peropp;OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;]
THEN ASM_SIMP_TAC[PAIR_FUN_SYM_0]
THEN MRESA_TAC (GEN_ALL Local_lemmas.CVLF_LF_F)[`       IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`IMAGE (vv:num->real^3) (:num)`;`
       IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;]
THEN MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF)[`IMAGE (vv:num->real^3) (:num)`;`
       IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`       IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`]
THEN MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.LOCAL_IMP_FINITE_DARTS)
[`       IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`
       IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (vv:num->real^3) (:num)`]
THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`]
THEN ASSUME_TAC(SET_RULE`IMAGE (\i. vv (SUC i),vv i) (:num) SUBSET
      IMAGE (\i. vv i,vv (SUC i)) (:num) UNION
      IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num)`)
THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num)`;`darts_of_hyp (IMAGE (\i. {vv i, (vv:num->real^3) (SUC i)}) (:num)) (IMAGE vv (:num))`]
THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0;CARD_EQUI_FF_SYM_0]
THEN MATCH_MP_TAC (REAL_ARITH`A=C==>A-B=C-B`)
THEN ASM_SIMP_TAC[SUM_PAIR_SYM_0;o_DEF;FST_SND_PAIR_SYM_0]
THEN MRESA_TAC(GEN_ALL Qknvmlb.SUM_AZIM_EQ_ANGLE_LE4)[`IMAGE (vv:num->real^3) (:num)`;`vv:num->real^3`;`1:num`;`s:scs_v39`;`(vv:num->real^3) (1 MOD scs_k_v39 s)`;`      IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`
       IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MATCH_MP_TAC SUM_EQ_GENERAL
THEN ASM_REWRITE_TAC[IN_ELIM_THM;]
THEN MP_TAC(ARITH_RULE`~(k<=3)==> SUC(k-1)=k/\ SUC(SUC(k-1))=k+1/\ SUC 0=1/\ ~(k=0)/\ 1 * k + 0=k/\ 1 * k + 1=k+1/\1<k/\ 3<k`)
THEN RESA_TAC
THEN EXISTS_TAC`(\i. (vv:num->real^3) (SUC i),vv i)`
THEN RESA_TAC;

REWRITE_TAC[IN_ELIM_THM;IMAGE;EXISTS_UNIQUE]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`x MOD k`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC DIVISION[`x:num`;`k:num`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`]
THEN MRESA_TAC th[`SUC x:num`]
THEN MRESA_TAC th[`SUC(x MOD k):num`])
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[MOD_SUC_MOD;PAIR_EQ]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`vv:num->real^3`]
[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`y':num`;`x MOD k`]);

REPEAT RESA_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

REWRITE_TAC[ADD1;NORM_NEG;REAL_EQ_MUL_LCANCEL]
THEN MATCH_MP_TAC(SET_RULE`A==> C\/A`)
THEN REWRITE_TAC[GSYM ADD1]
THEN ABBREV_TAC`V= IMAGE (vv:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((vv:num->real^3) i, vv (SUC i))) (:num)`
THEN MP_TAC LOCAL_FAN_DUAL_SYM_0
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_E_EQ;OPP_IMAGE_F_EQ2]
THEN ASM_SIMP_TAC[PAIR_FUN_SYM_0;IMAGE_E_SYM_0;IMAGE_V_SYM_0;OPP_IMAGE_E_EQ;OPP_IMAGE_F_EQ2]
THEN STRIP_TAC
THEN SUBGOAL_THEN`(--vv (SUC x),--vv x) IN IMAGE (\(x,y). --x,--y) (IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num))`ASSUME_TAC;

REWRITE_TAC[GSYM PAIR_FUN_SYM_0]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)
[`IMAGE (\x:real^3. --x) (IMAGE vv (:num))`;`IMAGE (\(x,y):real^3#real^3. --x,--y) (IMAGE (\i. vv (SUC i),vv i) (:num))`;`IMAGE (\i. {-- (vv:num->real^3) i, --vv (SUC i)}) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(--vv (SUC x),--(vv:num->real^3) x)`])
THEN ASM_SIMP_TAC[EE_SYM_0;EE_EXPAND_BB_VV]
THEN MRESAL_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x`;`k:num`;]
[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x +k-1`]
THEN MRESA_TAC th[`x:num`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MP_TAC(ARITH_RULE`~(k<=3) ==> SUC x + k - 1= 1 *k + x/\ ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`x:num`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]
THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)[`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`(vv:num->real^3) (1 MOD k)`;`vv:num->real^3`;`1 MOD k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39;GSYM ADD1]
THEN SUBGOAL_THEN`(vv:num->real^3) (SUC x) IN V`ASSUME_TAC;

EXPAND_TAC"V"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`SUC x:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

MP_TAC Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) (SUC x)`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x `])
THEN MRESAL_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`vv:num->real^3`;`IMAGE (vv:num->real^3) (:num)`;`k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN  MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) (SUC x)`])
THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)[`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`(vv:num->real^3) (SUC x MOD k)`;`vv:num->real^3`;`SUC x MOD k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39;GSYM ADD1]
THEN POP_ASSUM (fun th-> MRESAL_TAC th[`SUC 0`][ITER]
THEN MRESAL_TAC th[`k - 1`][ITER;ARITH_RULE`1+A=SUC A`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th->  
MRESA_TAC th[`x:num`]
THEN MRESA_TAC th[`SUC (SUC x )`]
THEN MRESA_TAC th[`SUC (SUC x MOD k) `]
THEN MRESA_TAC th[`k-1+ (SUC x MOD k) `])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[MOD_SUC_MOD]
THEN MP_TAC(ARITH_RULE`3<k==> k-1<k/\ k-1 +SUC x= 1*k+x`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`k-1`;`SUC x`;`k:num`]
THEN MATCH_MP_TAC AZIM_NEG
THEN SUBGOAL_THEN`(vv:num->real^3) (SUC x),vv (SUC (SUC x)) IN FF`ASSUME_TAC;

EXPAND_TAC"FF"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`SUC x:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`(vv:num->real^3) (SUC x), (vv:num->real^3) (SUC (SUC x))`]
THEN SUBGOAL_THEN`(vv:num->real^3) ( x),vv ( (SUC x)) IN FF`ASSUME_TAC;

EXPAND_TAC"FF"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`(vv:num->real^3) (x), (vv:num->real^3) ( (SUC x))`]]);;







let OPP_IS_SCS=
prove_by_refinement( `is_scs_v39 s/\ s' = scs_opp_v39 s==> is_scs_v39 (scs_opp_v39 s)`,

[
ABBREV_TAC`k=scs_k_v39 s`
THEN ASM_TAC
THEN REWRITE_TAC[scs_v39_explicit;scs_opp_v39;LET_DEF;LET_END_DEF;is_scs_v39;peropp]
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN REPEAT RESA_TAC;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
;



ASM_TAC
THEN REWRITE_TAC[periodic;peropp;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
;

ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;

ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;

ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;

ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;



ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;

ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;

ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;

ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESA_TAC MOD_LT[`i:num`;`k:num`]
THEN MRESA_TAC MOD_LT[`j:num`;`k:num`]
THEN MRESA_TAC SUC_INJ[`i:num`;`j:num`]
THEN MP_TAC(ARITH_RULE`i < k/\ j <k /\ ~(SUC i= SUC j)==> k- SUC i<k /\ k- SUC j<k /\ ~(k- SUC i= k- SUC j)`)
THEN RESA_TAC
;



ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC DIVISION[`i:num`;`scs_k_v39 s`][ARITH_3_TAC]
THEN MP_TAC(ARITH_RULE`i MOD 3<3 ==> i MOD 3=0\/ i MOD 3=1\/ i MOD 3=2`)
THEN RESA_TAC;



MRESAL_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`i:num`;`0:num`;`3`][ARITH_3_TAC]
THEN REPLICATE_TAC (29-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`1:num`[ARITH_3_TAC])
;


MRESAL_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`i:num`;`1:num`;`3`][ARITH_3_TAC]
THEN REPLICATE_TAC (29-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`0:num`[ARITH_3_TAC])
;


MRESAL_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`i:num`;`2:num`;`3`][ARITH_3_TAC]
THEN REPLICATE_TAC (29-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`2:num`[ARITH_3_TAC])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (29-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN ASSUME_TAC th
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s 2`][ARITH_3_TAC;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC])

;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`i MOD k<k /\3<k==> i MOD k= k-1 \/ i MOD k<k-1`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE`3<k==> k- SUC(k-1)=0/\ 1<k/\ k-1+1=k/\ k*1=k/\ k - (0 + 1)=k-1/\ SUC(k-1)=k`)
THEN RESA_TAC
THEN REWRITE_TAC[ADD1]
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MRESA_TAC MOD_MULT[`k:num`;`1:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`1`;`k:num`]
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (k-1)`][ARITH_3_TAC;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC])
THEN REPLICATE_TAC (37-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`k-1:num`[ARITH_3_TAC])
;


MP_TAC(ARITH_RULE`3<k/\ i MOD k< k-1==> k- SUC(k-1)=0/\ 1<k/\ k-1+1=k/\ k*1=k/\ k - (0 + 1)=k-1/\ SUC(k-1)=k/\ i MOD k+1<k/\ k - (i MOD k+1)=SUC (k - ((i MOD k+1) + 1)) `)
THEN RESA_TAC
THEN REWRITE_TAC[ADD1]
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MRESA_TAC MOD_LT[`i MOD k+1`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`1`;`k:num`]
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN REPLICATE_TAC (38-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`(k - ((i MOD k + 1) + 1)):num`[ARITH_3_TAC])
;





ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
THEN STRIP_TAC
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`3<=k/\ i MOD k<k /\ j MOD k<k==> SUC (k - SUC (i MOD k)) = (k -  (i MOD k))/\ k- SUC(i MOD k)<k /\ k- SUC(j MOD k)<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k- SUC(i MOD k)`;`k:num`]
THEN MRESA_TAC MOD_LT[`k- SUC(j MOD k)`;`k:num`]
THEN REPLICATE_TAC (34-18)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`k - SUC (i MOD k):num`;`(k - SUC (j MOD k))`][ARITH_3_TAC])
;

POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`i MOD k< k==> i MOD k=0 \/ k-i MOD k<k`)
THEN RESA_TAC;


MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k `]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`k - SUC (j MOD k) = 0 /\ j MOD k<k /\ 3<=k==> j MOD k= k-1 /\ k-1<k/\ SUC(k-1)=k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN 
MRESA_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`j:num`;`k-1:num`;`k:num`]
;


MRESA_TAC MOD_LT[`k-i MOD k`;`k:num`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`k - SUC (j MOD k) = k - i MOD k /\ i MOD k< k /\  j MOD k < k/\ k - i MOD k<k/\ 3<=k ==> i MOD k = SUC (j MOD k)/\ (j MOD k) +1 <k/\ 1<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MRESA_TAC MOD_LT[`j MOD k +1`;`k:num`]
THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`k:num`][ADD1]
;



 POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`j MOD k<k==> SUC(k- SUC(j MOD k))= k -j MOD k`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD k< k==> j MOD k=0 \/ k-j MOD k<k`)
THEN RESA_TAC;


MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k `]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`k - SUC (i MOD k) = 0 /\ i MOD k<k /\ 3<=k==> i MOD k= k-1 /\ k-1<k/\ SUC(k-1)=k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN 
MRESA_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`i:num`;`k-1:num`;`k:num`]
;


MRESA_TAC MOD_LT[`k-j MOD k`;`k:num`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`k - SUC (i MOD k) = k - j MOD k /\ j MOD k< k /\  i MOD k < k/\ k - j MOD k<k/\ 3<=k ==> j MOD k = SUC (i MOD k)/\ (i MOD k) +1 <k/\ 1<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MRESA_TAC MOD_LT[`i MOD k +1`;`k:num`]
THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`k:num`][ADD1]
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
THEN STRIP_TAC
THEN REPLICATE_TAC (25-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`k - SUC (i MOD k):num`;`(k - SUC (j MOD k))`][ARITH_3_TAC])
;


ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
THEN STRIP_TAC
THEN REPLICATE_TAC (25-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`k - SUC (i MOD k):num`;`(k - SUC (j MOD k))`][ARITH_3_TAC])
;




ASM_TAC
THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]
THEN SUBGOAL_THEN`
CARD
      {i | i < k /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
=CARD
 {i | i < k /\
      (&2 * h0 < scs_b_v39 s (k - SUC (i MOD k)) (k - SUC (SUC i MOD k)) \/
       &2 < scs_a_v39 s (k - SUC (i MOD k)) (k - SUC (SUC i MOD k)))}
`
ASSUME_TAC
;



MATCH_MP_TAC CARD_IMAGE_INJ_EQ
THEN REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`(\x. k -  SUC (SUC x MOD k))`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

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

STRIP_TAC;


GEN_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC MOD_LT[`x:num`;`k:num`]
THEN MRESA_TAC DIVISION[`SUC x`;`k:num`]
THEN MP_TAC(ARITH_RULE`3<=k /\ SUC x MOD k < k ==> k - SUC(SUC x MOD k )<k
/\ SUC (k - SUC (SUC x MOD k)) = k- SUC x MOD k`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k `]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (k-1)`][ARITH_3_TAC;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (k-1)`][ARITH_3_TAC;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC])
THEN MP_TAC(ARITH_RULE`x<k ==> SUC x=k \/ SUC x<k`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1/\ k-k=0/\ k-0=k`]
THEN MRESA_TAC MOD_LT[`SUC x`;`k:num`]
THEN RESA_TAC;



REWRITE_TAC[EXISTS_UNIQUE]
THEN REPEAT STRIP_TAC
;

POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`y<k ==> y=k-1\/ y< k-1`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE`3<=k==> k-1<k/\ SUC(k-1)=k`)
THEN RESA_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`k-1`
THEN MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (k-1)`][ARITH_3_TAC;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC])
THEN REPEAT STRIP_TAC
THEN MRESA_TAC DIVISION[`SUC y':num`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC y' MOD k< k /\ k - SUC (SUC y' MOD k) = k - 1 ==> SUC y' MOD k=0`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`y'<k /\ 3<=k ==> SUC y'<k\/ y'=k-1`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`]
;


STRIP_TAC
THEN EXISTS_TAC`k-y-2`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`y<k-1==> k-y-2<k/\ SUC(k-y-2)= k-y-1/\ k-y-1<k/\ k - SUC (k - y - 1) = y/\ k - (k - y - 1)= SUC y`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k-y-1`;`k:num`]
THEN MRESA_TAC MOD_LT[`k-y-2`;`k:num`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`y'<k /\ 3<=k ==> SUC y'<k\/ y'=k-1`)
THEN RESA_TAC
;

MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`k - y - 2 < k/\ k - SUC (SUC y') = y/\ SUC y'<k 
==> y'= k-y-2`)
THEN RESA_TAC;


MP_TAC(ARITH_RULE`3<=k/\ y< k-1 ==>SUC(k-1)=k/\ ~(k-1=y)`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
;


MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`k - y - 2 < k/\ k - SUC (SUC y') = y/\ SUC y'<k 
==> y'= k-y-2`)
THEN RESA_TAC;


MP_TAC(ARITH_RULE`3<=k/\ y< k-1 ==>SUC(k-1)=k/\ ~(k-1=y)`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
;



POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`y<k ==> y=k-1\/ y< k-1`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE`3<=k==> k-1<k/\ SUC(k-1)=k`)
THEN RESA_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`k-1`
THEN MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (k-1)`][ARITH_3_TAC;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC])
THEN REPEAT STRIP_TAC
THEN MRESA_TAC DIVISION[`SUC y':num`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC y' MOD k< k /\ k - SUC (SUC y' MOD k) = k - 1 ==> SUC y' MOD k=0`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`y'<k /\ 3<=k ==> SUC y'<k\/ y'=k-1`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`]
;


STRIP_TAC
THEN EXISTS_TAC`k-y-2`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`y<k-1==> k-y-2<k/\ SUC(k-y-2)= k-y-1/\ k-y-1<k/\ k - SUC (k - y - 1) = y/\ k - (k - y - 1)= SUC y`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k-y-1`;`k:num`]
THEN MRESA_TAC MOD_LT[`k-y-2`;`k:num`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`y'<k /\ 3<=k ==> SUC y'<k\/ y'=k-1`)
THEN RESA_TAC
;

MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`k - y - 2 < k/\ k - SUC (SUC y') = y/\ SUC y'<k 
==> y'= k-y-2`)
THEN RESA_TAC;


MP_TAC(ARITH_RULE`3<=k/\ y< k-1 ==>SUC(k-1)=k/\ ~(k-1=y)`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
;


MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`k - y - 2 < k/\ k - SUC (SUC y') = y/\ SUC y'<k 
==> y'= k-y-2`)
THEN RESA_TAC;


MP_TAC(ARITH_RULE`3<=k/\ y< k-1 ==>SUC(k-1)=k/\ ~(k-1=y)`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
;

POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
;



]);;

let DUAL_PEROPP=
prove(`~(k=0) /\ periodic a k==> peropp (peropp a k) k=a`,

STRIP_TAC
THEN ASM_SIMP_TAC[FUN_EQ_THM;peropp;OPP_SUC_MOD;PERIODIC_PROPERTY]);;

let DUAL_PEROPP2=
prove(`~(k=0) /\ periodic2 a k==> peropp2 (peropp2 a k) k=a`,

REWRITE_TAC[periodic2]
THEN STRIP_TAC
THEN ASM_SIMP_TAC[FUN_EQ_THM;peropp2;OPP_SUC_MOD;PERIODIC_PROPERTY;periodic]);;

let SCS_OPP_REFL=
prove(`is_scs_v39 s
==> (scs_opp_v39 ((scs_opp_v39 s)))=s`,

SIMP_TAC[scs_opp_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;is_scs_v39;BBprime_v39;is_scs_v39;DUAL_PEROPP2;DUAL_PEROPP]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<= scs_k_v39 s==> ~(scs_k_v39 s=0)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[scs_opp_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;is_scs_v39;BBprime_v39;is_scs_v39;DUAL_PEROPP2;DUAL_PEROPP]
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;scs_v39_explicit;scs_k_v39;
scs_d_v39;scs_a_v39 ;
  scs_am_v39 ;
  scs_bm_v39 ;
  scs_b_v39 ;
  scs_J_v39 ;
  scs_lo_v39 ;
  scs_hi_v39 ;
  scs_str_v39;
scs_v39;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.drop3;FST;
Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop1;
Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.drop2;
Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.drop3;
Misc_defs_and_lemmas.part4;Misc_defs_and_lemmas.drop0;
Misc_defs_and_lemmas.part5;
Misc_defs_and_lemmas.part7;
Misc_defs_and_lemmas.part8;
Misc_defs_and_lemmas.part0;]));;






let K_SCS_OPP=
prove(`scs_k_v39 (scs_opp_v39 s) = scs_k_v39 s`,

REWRITE_TAC[scs_v39_explicit;scs_opp_v39;LET_DEF;LET_END_DEF;is_scs_v39;peropp]
);;

let DUAL_NEG_PEROPP=
prove(`~(k=0) /\ periodic ww k==>(\i. --peropp (\i. --peropp (ww:num->real^N) k i) k i)= ww`,

STRIP_TAC
THEN ASM_SIMP_TAC[FUN_EQ_THM;peropp;OPP_SUC_MOD;VECTOR_ARITH`-- -- A=A:real^N`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`ww:num->real^N`][ARITH_3_TAC;]);;




let DUALNEG_PEROPP_BB=
prove(`scs_k_v39 s=k /\BBs_v39 (scs_opp_v39 s) ww /\ ~(k<=3)
==> (\i. --peropp (\i. --peropp (ww:num->real^3) k i) k i)= ww`,

STRIP_TAC
THEN MATCH_MP_TAC DUAL_NEG_PEROPP
THEN ASM_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;BBs_v39;scs_opp_v39]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC);;


let BBPRIME_EQ_OPP_SYM_0=
prove(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime_v39 s vv /\ ~(k<=3)
==> BBprime_v39 (scs_opp_v39 s) (\i. -- peropp vv k i)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC PEROPP_IN_BB_SYM_0
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL OPP_IS_SCS)[`scs_opp_v39 s`;`s:scs_v39`]
THEN MP_TAC SCS_OPP_REFL
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;BBprime_v39]
THEN REPEAT RESA_TAC
THENL[
MRESAL_TAC (GEN_ALL PEROPP_IN_BB_SYM_0)[`scs_opp_v39 s`;`ww:num->real^3`;`k:num`][K_SCS_OPP;]
THEN MP_TAC TAUSTAR_EQ_SYM_0
THEN RESA_TAC
THEN MP_TAC DUALNEG_PEROPP_BB
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_SYM_0)[`k:num`;`s:scs_v39`;`(\i. --peropp (ww:num->real^3) k i)`]
THEN REPLICATE_TAC (13-3)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`(\i. --peropp (ww:num->real^3) k i)`[ARITH_3_TAC]);
MP_TAC TAUSTAR_EQ_SYM_0
THEN RESA_TAC]);;



let BBINDEX_EQ_SYM_0=
prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime_v39 s vv /\ ~(k<=3)
==>
BBindex_v39 (scs_opp_v39 s) (\i. --peropp vv k i) = BBindex_v39 s vv`,

[
STRIP_TAC
THEN ASM_REWRITE_TAC[BBindex_v39;scs_opp_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;peropp;DIST_SYM_0]
THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`)
THEN RESA_TAC
THEN MATCH_MP_TAC CARD_IMAGE_INJ_EQ
THEN REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`(\x:num. (k - SUC(SUC (x MOD k)MOD k)))`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

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

STRIP_TAC;

GEN_TAC
THEN RESA_TAC;

ASM_SIMP_TAC[OPP_SUC_MOD]
THEN MRESA_TAC MOD_LT[`x:num`;`k:num`]
THEN MRESA_TAC DIVISION[`SUC x:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC x MOD k< k/\ ~(k<=3)==> k - SUC (SUC x MOD k) < k /\ SUC (k-1)=k/\ k-1<k`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x<k==> x=k-1\/ SUC x<k`)
THEN RESA_TAC;

MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
THEN REPLICATE_TAC (15-6)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2;is_scs_v39;LET_DEF;LET_END_DEF;BBprime_v39;BBs_v39]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (k-1)`][ARITH_3_TAC;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_3_TAC;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REPLICATE_TAC (4)(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN REPEAT RESA_TAC;

MRESA_TAC DIVISION[`SUC x:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC x<k==> SUC (k - SUC (SUC x))= k- SUC x/\ k - SUC x<k/\ k - SUC (k - SUC x)=x`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k- SUC x`;`k:num`]
THEN MRESA_TAC MOD_LT[`SUC x`;`k:num`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2;is_scs_v39;LET_DEF;LET_END_DEF;BBprime_v39;BBs_v39]
THEN REPEAT RESA_TAC;

REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[EXISTS_UNIQUE]
THEN EXISTS_TAC`k-SUC(SUC y  MOD k)`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC DIVISION[`SUC y`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC y MOD k<k/\ ~(k<=3) ==> k - SUC (SUC y MOD k) < k/\ SUC(k-1)=k/\ k-1<k/\ SUC 0=1/\ k-k=0`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[OPP_SUC_MOD;MOD_SUC_MOD]
THEN MP_TAC(ARITH_RULE`y<k==> y=k-1\/ SUC y<k`)
THEN RESA_TAC;

MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
THEN STRIP_TAC;

REPLICATE_TAC (16-6)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2;is_scs_v39;LET_DEF;LET_END_DEF;BBprime_v39;BBs_v39]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (k-1)`][ARITH_3_TAC;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_3_TAC;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REPLICATE_TAC (4)(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN REPEAT RESA_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);

REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC MOD_LT[`y':num`;`k:num`]
THEN STRIP_TAC
THEN MRESA_TAC DIVISION[`SUC y':num`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC y' MOD k< k /\ k - SUC (SUC y' MOD k) = k - 1 ==> SUC y' MOD k=0`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`y'<k /\ ~(k<=3) ==> SUC y'<k\/ y'=k-1`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`];

MRESA_TAC MOD_LT[`SUC y`;`k:num`]
THEN MP_TAC(ARITH_RULE`SUC y<k==> k- SUC(SUC y)<k/\ SUC (k - SUC (SUC y))= k- SUC y/\ k- SUC y< k/\ k - SUC (k - SUC y) = y`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k- SUC(SUC y)`;`k:num`]
THEN MRESA_TAC MOD_LT[`k- (SUC y)`;`k:num`]
THEN MRESA_TAC MOD_LT[`y:num`;`k:num`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REPLICATE_TAC (22-6)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2;is_scs_v39;LET_DEF;LET_END_DEF;BBprime_v39;BBs_v39]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MP_TAC(ARITH_RULE`y'<k /\ 3<=k ==> SUC y'<k\/ y'=k-1`)
THEN RESA_TAC;

MRESA_TAC MOD_LT[`SUC y'`;`k:num`]
THEN MRESA_TAC MOD_LT[`y':num`;`k:num`]
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`k- SUC(SUC y')=y/\ SUC y'<k /\ SUC y<k ==> y'= k-SUC(SUC y)`)
THEN RESA_TAC;

MRESA_TAC MOD_LT[`k-1`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`]
THEN MP_TAC(ARITH_RULE`SUC y<k /\ ~(k<=3)==> ~(k-1=y)`)
THEN RESA_TAC]);;

let IMAGE_BBINDEX_SYM_0=
prove(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime_v39 s vv /\ ~(k<=3)
==>(IMAGE (BBindex_v39 (scs_opp_v39 s)) (BBprime_v39 (scs_opp_v39 s))) =
  (IMAGE (BBindex_v39 s) (BBprime_v39 s))`,

REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION]
THEN REWRITE_TAC[IN]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THENL[
MRESA_TAC(GEN_ALL OPP_IS_SCS)[`scs_opp_v39 s`;`s:scs_v39`]
THEN MP_TAC SCS_OPP_REFL
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL BBPRIME_EQ_OPP_SYM_0)[`scs_opp_v39 s`;`x':num->real^3`;`k:num`][K_SCS_OPP;]
THEN EXISTS_TAC`(\i. --peropp (x':num->real^3) k i)`
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
THEN REPEAT RESA_TAC
THEN MRESA_TAC(GEN_ALL DUALNEG_PEROPP_BB)[`s:scs_v39`;`k:num`;`x':num->real^3`]
THEN MRESAL_TAC (GEN_ALL BBINDEX_EQ_SYM_0)[`k:num`;`s:scs_v39`;`(\i. --peropp (x':num->real^3) k i)`][BBprime_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;];

EXISTS_TAC`(\i. --peropp (x':num->real^3) k i)`
THEN MRESAL_TAC (GEN_ALL BBPRIME_EQ_OPP_SYM_0)[`s:scs_v39`;`x':num->real^3`;`k:num`][K_SCS_OPP;]
THEN MRESA_TAC (GEN_ALL BBINDEX_EQ_SYM_0)[`k:num`;`s:scs_v39`;`(x':num->real^3)`]]);;

let BBINDEX_MIN_SYM_0=
prove(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime_v39 s vv /\ ~(k<=3)
==> BBindex_min_v39 (scs_opp_v39 s) =BBindex_min_v39 (s)`,

STRIP_TAC
THEN ASM_REWRITE_TAC[BBindex_min_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;peropp;DIST_SYM_0]
THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC IMAGE_BBINDEX_SYM_0
THEN RESA_TAC);;



let BBPRIME2_SYM_0=
prove(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime2_v39 s vv /\ ~(k<=3)
==> BBprime2_v39 (scs_opp_v39 s) (\i. -- peropp vv k i)`,

STRIP_TAC
THEN MP_TAC BBPRIME_EQ_OPP_SYM_0
THEN RESA_TAC
THEN MP_TAC BBINDEX_EQ_SYM_0
THEN RESA_TAC
THEN MP_TAC BBINDEX_MIN_SYM_0
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;BBprime2_v39]
THEN REPEAT RESA_TAC)
;;

let MM_SCS_OPP=
prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ MMs_v39 s vv /\ ~(k<=3)
==> MMs_v39 (scs_opp_v39 s) (\i. -- peropp vv k i)`,

[
STRIP_TAC
THEN MP_TAC BBPRIME2_SYM_0
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;MMs_v39;scs_opp_v39;peropp;AZIM_NEG;BBprime2_v39;BBprime_v39]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`V= IMAGE (vv:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((vv:num->real^3) i, vv (SUC i))) (:num)`
THEN MP_TAC LOCAL_FAN_DUAL_SYM_0
THEN RESA_TAC;

SUBGOAL_THEN`--(vv:num->real^3) (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)) IN
      IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)))
      (:num)` ASSUME_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(i:num)IN(:num)`];

SUBGOAL_THEN`--vv (k - SUC ((i + k - 1) MOD k)),--vv (k - SUC (i MOD k)) IN
      IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)))
      (:num)`ASSUME_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`i+k-1:num`
THEN ASM_REWRITE_TAC[SET_RULE`(i:num)IN(:num)`]
THEN MP_TAC(ARITH_RULE`~(k<=3)==> SUC(i+k-1)=1*k+i/\ ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`i:num`];

MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)
[`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`;`
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)`;`
       IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)))
       (:num)`;`((--(vv:num->real^3) (k - SUC (i MOD k))) ,(--vv (k - SUC (SUC i MOD k))))`]
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)
[`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`;`
       IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))})
       (:num)`;`
       IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)))
       (:num)`;`((--vv (k - SUC ((i + k - 1) MOD k))), (--(vv:num->real^3) (k - SUC (i MOD k))) )`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN STRIP_TAC
THEN MRESAL_TAC(GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`{--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}`][ELEMENT2_SYM_0;REFL_SYM_0]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM ELEMENT2_SYM_0]
THEN ASM_REWRITE_TAC[SET_RULE`{A} UNION {B,C}={A,B,C}`]
THEN MRESAL_TAC(GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`{--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC ((i + k - 1) MOD k))}`][ELEMENT2_SYM_0;REFL_SYM_0]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM ELEMENT2_SYM_0]
THEN ASM_REWRITE_TAC[SET_RULE`{A} UNION {B,C}={A,B,C}`]
THEN REPEAT STRIP_TAC
THEN ASM_SIMP_TAC[AZIM_NEG]
THEN REPLICATE_TAC (26-6)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(k - SUC (i MOD k))`])
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`~(k<=3)==> SUC(i+k-1)=1*k+i/\ ~(k=0)/\ k-1<k/\ 1<k
/\ k-0=k/\ k - 1 + k - 1= 1*k+k-2/\ 0+1=1/\ 1+1=2/\ 0+k-1=k-1/\ k - (k - 1 + 1)=0/\ 0<k/\ 1 *k+0=k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`i MOD k<k ==> SUC (k - SUC (i MOD k))=k-i MOD k/\ (i MOD k + k - 1) + 1= 1*k + i MOD k`)
THEN RESA_TAC
THEN ASM_TAC 
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;MMs_v39;scs_opp_v39;peropp;AZIM_NEG;BBprime2_v39;BBprime_v39;BBs_v39]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (i MOD k) + k - 1`]
THEN MRESA_TAC th[`k - SUC (SUC i MOD k)`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_SIMP_TAC[ADD1]
THEN MRESA_TAC MOD_LT[`1:num`;`k:num`]
THEN MRESA_TAC MOD_LT[`0:num`;`k:num`]
THEN MRESA_TAC MOD_LT[`k-1:num`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`k-1:num`;`k:num`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`1:num`;`k:num`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`0:num`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`k-2:num`]
THEN MP_TAC(ARITH_RULE`i MOD k=0 \/ 0<i MOD k`)
THEN RESA_TAC;

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`k:num`]);

MP_TAC(ARITH_RULE`0< i MOD k/\ ~(k<=3)/\ i MOD k<k==> i MOD k + k - 1= 1*k+ (i MOD k -1)/\ i MOD k-1<k/\ k - (i MOD k - 1 + 1)= k- i MOD k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`i MOD k-1:num`]
THEN MRESA_TAC MOD_LT[`i MOD k-1`;`k:num`]
THEN MP_TAC(ARITH_RULE`i MOD k<k==> i MOD k=k-1\/ i MOD k +1<k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE`~(k<=3)==>k-1+1=k`)
THEN RESA_TAC;

MRESA_TAC MOD_LT[`i MOD k +1`;`k:num`]
THEN MP_TAC(ARITH_RULE`i MOD k +1<k==> k - (i MOD k + 1) + k - 1= 1*k+(k - ((i MOD k + 1) + 1))`)
THEN RESA_TAC
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`k - ((i MOD k + 1) + 1)`];

ASM_REWRITE_TAC[NORM_NEG]
THEN REPLICATE_TAC (20-7)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(k - SUC (i MOD k))`]) ;

ASM_REWRITE_TAC[NORM_NEG]
THEN REPLICATE_TAC (20-8)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(k - SUC (i MOD k))`]);

ASM_REWRITE_TAC[DIST_SYM_0]
THEN REPLICATE_TAC (20-8)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(k - SUC (i MOD k))`]);

ASM_REWRITE_TAC[DIST_SYM_0]
THEN REPLICATE_TAC (20-8)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(k - SUC (i MOD k))`])]) ;;


let YXIONXL2=
prove_by_refinement( `!s.
  is_scs_v39 s /\ scs_k_v39 s=k /\ ~(k<=3) ==> scs_arrow_v39 {s} {scs_opp_v39 s}`,

[REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;subdiv_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC;
MRESA_TAC(GEN_ALL OPP_IS_SCS)[`(scs_opp_v39 s)`;`s:scs_v39`];

DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);

ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN EXISTS_TAC`scs_opp_v39 s`
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv. vv IN A`;IN]
THEN STRIP_TAC
THEN EXISTS_TAC`(\i. -- peropp (vv:num->real^3) k i)`
THEN ASM_SIMP_TAC[MM_SCS_OPP]]);;

 end;;


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