(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================= *)




module   Tecoxbm = struct



open Wjscpro;;
open Polyhedron;;
open Sphere;;
open Fan_defs;;
open Hypermap;;
open Vol1;;
open Fan;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Sphere;;
open Hypermap;;
open Fan;;
open Topology;;
open Prove_by_refinement;;
open Pack_defs;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;


let CROSS_DOT_POS_SY=
prove_by_refinement(`!l:real^(M,3)finite_product. stable_system k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ k= dimindex(:M)/\ 2<k/\
u IN V_SY(vecmats(l))
/\ 1<= i /\ i<= dimindex (:M)
/\ row i (vecmats l)=y
/\  row (SUC (i MOD dimindex (:M))) (vecmats l)=z
/\l IN B_SY1 a b
==> &0<= (y cross z) dot u `,

[REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY]
THEN REPEAT STRIP_TAC
THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
THEN POP_ASSUM MP_TAC 
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN STRIP_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MP_TAC th
THEN REWRITE_TAC[convex_local_fan]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th1-> MP_TAC th1
THEN REWRITE_TAC[local_fan]
THEN LET_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
THEN STRIP_TAC
THEN ASSUME_TAC th1)
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN ASSUME_TAC th)
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
THEN SUBGOAL_THEN `(y,z)IN F_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[];
MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`y:real^3`;`z:real^3`;`(l:real^(M,3)finite_product)`]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z:real^3`;`y:real^3`]
THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
THEN REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.PGSQVBL)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`w:real^3`;`(y,z):real^3#real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
THEN RESA_TAC;
MRESAL_TAC (GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`;`y:real^3`;`z:real^3`;`vec 0:real^3`][VECTOR_ARITH`A -vec 0= A`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`u IN V_SY (vecmats (l:real^(M,3)finite_product))
/\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
==> &0<= (y cross z) dot u`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`y:real^3`;`z:real^3`;`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`]
THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
&0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
THEN ASM_REWRITE_TAC[azim]
THEN STRIP_TAC;
MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM MP_TAC
THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}
\/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY]
THEN ARITH_TAC;
MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
MP_TAC(REAL_ARITH`
&0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
      pi
==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
      &0 \/
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
      pi)`)
THEN RESA_TAC
THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN STRIP_TAC
THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`u IN V_SY (vecmats (l:real^(M,3)finite_product))
/\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
 aff_ge
 {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
 {z}
==> &0<= (y cross z) dot u`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC]);;

let IVS_RHO_NODE_IN_EDGE = 
prove(`!v. local_fan (V,E,FF) /\ v IN V ==> {v,ivs_rho_node1 FF v} IN E`,

NHANH EXISTS_INVERSE_OF_V THEN REPEAT STRIP_TAC 
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC(GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;
`FF:real^3#real^3->bool`;`vv:real^3`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;
`FF:real^3#real^3->bool`;`rho_node1 (FF:real^3#real^3->bool) vv`;`vv:real^3`]
THEN MP_TAC(SET_RULE`EE (rho_node1 FF vv) E = {rho_node1 FF (rho_node1 FF vv), vv} ==> vv IN EE (rho_node1 FF vv) (E:(real^3->bool)->bool) `)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REWRITE_TAC[EE;IN_ELIM_THM]);;

let RHO_IVS_IDD = 
prove(` local_fan (V,E,FF) /\ v IN V
==> rho_node1 FF ( ivs_rho_node1 FF v ) = v `,

NHANH EXISTS_INVERSE_OF_V 
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;
`FF:real^3#real^3->bool`;`vv:real^3`]);;


let PROPERTIES_OF_FAN_IN_B_SY=
prove_by_refinement(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ dimindex(:M)= k/\ 2<k
/\ 1<= i /\ i<= dimindex (:M)
/\ 1<= j /\ j<= dimindex (:M)
/\ ~(i=j)
/\ row i (vecmats l)=y
/\  row j (vecmats l)=z
/\l IN B_SY1 a b
==> &2<= norm (y-z)  `,

[REPEAT STRIP_TAC
THEN ASM_TAC
THEN DISCH_THEN(LABEL_TAC"THYGIANG")
THEN REPEAT STRIP_TAC
THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;CONDITION1_SY] THEN STRIP_TAC)
THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
THEN POP_ASSUM MP_TAC 
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN DISCH_THEN(LABEL_TAC"THY2")
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MP_TAC th
THEN REWRITE_TAC[convex_local_fan]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th1-> MP_TAC th1
THEN REWRITE_TAC[local_fan]
THEN LET_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
THEN STRIP_TAC
THEN ASSUME_TAC th1)
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN ASSUME_TAC th)
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
THEN REMOVE_THEN"THY2"(fun th-> MRESA_TAC th[`i:num`;`j:num`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN "THYGIANG" MP_TAC
THEN REWRITE_TAC[stable_system]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THYGIANG2")
THEN MP_TAC(ARITH_RULE`i<= dimindex (:M)==> i <= dimindex (:M)-1 \/ i = dimindex (:M)`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)
THEN RESA_TAC;

STRIP_TAC
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`j:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

MP_TAC(ARITH_RULE`1<= i /\ 2< k==> ~(i = 0) /\ ~(k=0)/\ 1<k /\ 1<=k`)
THEN RESA_TAC
THEN STRIP_TAC
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`0:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]
THEN REMOVE_THEN "THYGIANG2" MP_TAC
THEN REWRITE_TAC[constraint_system]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ k+k=k *2`])
THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]
THEN REAL_ARITH_TAC;

MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE`2< k==> ~(k = 0)/\ 1<=k /\ 1<k`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]
THEN REMOVE_THEN "THYGIANG2" MP_TAC
THEN REWRITE_TAC[constraint_system]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ k+k= k*2`])
THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`)
THEN RESA_TAC
THEN STRIP_TAC
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th])
THEN SET_TAC[]]);;

let AFF_GT_INTER_AFF_SY=
prove_by_refinement(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ dimindex(:M)= k/\ 2<k/\
{u,w} SUBSET V_SY(vecmats(l))
/\ norm(u-w)<= cstab
/\ &2<= norm(u-w)
/\ ~({u,w} IN E_SY(vecmats l))
/\ 1<= i /\ i<= dimindex (:M)
/\ row i (vecmats l)=y
/\  row (SUC (i MOD dimindex (:M))) (vecmats l)=z
/\l IN B_SY1 a b
==> aff_gt {vec 0}{u,w} INTER aff {vec 0,y,z}={} `,

[REPEAT STRIP_TAC
THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY] THEN STRIP_TAC)
THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
THEN POP_ASSUM MP_TAC 
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN STRIP_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MP_TAC th
THEN REWRITE_TAC[convex_local_fan]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th1-> MP_TAC th1
THEN REWRITE_TAC[local_fan]
THEN LET_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
THEN STRIP_TAC
THEN ASSUME_TAC th1)
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN ASSUME_TAC th)
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
THEN SUBGOAL_THEN `(y,z)IN F_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[];
MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`y:real^3`;`z:real^3`;`(l:real^(M,3)finite_product)`]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z:real^3`;`y:real^3`]
THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
THEN SUBGOAL_THEN `u IN ball_annulus` ASSUME_TAC;
MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l) ==> u IN V_SY (vecmats (l:real^(M,3)finite_product))`)
THEN ASM_REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
THEN STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i':num`);
SUBGOAL_THEN `w IN ball_annulus` ASSUME_TAC;
MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l) ==> w IN V_SY (vecmats (l:real^(M,3)finite_product))`)
THEN ASM_REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
THEN STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i':num`);
MRESAL_TAC (GEN_ALL NONPARALLEL_BALL_ANNULUS)[`u:real^3`;`w:real^3`][SET_RULE`{A} UNION {B,C}={A,B,C}`]
THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`u:real^3`;`w:real^3`]
THEN REWRITE_TAC[SET_RULE`A= {}<=> ~(?x1.  x1 IN A)`;INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`;DOT_RADD;DOT_RMUL];
SUBGOAL_THEN`&0<=(y cross z) dot u/\ &0<=(y cross z) dot w` ASSUME_TAC;
REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.PGSQVBL)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`w:real^3`;`(y,z):real^3#real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
THEN RESA_TAC;
MRESAL_TAC (GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`;`y:real^3`;`z:real^3`;`vec 0:real^3`][VECTOR_ARITH`A -vec 0= A`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
/\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
==> &0<= (y cross z) dot u /\ &0<= (y cross z) dot w`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`y:real^3`;`z:real^3`;`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`]
THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
&0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
THEN ASM_REWRITE_TAC[azim]
THEN STRIP_TAC;
MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM MP_TAC
THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}
\/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY]
THEN ARITH_TAC;
MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
MP_TAC(REAL_ARITH`
&0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
      pi
==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
      &0 \/
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
      pi)`)
THEN RESA_TAC
THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN STRIP_TAC
THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
/\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
 aff_ge
 {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
 {z}
==> &0<= (y cross z) dot u /\ &0<= (y cross z) dot w`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`&0<=A <=> &0< A \/ A= &0`]
THEN RESA_TAC;
REWRITE_TAC[REAL_ARITH`&0< A \/ A= &0<=> &0<=A `]
THEN STRIP_TAC;
MP_TAC(REAL_ARITH`&0< t3==> &0<= t3`)
THEN RESA_TAC
THEN MRESA_TAC REAL_LT_MUL[`t2:real`;`(y cross z) dot u`]
THEN MRESA_TAC REAL_LE_MUL[`t3:real`;`(y cross z) dot w`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC;
MRESA_TAC REAL_LT_MUL[`t3:real`;`(y cross z) dot w`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN ABBREV_TAC`y1= rho_node1 (F_SY(vecmats (l:real^(M,3)finite_product))) u`
THEN ABBREV_TAC`z1= ivs_rho_node1 (F_SY(vecmats (l:real^(M,3)finite_product))) u`
THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
==> u IN V_SY (vecmats (l:real^(M,3)finite_product))`)
THEN RESA_TAC
THEN SUBGOAL_THEN`y1 IN V_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th `SUC 0`[ITER;I_DEF;o_DEF]);
SUBGOAL_THEN`z1 IN V_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
MRESA_TAC (GEN_ALL Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`u:real^3`)
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th `CARD (V_SY (vecmats (l:real^(M,3)finite_product))) - 1`[]);
SUBGOAL_THEN`&0<= (y cross z) dot y1/\ &0<= (y cross z) dot z1`ASSUME_TAC;
REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.PGSQVBL)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`w:real^3`;`(y,z):real^3#real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
THEN RESA_TAC;
MRESAL_TAC (GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`;`y:real^3`;`z:real^3`;`vec 0:real^3`][VECTOR_ARITH`A -vec 0= A`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))
/\ z1 IN V_SY (vecmats (l:real^(M,3)finite_product))
/\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
==> &0<= (y cross z) dot y1 /\ &0<= (y cross z) dot z1`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`y:real^3`;`z:real^3`;`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`]
THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
&0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
THEN ASM_REWRITE_TAC[azim]
THEN STRIP_TAC;
MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM MP_TAC
THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}
\/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY]
THEN ARITH_TAC;
MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
MP_TAC(REAL_ARITH`
&0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
      pi
==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
      &0 \/
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
      pi)`)
THEN RESA_TAC
THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN STRIP_TAC
THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))
/\ z1 IN V_SY (vecmats (l:real^(M,3)finite_product))
/\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
 aff_ge
 {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
 {z}
==> &0<= (y cross z) dot y1 /\ &0<= (y cross z) dot z1 `)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"CHANGE")
THEN STRIP_TAC
THEN STRIP_TAC
THEN DISCH_THEN(LABEL_TAC"THY4")
THEN REMOVE_THEN"CHANGE" (fun th-> ASSUME_TAC th THEN
MP_TAC th THEN REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
THEN STRIP_TAC)
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN SUBGOAL_THEN`u,row (SUC (i' MOD k)) (vecmats l) IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i':num`
THEN ASM_REWRITE_TAC[];
MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`u:real^3,row (SUC (i' MOD k)) (vecmats (l:real^(M,3)finite_product))`[PAIR_EQ])
THEN MRESA_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`y1:real^3`;`y:real^3`;`l:real^(M,3)finite_product`]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`y1:real^3`;`z:real^3`;`l:real^(M,3)finite_product`]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`y1:real^3`;`z1:real^3`;`l:real^(M,3)finite_product`]
THEN SUBGOAL_THEN(` &0 <= (z1 cross u) dot w /\ &0 <= (z1 cross u) dot y /\ &0 <= (z1 cross u) dot z  `)ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=i'==> i'=1 \/ 1<= i'-1`)
THEN RESA_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
THEN MP_TAC(ARITH_RULE`2<k==> 1<= k/\ k<=k`)
THEN RESA_TAC
THEN SUBGOAL_THEN`row k (vecmats l), u IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`k:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`row k (vecmats (l:real^(M,3)finite_product)):real^3,u:real^3`[PAIR_EQ])
THEN FIND_ASSUM MP_TAC`ivs_rho_node1 (F_SY (vecmats (l:real^(M,3)finite_product))) u=z1`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
THEN SUBGOAL_THEN`row k (vecmats l) IN V_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`k:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
MRESA_TAC(GEN_ALL Local_lemmas.IVS_RHO_IDD) [`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`(row k (vecmats (l:real^(M,3)finite_product)))`]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`k:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`y:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`k:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`z:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
==> w IN V_SY (vecmats l) `)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`k:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`];
MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==> i'-1 < dimindex (:M)/\ i'-1 <= dimindex (:M)`)
THEN RESA_TAC 
THEN MRESAL_TAC MOD_LT[`i'-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
==> w IN V_SY (vecmats l) `)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'-1:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`y:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'-1:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`z:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'-1:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==>  SUC (i'-1)=i'`)
THEN RESA_TAC 
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN SUBGOAL_THEN`row (i'-1) (vecmats l), u IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i'-1:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`]
THEN MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==>  SUC (i'-1)=i'`)
THEN RESA_TAC 
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]);
MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`row (i'-1) (vecmats (l:real^(M,3)finite_product)):real^3,u:real^3`[PAIR_EQ])
THEN FIND_ASSUM MP_TAC`ivs_rho_node1 (F_SY (vecmats (l:real^(M,3)finite_product))) u=z1`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
THEN SUBGOAL_THEN`row (i'-1) (vecmats l) IN V_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i'-1:num`
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
MRESA_TAC(GEN_ALL Local_lemmas.IVS_RHO_IDD) [`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`(row (i'-1) (vecmats (l:real^(M,3)finite_product)))`]
THEN RESA_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`u IN aff{vec 0, y,z:real^3}` ASSUME_TAC;
ASM_REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`;IN_ELIM_THM];
POP_ASSUM MP_TAC
THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
THEN STRIP_TAC 
THEN POP_ASSUM (fun th-> REWRITE_TAC[th] THEN ASSUME_TAC (SYM th))
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;DOT_LADD;DOT_LMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A /\ &0+ A=A`;CROSS_RADD;CROSS_RMUL;]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN MP_TAC(REAL_ARITH`&0 <= (y cross z) dot y1 ==> ~((y cross z) dot y1< &0)`)
THEN RESA_TAC
THEN SUBGOAL_THEN`(y cross z1) dot z<= &0` ASSUME_TAC;
ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_SKEW]
THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- A<= &0<=> &0<= A`];
MP_TAC(REAL_ARITH` (y cross z1) dot z<= &0 ==> ~(&0< (y cross z1) dot z)`)
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN SUBGOAL_THEN`(y cross z1) dot z= &0 \/ (y cross z) dot y1= &0` ASSUME_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
THEN SUBGOAL_THEN`~(w' = &0 /\ v'= &0)` ASSUME_TAC;
STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN REWRITE_TAC[VECTOR_ARITH`&0 % A= vec 0/\ vec 0+ vec 0= vec 0`]
THEN REPEAT STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[SET_RULE`~(A /\ B)<=> ~A \/ ~B`]
THEN RESA_TAC;
RESA_TAC;
MP_TAC(REAL_ARITH`w'< &0==> ~(&0 < w')`)
THEN RESA_TAC
THEN SET_TAC[];
DISCH_TAC
THEN REMOVE_ASSUM_TAC
THEN RESA_TAC;
POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[CROSS_SKEW]
THEN ASM_REWRITE_TAC[DOT_LNEG;]
THEN REAL_ARITH_TAC;
MP_TAC(REAL_ARITH`v'< &0==> ~(&0 < v')`)
THEN RESA_TAC
THEN STRIP_TAC;
ONCE_REWRITE_TAC[CROSS_SKEW]
THEN ASM_REWRITE_TAC[DOT_LNEG;]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[CROSS_SKEW]
THEN ASM_REWRITE_TAC[DOT_LNEG; REAL_ARITH`&0< -- A<=> ~(&0 <= A)`];
POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ASM_REWRITE_TAC[DOT_LNEG; REAL_ARITH` A< &0 <=> ~(&0 <= A)`];
POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
==> w IN V_SY (vecmats l) `)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`y1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]
THEN SUBGOAL_THEN`w IN aff{vec 0, y,z:real^3}` ASSUME_TAC;
ASM_REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`;IN_ELIM_THM];
STRIP_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
THEN STRIP_TAC 
THEN STRIP_TAC 
THEN SUBGOAL_THEN`z1 IN aff{vec 0,u,w:real^3}` ASSUME_TAC;
MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`w:real^3`]
THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
THEN EXPAND_TAC"u"
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;DOT_LADD;DOT_LMUL;CROSS_RADD;CROSS_RMUL;DOT_CROSS_SELF;CROSS_REFL;DOT_LZERO]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_SKEW]
THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN STRIP_TAC
THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC `&0 <= (u cross y1) dot z1`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;DOT_RADD;DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A * &0+B=B`] THEN ASSUME_TAC (SYM th))
THEN MP_TAC(REAL_ARITH`&0 <= (u cross y1) dot w==> (u cross y1) dot w = &0 \/ &0 < (u cross y1) dot w`)
THEN RESA_TAC;
SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i':num`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`]
THEN SUBGOAL_THEN`w IN aff{vec 0,u,y1:real^3}` ASSUME_TAC;
MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`y1:real^3`]
THEN ASM_REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`];
POP_ASSUM MP_TAC
THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
THEN STRIP_TAC 
THEN POP_ASSUM (fun th-> ASSUME_TAC (SYM th))
THEN DISJ_CASES_TAC(REAL_ARITH`w''''< &0 \/ &0<= w''''`);
SUBGOAL_THEN`w IN aff_lt{vec 0,u} {y1:real^3}` ASSUME_TAC;
ASM_SIMP_TAC[AFF_LT_2_1;IN_ELIM_THM]
THEN EXISTS_TAC`u'''':real`
THEN EXISTS_TAC`v'''':real`
THEN EXISTS_TAC`w'''':real`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`];
MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`]
THEN MRESA_TAC AZIM_EQ_PI_ALT[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`]
THEN SUBGOAL_THEN`coplanar{vec 0, u, y1, z1:real^3} `ASSUME_TAC;
ASM_SIMP_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT;VECTOR_ARITH`A- vec 0=A`]
THEN EXPAND_TAC"z1"
THEN REWRITE_TAC[DOT_RADD;DOT_RMUL]
THEN ASM_REWRITE_TAC[DOT_CROSS_SELF]
THEN REAL_ARITH_TAC;
MRESA_TAC(GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`]
THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`z1:real^3`];
MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`;`y1:real^3`;`z1:real^3`]
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real^3`)
THEN MRESA_TAC(GEN_ALL RHO_IVS_IDD)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`];
POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`z1:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`w IN aff_gt {vec 0, u} {z1}
/\  aff_gt {vec 0, u} {z1} SUBSET aff_ge {vec 0, u} {z1}
==> w IN aff_ge {vec 0, u} {z1:real^3}`)
THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
THEN STRIP_TAC
THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z1:real^3`;`u:real^3`];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN ASM_REWRITE_TAC[];
DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
THEN RESA_TAC
THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[];
FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
THEN REWRITE_TAC[FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,z1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
/\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
/\ w IN aff_ge {vec 0} {u, z1}
==> vec 0= w:real^3`)
THEN RESA_TAC;
SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {y1}` ASSUME_TAC;
ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
THEN EXISTS_TAC`u'''':real`
THEN EXISTS_TAC`v'''':real`
THEN EXISTS_TAC`w'''':real`
THEN ASM_REWRITE_TAC[]
THEN VECTOR_ARITH_TAC;
MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN ASM_REWRITE_TAC[];
DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
THEN RESA_TAC
THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[];
FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
THEN REWRITE_TAC[FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,y1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
/\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
/\ w IN aff_ge {vec 0} {u, y1}
==> vec 0= w:real^3`)
THEN RESA_TAC;
MP_TAC(REAL_ARITH`&0 < (u cross y1:real^3) dot w ==> ~((u cross y1) dot w = &0) /\ ~((u cross y1) dot w < &0)`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
THEN STRIP_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN REWRITE_TAC[VECTOR_ARITH`&0 %A= vec 0/\ A + vec 0=A`]
THEN REPEAT STRIP_TAC
THEN SUBGOAL_THEN`z1 IN aff{vec 0, u:real^3}`ASSUME_TAC;
REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
THEN EXISTS_TAC`&1- v''':real`
THEN EXISTS_TAC`v''':real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - v''' + v''' = &1`]
THEN VECTOR_ARITH_TAC;
MRESA_TAC(GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`]
THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`z1:real^3`];
POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`]
THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`z1:real^3`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {z1}` ASSUME_TAC;
ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
THEN EXISTS_TAC`&1 + (inv w''') *v''' - inv w''':real`
THEN EXISTS_TAC`-- (inv w''') *v''':real`
THEN EXISTS_TAC`inv w''':real`
THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 + inv w''' * v''' - inv w''') + --inv w''' * v''' + inv w''' = &1`]
THEN EXPAND_TAC"z1"
THEN REWRITE_TAC[VECTOR_ARITH`(&1 + inv w''' * v''' - inv w''') % vec 0 +
 (--inv w''' * v''') % u +
 inv w''' % (v''' % u + w''' % w)
= (inv w''' *w''') % w`]
THEN MP_TAC(REAL_ARITH`&0< w'''==> ~(w'''= &0)`)
THEN RESA_TAC
THEN MRESAL1_TAC REAL_MUL_LINV`w''':real`[VECTOR_ARITH`A= &1 %A`]
THEN MATCH_MP_TAC REAL_LE_INV
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"A")
THEN STRIP_TAC
THEN REMOVE_THEN"A" MP_TAC
THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC th3[`u:real^3`;`z1:real^3`;`vec 0:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC;
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`]
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_REWRITE_TAC[];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN ASM_REWRITE_TAC[];
DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`];
MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
THEN RESA_TAC
THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[];
MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`]
THEN FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
THEN REWRITE_TAC[FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,z1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
/\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
/\ w IN aff_ge {vec 0} {u, z1}
==> vec 0= w:real^3`)
THEN RESA_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
THEN STRIP_TAC 
THEN STRIP_TAC 
THEN SUBGOAL_THEN`y1 IN aff{vec 0,u,w:real^3}` ASSUME_TAC;
MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`w:real^3`]
THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
THEN EXPAND_TAC"u"
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;DOT_LADD;DOT_LMUL;CROSS_RADD;CROSS_RMUL;DOT_CROSS_SELF;CROSS_REFL;DOT_LZERO]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[CROSS_SKEW]
THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN STRIP_TAC
THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC `&0 <= (u cross y1) dot z1`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;CROSS_RADD;CROSS_RMUL;DOT_LADD;DOT_LMUL;DOT_CROSS_SELF;] THEN ASSUME_TAC (SYM th))
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN REWRITE_TAC[DOT_CROSS_SELF;REAL_ARITH`A * &0+B=B`]
THEN MP_TAC(REAL_ARITH`&0 <= (z1 cross u) dot w==> (z1 cross u) dot w = &0 \/ &0 < (z1 cross u) dot w`)
THEN RESA_TAC;
SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i':num`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z1:real^3`;`u:real^3`]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`]
THEN SUBGOAL_THEN`w IN aff{vec 0,u,z1:real^3}` ASSUME_TAC;
MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`z1:real^3`]
THEN ASM_REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
THEN ONCE_REWRITE_TAC[CROSS_SKEW]
THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
THEN STRIP_TAC 
THEN POP_ASSUM (fun th-> ASSUME_TAC (SYM th))
THEN DISJ_CASES_TAC(REAL_ARITH`w''''< &0 \/ &0<= w''''`);
SUBGOAL_THEN`w IN aff_lt{vec 0,u} {z1:real^3}` ASSUME_TAC;
ASM_SIMP_TAC[AFF_LT_2_1;IN_ELIM_THM]
THEN EXISTS_TAC`u'''':real`
THEN EXISTS_TAC`v'''':real`
THEN EXISTS_TAC`w'''':real`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`];
MRESA_TAC AZIM_EQ_PI_ALT[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`]
THEN SUBGOAL_THEN`coplanar{vec 0, u, z1, y1:real^3} `ASSUME_TAC;
ASM_SIMP_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT;VECTOR_ARITH`A- vec 0=A`]
THEN EXPAND_TAC"y1"
THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_LADD;CROSS_LADD;DOT_RADD;DOT_RMUL;CROSS_REFL]
THEN ASM_REWRITE_TAC[DOT_CROSS_SELF;]
THEN ONCE_REWRITE_TAC[CROSS_SKEW]
THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
THEN REAL_ARITH_TAC;
MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`y1:real^3`];
MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`;`z1:real^3`;`y1:real^3`]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real^3`)
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
THEN MRESA_TAC(GEN_ALL RHO_IVS_IDD)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`];
POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`y1:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`w IN aff_gt {vec 0, u} {y1}
/\  aff_gt {vec 0, u} {y1} SUBSET aff_ge {vec 0, u} {y1}
==> w IN aff_ge {vec 0, u} {y1:real^3}`)
THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
THEN STRIP_TAC
THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[];
DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
THEN RESA_TAC
THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[];
FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
THEN REWRITE_TAC[FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,y1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
/\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
/\ w IN aff_ge {vec 0} {u, y1}
==> vec 0= w:real^3`)
THEN RESA_TAC;
SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {z1}` ASSUME_TAC;
ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
THEN EXISTS_TAC`u'''':real`
THEN EXISTS_TAC`v'''':real`
THEN EXISTS_TAC`w'''':real`
THEN ASM_REWRITE_TAC[]
THEN VECTOR_ARITH_TAC;
MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z1:real^3`;`u:real^3`];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN ASM_REWRITE_TAC[];
DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
THEN RESA_TAC
THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[];
FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
THEN REWRITE_TAC[FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,z1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
/\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
/\ w IN aff_ge {vec 0} {u, z1}
==> vec 0= w:real^3`)
THEN RESA_TAC;
ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN MP_TAC(REAL_ARITH`&0 < (z1 cross u:real^3) dot w ==> ~((z1 cross u) dot w = &0) /\ ~((z1 cross u) dot w < &0)`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
THEN STRIP_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN REWRITE_TAC[VECTOR_ARITH`&0 %A= vec 0/\ A + vec 0=A`]
THEN REPEAT STRIP_TAC
THEN SUBGOAL_THEN`y1 IN aff{vec 0, u:real^3}`ASSUME_TAC;
REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
THEN EXISTS_TAC`&1- v''':real`
THEN EXISTS_TAC`v''':real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - v''' + v''' = &1`]
THEN VECTOR_ARITH_TAC;
SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i':num`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`];
SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i':num`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`]
THEN SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {y1}` ASSUME_TAC;
ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
THEN EXISTS_TAC`&1 + (inv w''') *v''' - inv w''':real`
THEN EXISTS_TAC`-- (inv w''') *v''':real`
THEN EXISTS_TAC`inv w''':real`
THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 + inv w''' * v''' - inv w''') + --inv w''' * v''' + inv w''' = &1`]
THEN EXPAND_TAC"y1"
THEN REWRITE_TAC[VECTOR_ARITH`(&1 + inv w''' * v''' - inv w''') % vec 0 +
 (--inv w''' * v''') % u +
 inv w''' % (v''' % u + w''' % w)
= (inv w''' *w''') % w`]
THEN MP_TAC(REAL_ARITH`&0< w'''==> ~(w'''= &0)`)
THEN RESA_TAC
THEN MRESAL1_TAC REAL_MUL_LINV`w''':real`[VECTOR_ARITH`A= &1 %A`]
THEN MATCH_MP_TAC REAL_LE_INV
THEN ASM_TAC 
THEN REAL_ARITH_TAC;
REMOVE_THEN "THY4" MP_TAC
THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[];
DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
THEN ASM_TAC
THEN SET_TAC[];
MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
THEN RESA_TAC
THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[];
FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
THEN REWRITE_TAC[FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,y1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
/\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
/\ w IN aff_ge {vec 0} {u, y1}
==> vec 0= w:real^3`)
THEN RESA_TAC]);;



let TECOXBM1=
prove_by_refinement(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ k= dimindex(:M)/\ 2<k/\
{u,w} SUBSET V_SY(vecmats(l))
/\ norm(u-w)<= cstab
/\ &2<= norm(u-w)
/\ ~({u,w} IN E_SY(vecmats l))
/\l IN B_SY1 a b
==> (!x. x IN F_SY(vecmats l)==> aff_gt {vec 0}{u,w} SUBSET wedge_in_fan_gt x (E_SY (vecmats l))) `,

[GEN_TAC THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM MP_TAC
THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
THEN POP_ASSUM MP_TAC 
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> MP_TAC th
THEN REWRITE_TAC[convex_local_fan]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th2-> ASSUME_TAC th2 THEN MP_TAC th2
THEN REWRITE_TAC[local_fan]
THEN LET_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th3-> ASSUME_TAC(SYM th3))
THEN STRIP_TAC)
THEN DISCH_THEN(LABEL_TAC"YEU")
THEN ASSUME_TAC th)
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
THEN MP_TAC(SET_RULE`{u,w} SUBSET V_SY(vecmats(l)) ==>  w IN V_SY(vecmats(l:real^(M,3)finite_product)) /\ u IN V_SY(vecmats(l))`)
THEN RESA_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MP_TAC th
THEN REWRITE_TAC[F_SY;IN_ELIM_THM;]
THEN STRIP_TAC
THEN ASSUME_TAC th)
THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))`
THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
THEN SUBGOAL_THEN `y IN V_SY (vecmats (l:real^(M,3)finite_product))`ASSUME_TAC;
REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[];
MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats (l:real^(M,3)finite_product))`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`;]
THEN ASM_REWRITE_TAC[wedge_in_fan_gt;ARITH_RULE`2>1`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`(x:real^3#real^3)`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.PGSQVBL)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`w:real^3`;`x:real^3#real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0:real^3}`;`{u,w:real^3}`]
THEN MP_TAC(SET_RULE`aff_gt {vec 0} {u, w} SUBSET aff_ge {vec 0} {u, w}
/\ aff_ge {vec 0} {u, w} SUBSET wedge_ge (vec 0) y z (azim_cycle (EE y (E_SY (vecmats l))) (vec 0) y z)
==> aff_gt {vec 0} {u, w} SUBSET wedge_ge (vec 0) y z (azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN "YEU"(fun th-> MRESA1_TAC th`x:real^3#real^3`)
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`(x:real^3#real^3)`]
THEN ABBREV_TAC`y1=azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z`
THEN REWRITE_TAC[REAL_ARITH`a<= b<=> a=b\/ a< b`]
THEN STRIP_TAC;
MRESA_TAC(GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`y1:real^3`;`y:real^3`;`z:real^3`;`vec 0:real^3`]
THEN SUBGOAL_THEN`{y,row (SUC (i MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z:real^3`;`y:real^3`]
THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
THEN MRESA_TAC (GEN_ALL Nkezbfc_local.AZIM_PI_WEDGE_CROSS_DOT)[`y1:real^3`;`y:real^3`;`z:real^3`;`vec 0:real^3`]
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
THEN DISCH_THEN(LABEL_TAC"THY4")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN"THY4"(fun th-> MRESA1_TAC th`x'':real^3`)
THEN SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y, z:real^3}` ASSUME_TAC;
ASM_REWRITE_TAC[INTER;IN_ELIM_THM];
MRESAL_TAC(GEN_ALL AFF_GT_INTER_AFF_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i:num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`y:real^3`;`z:real^3`;`l:real^(M,3)finite_product`][B_SY1;IN_ELIM_THM;CONDITION2_SY]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[];
POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`{y,row (SUC (i MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z:real^3`;`y:real^3`]
THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`y:real^3`;`z:real^3`;`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`]
THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
&0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
THEN ASM_REWRITE_TAC[azim]
THEN STRIP_TAC;
MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
THEN POP_ASSUM MP_TAC
THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}
\/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);
POP_ASSUM MP_TAC
THEN RESA_TAC
THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY]
THEN ARITH_TAC;
MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
MP_TAC(REAL_ARITH`
&0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
      pi
==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
      &0 \/
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
      pi)`)
THEN RESA_TAC
THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN STRIP_TAC
THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN MRESA_TAC WEDGE_LUNE[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN RESA_TAC
THEN MRESA_TAC(inter_aff_gt_3_1_is_aff_gt_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC aff_gt_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN MRESAL_TAC aff_gt_3_1_rep_cross_dot [`vec 0:real^3`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN RESA_TAC
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;INTER]
THEN DISCH_THEN(LABEL_TAC"YEU1")
THEN REPEAT STRIP_TAC;
REMOVE_THEN "YEU1"(fun th-> MRESA1_TAC th`x'':real^3`)
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
THEN STRIP_TAC;
SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y, z:real^3}` ASSUME_TAC;
ASM_REWRITE_TAC[INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ASM_REWRITE_TAC[];
MRESAL_TAC(GEN_ALL AFF_GT_INTER_AFF_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i:num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`y:real^3`;`z:real^3`;`l:real^(M,3)finite_product`][B_SY1;IN_ELIM_THM;CONDITION2_SY]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[];
REMOVE_THEN "YEU1"(fun th-> MRESA1_TAC th`x'':real^3`)
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
THEN STRIP_TAC;
SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y1, y:real^3}` ASSUME_TAC;
MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y1:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN MRESA_TAC(GEN_ALL Lvducxu.AZIM_CY_FST_Y_IN_FF)[`x':real^3#real^3`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`vec 0:real^3`;`x:real^3#real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[F_SY;IN_ELIM_THM;PAIR_EQ]
THEN STRIP_TAC
THEN MRESAL_TAC(GEN_ALL AFF_GT_INTER_AFF_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`y1:real^3`;`y:real^3`;`l:real^(M,3)finite_product`][B_SY1;IN_ELIM_THM;CONDITION2_SY]
THEN SET_TAC[]]);;

let TECOXBM2= 
prove(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ k= dimindex(:M)/\ 2<k/\
{u,w} SUBSET V_SY(vecmats(l))
/\ norm(u-w)<= cstab
/\ &2<= norm(u-w)
/\ ~({u,w} IN E_SY(vecmats l))
/\l IN B_SY1 a b
==> ~(collinear ({vec 0} UNION {u,w}))`,

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY] THEN STRIP_TAC)
THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
THEN POP_ASSUM MP_TAC 
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN STRIP_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MP_TAC th
THEN REWRITE_TAC[convex_local_fan]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th1-> MP_TAC th1
THEN REWRITE_TAC[local_fan]
THEN LET_TAC
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
THEN STRIP_TAC
THEN ASSUME_TAC th1)
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN ASSUME_TAC th)
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
THEN MATCH_MP_TAC NONPARALLEL_BALL_ANNULUS
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l)
==> u IN V_SY(vecmats l) /\ w IN V_SY(vecmats (l:real^(M,3)finite_product))`)
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
THEN STRIP_TAC
THEN REMOVE_THEN"THY" (fun th-> MRESA1_TAC th`i:num` THEN  MRESA1_TAC th`i':num` ));;
let TECOXBM=
prove(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ k= dimindex(:M)/\ 2<k/\
{u,w} SUBSET V_SY(vecmats(l))
/\ norm(u-w)<= cstab
/\ &2<= norm(u-w)
/\ ~({u,w} IN E_SY(vecmats l))
/\l IN B_SY1 a b
==> ~(collinear ({vec 0} UNION {u,w}))
/\ (!x. x IN F_SY(vecmats l)==> aff_gt {vec 0}{u,w} SUBSET wedge_in_fan_gt x (E_SY (vecmats l)))`,

GEN_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THENL[MRESA_TAC (GEN_ALL TECOXBM2)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
MRESA_TAC (GEN_ALL TECOXBM1)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]]);;

end;;