text_formalization/local/TECOXBM.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2010-02-09                                                           *)
   7 (* ========================================================================= *)
   8
   9
  10
  11
  12 module   Tecoxbm = struct
  13
  14
  15
  16 open Wjscpro;;
  17 open Polyhedron;;
  18 open Sphere;;
  19 open Fan_defs;;
  20 open Hypermap;;
  21 open Vol1;;
  22 open Fan;;
  23 open Topology;;
  24 open Fan_misc;;
  25 open Planarity;;
  26 open Conforming;;
  27 open Sphere;;
  28 open Hypermap;;
  29 open Fan;;
  30 open Topology;;
  31 open Prove_by_refinement;;
  32 open Pack_defs;;
  33 open Wrgcvdr_cizmrrh;;
  34 open Local_lemmas;;
  35 open Collect_geom;;
  36 open Dih2k_hypermap;;
  37
  38
  39 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/\
  40 u IN V_SY(vecmats(l))
  41 /\ 1<= i /\ i<= dimindex (:M)
  42 /\ row i (vecmats l)=y
  43 /\  row (SUC (i MOD dimindex (:M))) (vecmats l)=z
  44 /\l IN B_SY1 a b
  45 ==> &0<= (y cross z) dot u `,
  46 [REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY]
  47 THEN REPEAT STRIP_TAC
  48 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
  49 THEN POP_ASSUM MP_TAC
  50 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
  51 THEN POP_ASSUM MP_TAC
  52 THEN POP_ASSUM MP_TAC
  53 THEN POP_ASSUM MP_TAC
  54 THEN DISCH_THEN(LABEL_TAC"THY")
  55 THEN STRIP_TAC
  56 THEN STRIP_TAC
  57 THEN POP_ASSUM(fun th-> MP_TAC th
  58 THEN REWRITE_TAC[convex_local_fan]
  59 THEN STRIP_TAC
  60 THEN POP_ASSUM MP_TAC
  61 THEN POP_ASSUM(fun th1-> MP_TAC th1
  62 THEN REWRITE_TAC[local_fan]
  63 THEN LET_TAC
  64 THEN STRIP_TAC
  65 THEN POP_ASSUM MP_TAC
  66 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
  67 THEN STRIP_TAC
  68 THEN ASSUME_TAC th1)
  69 THEN DISCH_THEN(LABEL_TAC"THY1")
  70 THEN ASSUME_TAC th)
  71 THEN STRIP_TAC
  72 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
  73 THEN SUBGOAL_THEN `(y,z)IN F_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
  74 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
  75 THEN EXISTS_TAC`i:num`
  76 THEN ASM_REWRITE_TAC[];
  77 MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`y:real^3`;`z:real^3`;`(l:real^(M,3)finite_product)`]
  78 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`]
  79 THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
  80 THEN REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
  81 THEN POP_ASSUM MP_TAC
  82 THEN POP_ASSUM MP_TAC
  83 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)`]
  84 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))`]
  85 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)`]
  86 THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
  87 THEN RESA_TAC;
  88 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`]
  89 THEN STRIP_TAC
  90 THEN MP_TAC(SET_RULE`u IN V_SY (vecmats (l:real^(M,3)finite_product))
  91 /\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
  92 ==> &0<= (y cross z) dot u`)
  93 THEN RESA_TAC
  94 THEN POP_ASSUM MP_TAC
  95 THEN POP_ASSUM MP_TAC
  96 THEN REAL_ARITH_TAC;
  97 POP_ASSUM MP_TAC
  98 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`]
  99 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))`;]
 100 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)))
 101       (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
 102 THEN POP_ASSUM MP_TAC
 103 THEN RESA_TAC
 104 THEN STRIP_TAC
 105 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)`]
 106 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)))
 107       (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)))
 108       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
 109 ==> 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)))
 110       (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)))
 111       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
 112 &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)))
 113       (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)))
 114       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
 115 THEN ASM_REWRITE_TAC[azim]
 116 THEN STRIP_TAC;
 117 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)))
 118       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 119 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))`]
 120 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))`]
 121 THEN POP_ASSUM MP_TAC
 122 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)}
 123 \/ ~(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)))})`);
 124 POP_ASSUM MP_TAC
 125 THEN RESA_TAC
 126 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 127                  IN_INSERT; NOT_IN_EMPTY]
 128 THEN ARITH_TAC;
 129 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))`]
 130 THEN REMOVE_ASSUM_TAC
 131 THEN POP_ASSUM MP_TAC
 132 THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
 133 THEN REMOVE_ASSUM_TAC
 134 THEN REMOVE_ASSUM_TAC
 135 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
 136 MP_TAC(REAL_ARITH`
 137 &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)))
 138       (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)))
 139       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
 140       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)))
 141       (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)))
 142       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
 143       pi
 144 ==> ~(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)))
 145       (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)))
 146       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
 147       &0 \/
 148       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)))
 149       (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)))
 150       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
 151       pi)`)
 152 THEN RESA_TAC
 153 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)))
 154       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 155 THEN POP_ASSUM MP_TAC
 156 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
 157 THEN STRIP_TAC
 158 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)))
 159       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 160 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 161 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)))
 162       (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`]
 163 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)))
 164       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
 165 THEN POP_ASSUM MP_TAC
 166 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
 167 THEN RESA_TAC
 168 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 169 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 170 THEN STRIP_TAC
 171 THEN MP_TAC(SET_RULE`u IN V_SY (vecmats (l:real^(M,3)finite_product))
 172 /\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
 173  aff_ge
 174  {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
 175  {z}
 176 ==> &0<= (y cross z) dot u`)
 177 THEN RESA_TAC
 178 THEN POP_ASSUM MP_TAC
 179 THEN POP_ASSUM MP_TAC
 180 THEN REAL_ARITH_TAC]);;
 181
 182
 183 let IVS_RHO_NODE_IN_EDGE = prove(`!v. local_fan (V,E,FF) /\ v IN V ==> {v,ivs_rho_node1 FF v} IN E`,
 184 NHANH EXISTS_INVERSE_OF_V THEN REPEAT STRIP_TAC
 185 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 186 THEN MRESA_TAC(GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;
 187 `FF:real^3#real^3->bool`;`vv:real^3`]
 188 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;
 189 `FF:real^3#real^3->bool`;`rho_node1 (FF:real^3#real^3->bool) vv`;`vv:real^3`]
 190 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) `)
 191 THEN RESA_TAC
 192 THEN POP_ASSUM MP_TAC
 193 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 194 THEN REWRITE_TAC[EE;IN_ELIM_THM]);;
 195
 196
 197 let RHO_IVS_IDD = prove(` local_fan (V,E,FF) /\ v IN V
 198 ==> rho_node1 FF ( ivs_rho_node1 FF v ) = v `,
 199 NHANH EXISTS_INVERSE_OF_V
 200 THEN REPEAT STRIP_TAC
 201 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 202 THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;
 203 `FF:real^3#real^3->bool`;`vv:real^3`]);;
 204
 205
 206
 207 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
 208 /\ 1<= i /\ i<= dimindex (:M)
 209 /\ 1<= j /\ j<= dimindex (:M)
 210 /\ ~(i=j)
 211 /\ row i (vecmats l)=y
 212 /\  row j (vecmats l)=z
 213 /\l IN B_SY1 a b
 214 ==> &2<= norm (y-z)  `,
 215 [REPEAT STRIP_TAC
 216 THEN ASM_TAC
 217 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
 218 THEN REPEAT STRIP_TAC
 219 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)
 220 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
 221 THEN POP_ASSUM MP_TAC
 222 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 223 THEN POP_ASSUM MP_TAC
 224 THEN POP_ASSUM MP_TAC
 225 THEN POP_ASSUM MP_TAC
 226 THEN DISCH_THEN(LABEL_TAC"THY")
 227 THEN DISCH_THEN(LABEL_TAC"THY2")
 228 THEN STRIP_TAC
 229 THEN POP_ASSUM(fun th-> MP_TAC th
 230 THEN REWRITE_TAC[convex_local_fan]
 231 THEN STRIP_TAC
 232 THEN POP_ASSUM MP_TAC
 233 THEN POP_ASSUM(fun th1-> MP_TAC th1
 234 THEN REWRITE_TAC[local_fan]
 235 THEN LET_TAC
 236 THEN STRIP_TAC
 237 THEN POP_ASSUM MP_TAC
 238 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
 239 THEN STRIP_TAC
 240 THEN ASSUME_TAC th1)
 241 THEN DISCH_THEN(LABEL_TAC"THY1")
 242 THEN ASSUME_TAC th)
 243 THEN STRIP_TAC
 244 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
 245 THEN REMOVE_THEN"THY2"(fun th-> MRESA_TAC th[`i:num`;`j:num`])
 246 THEN REMOVE_ASSUM_TAC
 247 THEN POP_ASSUM MP_TAC
 248 THEN REMOVE_THEN "THYGIANG" MP_TAC
 249 THEN REWRITE_TAC[stable_system]
 250 THEN STRIP_TAC
 251 THEN REMOVE_ASSUM_TAC
 252 THEN REMOVE_ASSUM_TAC
 253 THEN POP_ASSUM MP_TAC
 254 THEN POP_ASSUM MP_TAC
 255 THEN DISCH_THEN(LABEL_TAC"THYGIANG2")
 256 THEN MP_TAC(ARITH_RULE`i<= dimindex (:M)==> i <= dimindex (:M)-1 \/ i = dimindex (:M)`)
 257 THEN RESA_TAC;
 258
 259 MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)
 260 THEN RESA_TAC;
 261
 262 STRIP_TAC
 263 THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`j:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
 264 THEN POP_ASSUM MP_TAC
 265 THEN REAL_ARITH_TAC;
 266
 267 MP_TAC(ARITH_RULE`1<= i /\ 2< k==> ~(i = 0) /\ ~(k=0)/\ 1<k /\ 1<=k`)
 268 THEN RESA_TAC
 269 THEN STRIP_TAC
 270 THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`0:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
 271 THEN POP_ASSUM MP_TAC
 272 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
 273 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]
 274 THEN REMOVE_THEN "THYGIANG2" MP_TAC
 275 THEN REWRITE_TAC[constraint_system]
 276 THEN STRIP_TAC
 277 THEN REMOVE_ASSUM_TAC
 278 THEN REMOVE_ASSUM_TAC
 279 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`])
 280 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]
 281 THEN REAL_ARITH_TAC;
 282
 283 MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)
 284 THEN RESA_TAC;
 285
 286 MP_TAC(ARITH_RULE`2< k==> ~(k = 0)/\ 1<=k /\ 1<k`)
 287 THEN RESA_TAC
 288 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]
 289 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
 290 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]
 291 THEN REMOVE_THEN "THYGIANG2" MP_TAC
 292 THEN REWRITE_TAC[constraint_system]
 293 THEN STRIP_TAC
 294 THEN REMOVE_ASSUM_TAC
 295 THEN REMOVE_ASSUM_TAC
 296 THEN POP_ASSUM MP_TAC
 297 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])
 298 THEN STRIP_TAC
 299 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`])
 300 THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`)
 301 THEN RESA_TAC
 302 THEN STRIP_TAC
 303 THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
 304 THEN POP_ASSUM MP_TAC
 305 THEN REAL_ARITH_TAC;
 306
 307 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th])
 308 THEN SET_TAC[]]);;
 309
 310
 311 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/\
 312 {u,w} SUBSET V_SY(vecmats(l))
 313 /\ norm(u-w)<= cstab
 314 /\ &2<= norm(u-w)
 315 /\ ~({u,w} IN E_SY(vecmats l))
 316 /\ 1<= i /\ i<= dimindex (:M)
 317 /\ row i (vecmats l)=y
 318 /\  row (SUC (i MOD dimindex (:M))) (vecmats l)=z
 319 /\l IN B_SY1 a b
 320 ==> aff_gt {vec 0}{u,w} INTER aff {vec 0,y,z}={} `,
 321 [REPEAT STRIP_TAC
 322 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)
 323 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
 324 THEN POP_ASSUM MP_TAC
 325 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 326 THEN POP_ASSUM MP_TAC
 327 THEN POP_ASSUM MP_TAC
 328 THEN POP_ASSUM MP_TAC
 329 THEN DISCH_THEN(LABEL_TAC"THY")
 330 THEN STRIP_TAC
 331 THEN STRIP_TAC
 332 THEN POP_ASSUM(fun th-> MP_TAC th
 333 THEN REWRITE_TAC[convex_local_fan]
 334 THEN STRIP_TAC
 335 THEN POP_ASSUM MP_TAC
 336 THEN POP_ASSUM(fun th1-> MP_TAC th1
 337 THEN REWRITE_TAC[local_fan]
 338 THEN LET_TAC
 339 THEN STRIP_TAC
 340 THEN POP_ASSUM MP_TAC
 341 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
 342 THEN STRIP_TAC
 343 THEN ASSUME_TAC th1)
 344 THEN DISCH_THEN(LABEL_TAC"THY1")
 345 THEN ASSUME_TAC th)
 346 THEN STRIP_TAC
 347 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
 348 THEN SUBGOAL_THEN `(y,z)IN F_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
 349 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
 350 THEN EXISTS_TAC`i:num`
 351 THEN ASM_REWRITE_TAC[];
 352 MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`y:real^3`;`z:real^3`;`(l:real^(M,3)finite_product)`]
 353 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`]
 354 THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
 355 THEN SUBGOAL_THEN `u IN ball_annulus` ASSUME_TAC;
 356 MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l) ==> u IN V_SY (vecmats (l:real^(M,3)finite_product))`)
 357 THEN ASM_REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
 358 THEN STRIP_TAC
 359 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i':num`);
 360 SUBGOAL_THEN `w IN ball_annulus` ASSUME_TAC;
 361 MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l) ==> w IN V_SY (vecmats (l:real^(M,3)finite_product))`)
 362 THEN ASM_REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
 363 THEN STRIP_TAC
 364 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i':num`);
 365 MRESAL_TAC (GEN_ALL NONPARALLEL_BALL_ANNULUS)[`u:real^3`;`w:real^3`][SET_RULE`{A} UNION {B,C}={A,B,C}`]
 366 THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`w:real^3`]
 367 THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`u:real^3`;`w:real^3`]
 368 THEN REWRITE_TAC[SET_RULE`A= {}<=> ~(?x1.  x1 IN A)`;INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
 369 THEN STRIP_TAC
 370 THEN POP_ASSUM MP_TAC
 371 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`;DOT_RADD;DOT_RMUL];
 372 SUBGOAL_THEN`&0<=(y cross z) dot u/\ &0<=(y cross z) dot w` ASSUME_TAC;
 373 REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
 374 THEN POP_ASSUM MP_TAC
 375 THEN POP_ASSUM MP_TAC
 376 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)`]
 377 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))`]
 378 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)`]
 379 THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
 380 THEN RESA_TAC;
 381 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`]
 382 THEN STRIP_TAC
 383 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
 384 /\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
 385 ==> &0<= (y cross z) dot u /\ &0<= (y cross z) dot w`)
 386 THEN RESA_TAC
 387 THEN POP_ASSUM MP_TAC
 388 THEN POP_ASSUM MP_TAC
 389 THEN REAL_ARITH_TAC;
 390 POP_ASSUM MP_TAC
 391 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`]
 392 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))`;]
 393 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)))
 394       (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
 395 THEN POP_ASSUM MP_TAC
 396 THEN RESA_TAC
 397 THEN STRIP_TAC
 398 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)`]
 399 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)))
 400       (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)))
 401       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
 402 ==> 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)))
 403       (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)))
 404       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
 405 &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)))
 406       (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)))
 407       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
 408 THEN ASM_REWRITE_TAC[azim]
 409 THEN STRIP_TAC;
 410 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)))
 411       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 412 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))`]
 413 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))`]
 414 THEN POP_ASSUM MP_TAC
 415 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)}
 416 \/ ~(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)))})`);
 417 POP_ASSUM MP_TAC
 418 THEN RESA_TAC
 419 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 420                  IN_INSERT; NOT_IN_EMPTY]
 421 THEN ARITH_TAC;
 422 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))`]
 423 THEN REMOVE_ASSUM_TAC
 424 THEN POP_ASSUM MP_TAC
 425 THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
 426 THEN REMOVE_ASSUM_TAC
 427 THEN REMOVE_ASSUM_TAC
 428 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
 429 MP_TAC(REAL_ARITH`
 430 &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)))
 431       (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)))
 432       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
 433       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)))
 434       (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)))
 435       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
 436       pi
 437 ==> ~(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)))
 438       (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)))
 439       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
 440       &0 \/
 441       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)))
 442       (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)))
 443       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
 444       pi)`)
 445 THEN RESA_TAC
 446 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)))
 447       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 448 THEN POP_ASSUM MP_TAC
 449 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
 450 THEN STRIP_TAC
 451 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)))
 452       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 453 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 454 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)))
 455       (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`]
 456 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)))
 457       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
 458 THEN POP_ASSUM MP_TAC
 459 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
 460 THEN RESA_TAC
 461 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 462 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 463 THEN STRIP_TAC
 464 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
 465 /\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
 466  aff_ge
 467  {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
 468  {z}
 469 ==> &0<= (y cross z) dot u /\ &0<= (y cross z) dot w`)
 470 THEN RESA_TAC
 471 THEN POP_ASSUM MP_TAC
 472 THEN POP_ASSUM MP_TAC
 473 THEN REAL_ARITH_TAC;
 474 POP_ASSUM MP_TAC
 475 THEN STRIP_TAC
 476 THEN POP_ASSUM MP_TAC
 477 THEN POP_ASSUM MP_TAC
 478 THEN REWRITE_TAC[REAL_ARITH`&0<=A <=> &0< A \/ A= &0`]
 479 THEN RESA_TAC;
 480 REWRITE_TAC[REAL_ARITH`&0< A \/ A= &0<=> &0<=A `]
 481 THEN STRIP_TAC;
 482 MP_TAC(REAL_ARITH`&0< t3==> &0<= t3`)
 483 THEN RESA_TAC
 484 THEN MRESA_TAC REAL_LT_MUL[`t2:real`;`(y cross z) dot u`]
 485 THEN MRESA_TAC REAL_LE_MUL[`t3:real`;`(y cross z) dot w`]
 486 THEN POP_ASSUM MP_TAC
 487 THEN POP_ASSUM MP_TAC
 488 THEN REAL_ARITH_TAC;
 489 STRIP_TAC;
 490 MRESA_TAC REAL_LT_MUL[`t3:real`;`(y cross z) dot w`]
 491 THEN POP_ASSUM MP_TAC
 492 THEN REAL_ARITH_TAC;
 493 STRIP_TAC
 494 THEN REMOVE_ASSUM_TAC
 495 THEN ABBREV_TAC`y1= rho_node1 (F_SY(vecmats (l:real^(M,3)finite_product))) u`
 496 THEN ABBREV_TAC`z1= ivs_rho_node1 (F_SY(vecmats (l:real^(M,3)finite_product))) u`
 497 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
 498 ==> u IN V_SY (vecmats (l:real^(M,3)finite_product))`)
 499 THEN RESA_TAC
 500 THEN SUBGOAL_THEN`y1 IN V_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
 501 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))`;]
 502 THEN POP_ASSUM (fun th-> MRESAL1_TAC th `SUC 0`[ITER;I_DEF;o_DEF]);
 503 SUBGOAL_THEN`z1 IN V_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
 504 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))`;]
 505 THEN POP_ASSUM(fun th-> MRESA1_TAC th`u:real^3`)
 506 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))`;]
 507 THEN POP_ASSUM (fun th-> MRESAL1_TAC th `CARD (V_SY (vecmats (l:real^(M,3)finite_product))) - 1`[]);
 508 SUBGOAL_THEN`&0<= (y cross z) dot y1/\ &0<= (y cross z) dot z1`ASSUME_TAC;
 509 REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
 510 THEN POP_ASSUM MP_TAC
 511 THEN POP_ASSUM MP_TAC
 512 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)`]
 513 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))`]
 514 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)`]
 515 THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
 516 THEN RESA_TAC;
 517 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`]
 518 THEN STRIP_TAC
 519 THEN MP_TAC(SET_RULE`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))
 520 /\ z1 IN V_SY (vecmats (l:real^(M,3)finite_product))
 521 /\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
 522 ==> &0<= (y cross z) dot y1 /\ &0<= (y cross z) dot z1`)
 523 THEN RESA_TAC
 524 THEN POP_ASSUM MP_TAC
 525 THEN POP_ASSUM MP_TAC
 526 THEN REAL_ARITH_TAC;
 527 POP_ASSUM MP_TAC
 528 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`]
 529 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))`;]
 530 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)))
 531       (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
 532 THEN POP_ASSUM MP_TAC
 533 THEN RESA_TAC
 534 THEN STRIP_TAC
 535 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)`]
 536 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)))
 537       (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)))
 538       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
 539 ==> 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)))
 540       (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)))
 541       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
 542 &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)))
 543       (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)))
 544       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
 545 THEN ASM_REWRITE_TAC[azim]
 546 THEN STRIP_TAC;
 547 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)))
 548       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 549 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))`]
 550 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))`]
 551 THEN POP_ASSUM MP_TAC
 552 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)}
 553 \/ ~(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)))})`);
 554 POP_ASSUM MP_TAC
 555 THEN RESA_TAC
 556 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 557                  IN_INSERT; NOT_IN_EMPTY]
 558 THEN ARITH_TAC;
 559 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))`]
 560 THEN REMOVE_ASSUM_TAC
 561 THEN POP_ASSUM MP_TAC
 562 THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
 563 THEN REMOVE_ASSUM_TAC
 564 THEN REMOVE_ASSUM_TAC
 565 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
 566 MP_TAC(REAL_ARITH`
 567 &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)))
 568       (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)))
 569       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
 570       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)))
 571       (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)))
 572       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
 573       pi
 574 ==> ~(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)))
 575       (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)))
 576       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
 577       &0 \/
 578       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)))
 579       (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)))
 580       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
 581       pi)`)
 582 THEN RESA_TAC
 583 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)))
 584       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 585 THEN POP_ASSUM MP_TAC
 586 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
 587 THEN STRIP_TAC
 588 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)))
 589       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
 590 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 591 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)))
 592       (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`]
 593 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)))
 594       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
 595 THEN POP_ASSUM MP_TAC
 596 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
 597 THEN RESA_TAC
 598 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 599 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 600 THEN STRIP_TAC
 601 THEN MP_TAC(SET_RULE`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))
 602 /\ z1 IN V_SY (vecmats (l:real^(M,3)finite_product))
 603 /\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
 604  aff_ge
 605  {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
 606  {z}
 607 ==> &0<= (y cross z) dot y1 /\ &0<= (y cross z) dot z1 `)
 608 THEN RESA_TAC
 609 THEN POP_ASSUM MP_TAC
 610 THEN POP_ASSUM MP_TAC
 611 THEN REAL_ARITH_TAC;
 612 POP_ASSUM MP_TAC
 613 THEN POP_ASSUM MP_TAC
 614 THEN POP_ASSUM MP_TAC
 615 THEN POP_ASSUM MP_TAC
 616 THEN DISCH_THEN(LABEL_TAC"CHANGE")
 617 THEN STRIP_TAC
 618 THEN STRIP_TAC
 619 THEN DISCH_THEN(LABEL_TAC"THY4")
 620 THEN REMOVE_THEN"CHANGE" (fun th-> ASSUME_TAC th THEN
 621 MP_TAC th THEN REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
 622 THEN STRIP_TAC)
 623 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
 624 THEN SUBGOAL_THEN`u,row (SUC (i' MOD k)) (vecmats l) IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
 625 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
 626 THEN EXISTS_TAC`i':num`
 627 THEN ASM_REWRITE_TAC[];
 628 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))`;]
 629 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])
 630 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`]
 631 THEN POP_ASSUM MP_TAC
 632 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`]
 633 THEN POP_ASSUM MP_TAC
 634 THEN POP_ASSUM MP_TAC
 635 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 636 THEN RESA_TAC
 637 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 638 THEN RESA_TAC
 639 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`]
 640 THEN POP_ASSUM MP_TAC
 641 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`]
 642 THEN SUBGOAL_THEN(` &0 <= (z1 cross u) dot w /\ &0 <= (z1 cross u) dot y /\ &0 <= (z1 cross u) dot z  `)ASSUME_TAC;
 643 MP_TAC(ARITH_RULE`1<=i'==> i'=1 \/ 1<= i'-1`)
 644 THEN RESA_TAC;
 645 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 646 THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 647 THEN MP_TAC(ARITH_RULE`2<k==> 1<= k/\ k<=k`)
 648 THEN RESA_TAC
 649 THEN SUBGOAL_THEN`row k (vecmats l), u IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
 650 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
 651 THEN EXISTS_TAC`k:num`
 652 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
 653 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))`;]
 654 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`row k (vecmats (l:real^(M,3)finite_product)):real^3,u:real^3`[PAIR_EQ])
 655 THEN FIND_ASSUM MP_TAC`ivs_rho_node1 (F_SY (vecmats (l:real^(M,3)finite_product))) u=z1`
 656 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
 657 THEN SUBGOAL_THEN`row k (vecmats l) IN V_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
 658 REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 659 THEN EXISTS_TAC`k:num`
 660 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
 661 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)))`]
 662 THEN STRIP_TAC
 663 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)`]
 664 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)`]
 665 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
 666 ==> w IN V_SY (vecmats l) `)
 667 THEN RESA_TAC
 668 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)`];
 669 MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==> i'-1 < dimindex (:M)/\ i'-1 <= dimindex (:M)`)
 670 THEN RESA_TAC
 671 THEN MRESAL_TAC MOD_LT[`i'-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
 672 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
 673 ==> w IN V_SY (vecmats l) `)
 674 THEN RESA_TAC
 675 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)`]
 676 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)`]
 677 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)`]
 678 THEN POP_ASSUM MP_TAC
 679 THEN POP_ASSUM MP_TAC
 680 THEN POP_ASSUM MP_TAC
 681 THEN MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==>  SUC (i'-1)=i'`)
 682 THEN RESA_TAC
 683 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 684 THEN SUBGOAL_THEN`row (i'-1) (vecmats l), u IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
 685 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
 686 THEN EXISTS_TAC`i'-1:num`
 687 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`]
 688 THEN MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==>  SUC (i'-1)=i'`)
 689 THEN RESA_TAC
 690 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]);
 691 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))`;]
 692 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])
 693 THEN FIND_ASSUM MP_TAC`ivs_rho_node1 (F_SY (vecmats (l:real^(M,3)finite_product))) u=z1`
 694 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
 695 THEN SUBGOAL_THEN`row (i'-1) (vecmats l) IN V_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
 696 REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 697 THEN EXISTS_TAC`i'-1:num`
 698 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
 699 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)))`]
 700 THEN RESA_TAC
 701 THEN REAL_ARITH_TAC;
 702 POP_ASSUM MP_TAC
 703 THEN STRIP_TAC
 704 THEN POP_ASSUM MP_TAC
 705 THEN POP_ASSUM MP_TAC
 706 THEN SUBGOAL_THEN`u IN aff{vec 0, y,z:real^3}` ASSUME_TAC;
 707 ASM_REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`;IN_ELIM_THM];
 708 POP_ASSUM MP_TAC
 709 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
 710 THEN STRIP_TAC
 711 THEN POP_ASSUM (fun th-> REWRITE_TAC[th] THEN ASSUME_TAC (SYM th))
 712 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;]
 713 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 714 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 715 THEN MP_TAC(REAL_ARITH`&0 <= (y cross z) dot y1 ==> ~((y cross z) dot y1< &0)`)
 716 THEN RESA_TAC
 717 THEN SUBGOAL_THEN`(y cross z1) dot z<= &0` ASSUME_TAC;
 718 ONCE_REWRITE_TAC[CROSS_TRIPLE]
 719 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 720 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 721 THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- A<= &0<=> &0<= A`];
 722 MP_TAC(REAL_ARITH` (y cross z1) dot z<= &0 ==> ~(&0< (y cross z1) dot z)`)
 723 THEN RESA_TAC
 724 THEN REPEAT STRIP_TAC
 725 THEN SUBGOAL_THEN`(y cross z1) dot z= &0 \/ (y cross z) dot y1= &0` ASSUME_TAC;
 726 POP_ASSUM MP_TAC
 727 THEN POP_ASSUM MP_TAC
 728 THEN POP_ASSUM MP_TAC
 729 THEN POP_ASSUM MP_TAC
 730 THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
 731 THEN SUBGOAL_THEN`~(w' = &0 /\ v'= &0)` ASSUME_TAC;
 732 STRIP_TAC
 733 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 734 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 735 THEN ASM_TAC
 736 THEN REWRITE_TAC[VECTOR_ARITH`&0 % A= vec 0/\ vec 0+ vec 0= vec 0`]
 737 THEN REPEAT STRIP_TAC
 738 THEN REMOVE_ASSUM_TAC
 739 THEN REMOVE_ASSUM_TAC
 740 THEN POP_ASSUM MP_TAC
 741 THEN ASM_REWRITE_TAC[];
 742 POP_ASSUM MP_TAC
 743 THEN ASM_REWRITE_TAC[SET_RULE`~(A /\ B)<=> ~A \/ ~B`]
 744 THEN RESA_TAC;
 745 RESA_TAC;
 746 MP_TAC(REAL_ARITH`w'< &0==> ~(&0 < w')`)
 747 THEN RESA_TAC
 748 THEN SET_TAC[];
 749 DISCH_TAC
 750 THEN REMOVE_ASSUM_TAC
 751 THEN RESA_TAC;
 752 POP_ASSUM MP_TAC
 753 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 754 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 755 THEN STRIP_TAC
 756 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 757 THEN ASM_REWRITE_TAC[DOT_LNEG;]
 758 THEN REAL_ARITH_TAC;
 759 MP_TAC(REAL_ARITH`v'< &0==> ~(&0 < v')`)
 760 THEN RESA_TAC
 761 THEN STRIP_TAC;
 762 ONCE_REWRITE_TAC[CROSS_SKEW]
 763 THEN ASM_REWRITE_TAC[DOT_LNEG;]
 764 THEN REAL_ARITH_TAC;
 765 POP_ASSUM MP_TAC
 766 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 767 THEN ASM_REWRITE_TAC[DOT_LNEG; REAL_ARITH`&0< -- A<=> ~(&0 <= A)`];
 768 POP_ASSUM MP_TAC
 769 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 770 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 771 THEN ASM_REWRITE_TAC[DOT_LNEG; REAL_ARITH` A< &0 <=> ~(&0 <= A)`];
 772 POP_ASSUM MP_TAC
 773 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
 774 ==> w IN V_SY (vecmats l) `)
 775 THEN RESA_TAC
 776 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`]
 777 THEN SUBGOAL_THEN`w IN aff{vec 0, y,z:real^3}` ASSUME_TAC;
 778 ASM_REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`;IN_ELIM_THM];
 779 STRIP_TAC;
 780 POP_ASSUM MP_TAC
 781 THEN POP_ASSUM MP_TAC
 782 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
 783 THEN STRIP_TAC
 784 THEN STRIP_TAC
 785 THEN SUBGOAL_THEN`z1 IN aff{vec 0,u,w:real^3}` ASSUME_TAC;
 786 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`w:real^3`]
 787 THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
 788 THEN EXPAND_TAC"u"
 789 THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;DOT_LADD;DOT_LMUL;CROSS_RADD;CROSS_RMUL;DOT_CROSS_SELF;CROSS_REFL;DOT_LZERO]
 790 THEN ASM_REWRITE_TAC[]
 791 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 792 THEN ASM_REWRITE_TAC[]
 793 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 794 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 795 THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
 796 THEN REAL_ARITH_TAC;
 797 POP_ASSUM MP_TAC
 798 THEN POP_ASSUM MP_TAC
 799 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
 800 THEN STRIP_TAC
 801 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
 802 THEN STRIP_TAC
 803 THEN FIND_ASSUM MP_TAC `&0 <= (u cross y1) dot z1`
 804 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))
 805 THEN MP_TAC(REAL_ARITH`&0 <= (u cross y1) dot w==> (u cross y1) dot w = &0 \/ &0 < (u cross y1) dot w`)
 806 THEN RESA_TAC;
 807 SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
 808 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
 809 THEN EXISTS_TAC`i':num`
 810 THEN ASM_REWRITE_TAC[];
 811 POP_ASSUM MP_TAC
 812 THEN RESA_TAC
 813 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`]
 814 THEN SUBGOAL_THEN`w IN aff{vec 0,u,y1:real^3}` ASSUME_TAC;
 815 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`y1:real^3`]
 816 THEN ASM_REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`];
 817 POP_ASSUM MP_TAC
 818 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
 819 THEN STRIP_TAC
 820 THEN POP_ASSUM (fun th-> ASSUME_TAC (SYM th))
 821 THEN DISJ_CASES_TAC(REAL_ARITH`w''''< &0 \/ &0<= w''''`);
 822 SUBGOAL_THEN`w IN aff_lt{vec 0,u} {y1:real^3}` ASSUME_TAC;
 823 ASM_SIMP_TAC[AFF_LT_2_1;IN_ELIM_THM]
 824 THEN EXISTS_TAC`u'''':real`
 825 THEN EXISTS_TAC`v'''':real`
 826 THEN EXISTS_TAC`w'''':real`
 827 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`];
 828 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`]
 829 THEN MRESA_TAC AZIM_EQ_PI_ALT[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`]
 830 THEN SUBGOAL_THEN`coplanar{vec 0, u, y1, z1:real^3} `ASSUME_TAC;
 831 ASM_SIMP_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT;VECTOR_ARITH`A- vec 0=A`]
 832 THEN EXPAND_TAC"z1"
 833 THEN REWRITE_TAC[DOT_RADD;DOT_RMUL]
 834 THEN ASM_REWRITE_TAC[DOT_CROSS_SELF]
 835 THEN REAL_ARITH_TAC;
 836 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`]
 837 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`z1:real^3`];
 838 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`]
 839 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))`]
 840 THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real^3`)
 841 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`];
 842 POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
 843 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`z1:real^3`;`w:real^3`]
 844 THEN MP_TAC(SET_RULE`w IN aff_gt {vec 0, u} {z1}
 845 /\  aff_gt {vec 0, u} {z1} SUBSET aff_ge {vec 0, u} {z1}
 846 ==> w IN aff_ge {vec 0, u} {z1:real^3}`)
 847 THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
 848 THEN STRIP_TAC
 849 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
 850 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
 851 THEN POP_ASSUM MP_TAC
 852 THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
 853 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
 854 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 855 THEN STRIP_TAC
 856 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
 857 SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
 858 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
 859 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 860 THEN STRIP_TAC
 861 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
 862 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 863 THEN POP_ASSUM MP_TAC
 864 THEN RESA_TAC
 865 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`];
 866 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`];
 867 SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
 868 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
 869 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 870 THEN STRIP_TAC
 871 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
 872 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 873 THEN STRIP_TAC
 874 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
 875 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 876 THEN POP_ASSUM MP_TAC
 877 THEN RESA_TAC
 878 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
 879 THEN REMOVE_ASSUM_TAC
 880 THEN REMOVE_ASSUM_TAC
 881 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 882 THEN STRIP_TAC
 883 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 884 THEN ASM_TAC
 885 THEN SET_TAC[];
 886 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`];
 887 ASM_REWRITE_TAC[]
 888 THEN STRIP_TAC
 889 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
 890 THEN POP_ASSUM MP_TAC
 891 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 892 THEN ASM_REWRITE_TAC[]
 893 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
 894 THEN ASM_REWRITE_TAC[];
 895 DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
 896 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 897 THEN ASM_TAC
 898 THEN SET_TAC[];
 899 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
 900 THEN POP_ASSUM MP_TAC
 901 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
 902 THEN RESA_TAC
 903 THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
 904 THEN RESA_TAC
 905 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
 906 EXISTS_TAC`w:real^3`
 907 THEN ASM_REWRITE_TAC[];
 908 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
 909 THEN REWRITE_TAC[FAN;fan7]
 910 THEN STRIP_TAC
 911 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])
 912 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
 913 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
 914 /\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
 915 /\ w IN aff_ge {vec 0} {u, z1}
 916 ==> vec 0= w:real^3`)
 917 THEN RESA_TAC;
 918 SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {y1}` ASSUME_TAC;
 919 ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
 920 THEN EXISTS_TAC`u'''':real`
 921 THEN EXISTS_TAC`v'''':real`
 922 THEN EXISTS_TAC`w'''':real`
 923 THEN ASM_REWRITE_TAC[]
 924 THEN VECTOR_ARITH_TAC;
 925 MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
 926 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
 927 THEN POP_ASSUM MP_TAC
 928 THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
 929 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
 930 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 931 THEN STRIP_TAC
 932 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
 933 SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
 934 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
 935 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 936 THEN STRIP_TAC
 937 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
 938 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 939 THEN POP_ASSUM MP_TAC
 940 THEN RESA_TAC
 941 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`];
 942 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`];
 943 SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
 944 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
 945 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 946 THEN STRIP_TAC
 947 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
 948 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
 949 THEN STRIP_TAC
 950 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
 951 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 952 THEN POP_ASSUM MP_TAC
 953 THEN RESA_TAC
 954 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
 955 THEN REMOVE_ASSUM_TAC
 956 THEN REMOVE_ASSUM_TAC
 957 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 958 THEN STRIP_TAC
 959 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 960 THEN ASM_TAC
 961 THEN SET_TAC[];
 962 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`];
 963 ASM_REWRITE_TAC[]
 964 THEN STRIP_TAC
 965 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
 966 THEN POP_ASSUM MP_TAC
 967 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 968 THEN ASM_REWRITE_TAC[]
 969 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
 970 THEN ASM_REWRITE_TAC[];
 971 DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
 972 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 973 THEN ASM_TAC
 974 THEN SET_TAC[];
 975 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
 976 THEN POP_ASSUM MP_TAC
 977 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
 978 THEN RESA_TAC
 979 THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
 980 THEN RESA_TAC
 981 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
 982 EXISTS_TAC`w:real^3`
 983 THEN ASM_REWRITE_TAC[];
 984 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
 985 THEN REWRITE_TAC[FAN;fan7]
 986 THEN STRIP_TAC
 987 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])
 988 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
 989 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
 990 /\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
 991 /\ w IN aff_ge {vec 0} {u, y1}
 992 ==> vec 0= w:real^3`)
 993 THEN RESA_TAC;
 994 MP_TAC(REAL_ARITH`&0 < (u cross y1:real^3) dot w ==> ~((u cross y1) dot w = &0) /\ ~((u cross y1) dot w < &0)`)
 995 THEN RESA_TAC
 996 THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
 997 THEN STRIP_TAC;
 998 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 999 THEN ASM_TAC
1000 THEN REWRITE_TAC[VECTOR_ARITH`&0 %A= vec 0/\ A + vec 0=A`]
1001 THEN REPEAT STRIP_TAC
1002 THEN SUBGOAL_THEN`z1 IN aff{vec 0, u:real^3}`ASSUME_TAC;
1003 REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
1004 THEN EXISTS_TAC`&1- v''':real`
1005 THEN EXISTS_TAC`v''':real`
1006 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - v''' + v''' = &1`]
1007 THEN VECTOR_ARITH_TAC;
1008 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`]
1009 THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`z1:real^3`];
1010 POP_ASSUM MP_TAC
1011 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`]
1012 THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`z1:real^3`]
1013 THEN STRIP_TAC
1014 THEN SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {z1}` ASSUME_TAC;
1015 ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
1016 THEN EXISTS_TAC`&1 + (inv w''') *v''' - inv w''':real`
1017 THEN EXISTS_TAC`-- (inv w''') *v''':real`
1018 THEN EXISTS_TAC`inv w''':real`
1019 THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 + inv w''' * v''' - inv w''') + --inv w''' * v''' + inv w''' = &1`]
1020 THEN EXPAND_TAC"z1"
1021 THEN REWRITE_TAC[VECTOR_ARITH`(&1 + inv w''' * v''' - inv w''') % vec 0 +
1022  (--inv w''' * v''') % u +
1023  inv w''' % (v''' % u + w''' % w)
1024 = (inv w''' *w''') % w`]
1025 THEN MP_TAC(REAL_ARITH`&0< w'''==> ~(w'''= &0)`)
1026 THEN RESA_TAC
1027 THEN MRESAL1_TAC REAL_MUL_LINV`w''':real`[VECTOR_ARITH`A= &1 %A`]
1028 THEN MATCH_MP_TAC REAL_LE_INV
1029 THEN REMOVE_ASSUM_TAC
1030 THEN REMOVE_ASSUM_TAC
1031 THEN POP_ASSUM MP_TAC
1032 THEN REAL_ARITH_TAC;
1033 POP_ASSUM MP_TAC
1034 THEN POP_ASSUM MP_TAC
1035 THEN DISCH_THEN(LABEL_TAC"A")
1036 THEN STRIP_TAC
1037 THEN REMOVE_THEN"A" MP_TAC
1038 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
1039 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
1040 THEN POP_ASSUM MP_TAC
1041 THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
1042 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1043 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1044 THEN STRIP_TAC
1045 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
1046 SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
1047 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1048 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1049 THEN STRIP_TAC
1050 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
1051 POP_ASSUM MP_TAC
1052 THEN POP_ASSUM MP_TAC
1053 THEN MRESA_TAC th3[`u:real^3`;`z1:real^3`;`vec 0:real^3`]
1054 THEN POP_ASSUM MP_TAC
1055 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1056 THEN RESA_TAC
1057 THEN STRIP_TAC
1058 THEN STRIP_TAC
1059 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1060 THEN POP_ASSUM MP_TAC
1061 THEN RESA_TAC;
1062 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`];
1063 SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
1064 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1065 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1066 THEN STRIP_TAC
1067 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
1068 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1069 THEN STRIP_TAC
1070 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`]
1071 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
1072 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1073 THEN POP_ASSUM MP_TAC
1074 THEN RESA_TAC
1075 THEN POP_ASSUM MP_TAC
1076 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1077 THEN ASM_REWRITE_TAC[];
1078 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`];
1079 ASM_REWRITE_TAC[]
1080 THEN STRIP_TAC
1081 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
1082 THEN POP_ASSUM MP_TAC
1083 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1084 THEN ASM_REWRITE_TAC[]
1085 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1086 THEN ASM_REWRITE_TAC[];
1087 DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
1088 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`];
1089 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
1090 THEN POP_ASSUM MP_TAC
1091 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1092 THEN RESA_TAC
1093 THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
1094 THEN RESA_TAC
1095 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
1096 EXISTS_TAC`w:real^3`
1097 THEN ASM_REWRITE_TAC[];
1098 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`]
1099 THEN FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
1100 THEN REWRITE_TAC[FAN;fan7]
1101 THEN STRIP_TAC
1102 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])
1103 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
1104 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
1105 /\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
1106 /\ w IN aff_ge {vec 0} {u, z1}
1107 ==> vec 0= w:real^3`)
1108 THEN RESA_TAC;
1109 POP_ASSUM MP_TAC
1110 THEN POP_ASSUM MP_TAC
1111 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
1112 THEN STRIP_TAC
1113 THEN STRIP_TAC
1114 THEN SUBGOAL_THEN`y1 IN aff{vec 0,u,w:real^3}` ASSUME_TAC;
1115 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`w:real^3`]
1116 THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
1117 THEN EXPAND_TAC"u"
1118 THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;DOT_LADD;DOT_LMUL;CROSS_RADD;CROSS_RMUL;DOT_CROSS_SELF;CROSS_REFL;DOT_LZERO]
1119 THEN ASM_REWRITE_TAC[]
1120 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
1121 THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
1122 THEN REAL_ARITH_TAC;
1123 POP_ASSUM MP_TAC
1124 THEN POP_ASSUM MP_TAC
1125 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
1126 THEN STRIP_TAC
1127 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
1128 THEN STRIP_TAC
1129 THEN FIND_ASSUM MP_TAC `&0 <= (u cross y1) dot z1`
1130 THEN POP_ASSUM(fun th-> REWRITE_TAC[th;CROSS_RADD;CROSS_RMUL;DOT_LADD;DOT_LMUL;DOT_CROSS_SELF;] THEN ASSUME_TAC (SYM th))
1131 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1132 THEN REWRITE_TAC[DOT_CROSS_SELF;REAL_ARITH`A * &0+B=B`]
1133 THEN MP_TAC(REAL_ARITH`&0 <= (z1 cross u) dot w==> (z1 cross u) dot w = &0 \/ &0 < (z1 cross u) dot w`)
1134 THEN RESA_TAC;
1135 SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1136 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1137 THEN EXISTS_TAC`i':num`
1138 THEN ASM_REWRITE_TAC[];
1139 POP_ASSUM MP_TAC
1140 THEN RESA_TAC
1141 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`]
1142 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`]
1143 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`]
1144 THEN SUBGOAL_THEN`w IN aff{vec 0,u,z1:real^3}` ASSUME_TAC;
1145 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`z1:real^3`]
1146 THEN ASM_REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
1147 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
1148 THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
1149 THEN REAL_ARITH_TAC;
1150 POP_ASSUM MP_TAC
1151 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
1152 THEN STRIP_TAC
1153 THEN POP_ASSUM (fun th-> ASSUME_TAC (SYM th))
1154 THEN DISJ_CASES_TAC(REAL_ARITH`w''''< &0 \/ &0<= w''''`);
1155 SUBGOAL_THEN`w IN aff_lt{vec 0,u} {z1:real^3}` ASSUME_TAC;
1156 ASM_SIMP_TAC[AFF_LT_2_1;IN_ELIM_THM]
1157 THEN EXISTS_TAC`u'''':real`
1158 THEN EXISTS_TAC`v'''':real`
1159 THEN EXISTS_TAC`w'''':real`
1160 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`];
1161 MRESA_TAC AZIM_EQ_PI_ALT[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`]
1162 THEN SUBGOAL_THEN`coplanar{vec 0, u, z1, y1:real^3} `ASSUME_TAC;
1163 ASM_SIMP_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT;VECTOR_ARITH`A- vec 0=A`]
1164 THEN EXPAND_TAC"y1"
1165 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_LADD;CROSS_LADD;DOT_RADD;DOT_RMUL;CROSS_REFL]
1166 THEN ASM_REWRITE_TAC[DOT_CROSS_SELF;]
1167 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
1168 THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
1169 THEN REAL_ARITH_TAC;
1170 MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`y1:real^3`];
1171 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`]
1172 THEN POP_ASSUM MP_TAC
1173 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))`]
1174 THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real^3`)
1175 THEN STRIP_TAC
1176 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1177 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`];
1178 POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1179 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`y1:real^3`;`w:real^3`]
1180 THEN MP_TAC(SET_RULE`w IN aff_gt {vec 0, u} {y1}
1181 /\  aff_gt {vec 0, u} {y1} SUBSET aff_ge {vec 0, u} {y1}
1182 ==> w IN aff_ge {vec 0, u} {y1:real^3}`)
1183 THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
1184 THEN STRIP_TAC
1185 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
1186 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
1187 THEN POP_ASSUM MP_TAC
1188 THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
1189 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1190 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1191 THEN STRIP_TAC
1192 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
1193 SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
1194 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1195 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1196 THEN STRIP_TAC
1197 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
1198 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1199 THEN POP_ASSUM MP_TAC
1200 THEN RESA_TAC
1201 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`];
1202 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`];
1203 SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
1204 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1205 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1206 THEN STRIP_TAC
1207 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
1208 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1209 THEN STRIP_TAC
1210 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
1211 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1212 THEN POP_ASSUM MP_TAC
1213 THEN RESA_TAC
1214 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
1215 THEN REMOVE_ASSUM_TAC
1216 THEN REMOVE_ASSUM_TAC
1217 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1218 THEN STRIP_TAC
1219 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1220 THEN ASM_TAC
1221 THEN SET_TAC[];
1222 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`];
1223 ASM_REWRITE_TAC[]
1224 THEN STRIP_TAC
1225 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
1226 THEN POP_ASSUM MP_TAC
1227 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1228 THEN ASM_REWRITE_TAC[]
1229 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1230 THEN ASM_REWRITE_TAC[]
1231 THEN STRIP_TAC
1232 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1233 THEN ASM_REWRITE_TAC[];
1234 DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
1235 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1236 THEN ASM_TAC
1237 THEN SET_TAC[];
1238 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
1239 THEN POP_ASSUM MP_TAC
1240 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1241 THEN RESA_TAC
1242 THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
1243 THEN RESA_TAC
1244 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
1245 EXISTS_TAC`w:real^3`
1246 THEN ASM_REWRITE_TAC[];
1247 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
1248 THEN REWRITE_TAC[FAN;fan7]
1249 THEN STRIP_TAC
1250 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])
1251 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
1252 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
1253 /\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
1254 /\ w IN aff_ge {vec 0} {u, y1}
1255 ==> vec 0= w:real^3`)
1256 THEN RESA_TAC;
1257 SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {z1}` ASSUME_TAC;
1258 ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
1259 THEN EXISTS_TAC`u'''':real`
1260 THEN EXISTS_TAC`v'''':real`
1261 THEN EXISTS_TAC`w'''':real`
1262 THEN ASM_REWRITE_TAC[]
1263 THEN VECTOR_ARITH_TAC;
1264 MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
1265 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
1266 THEN POP_ASSUM MP_TAC
1267 THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
1268 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1269 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1270 THEN STRIP_TAC
1271 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
1272 SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
1273 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1274 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1275 THEN STRIP_TAC
1276 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
1277 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1278 THEN POP_ASSUM MP_TAC
1279 THEN RESA_TAC
1280 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`];
1281 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`];
1282 SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
1283 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1284 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1285 THEN STRIP_TAC
1286 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
1287 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1288 THEN STRIP_TAC
1289 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
1290 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1291 THEN POP_ASSUM MP_TAC
1292 THEN RESA_TAC
1293 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
1294 THEN REMOVE_ASSUM_TAC
1295 THEN REMOVE_ASSUM_TAC
1296 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1297 THEN STRIP_TAC
1298 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1299 THEN ASM_TAC
1300 THEN SET_TAC[];
1301 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`];
1302 ASM_REWRITE_TAC[]
1303 THEN STRIP_TAC
1304 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
1305 THEN POP_ASSUM MP_TAC
1306 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1307 THEN ASM_REWRITE_TAC[]
1308 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1309 THEN ASM_REWRITE_TAC[];
1310 DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
1311 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1312 THEN ASM_TAC
1313 THEN SET_TAC[];
1314 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
1315 THEN POP_ASSUM MP_TAC
1316 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1317 THEN RESA_TAC
1318 THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
1319 THEN RESA_TAC
1320 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
1321 EXISTS_TAC`w:real^3`
1322 THEN ASM_REWRITE_TAC[];
1323 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
1324 THEN REWRITE_TAC[FAN;fan7]
1325 THEN STRIP_TAC
1326 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])
1327 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
1328 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
1329 /\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
1330 /\ w IN aff_ge {vec 0} {u, z1}
1331 ==> vec 0= w:real^3`)
1332 THEN RESA_TAC;
1333 ONCE_REWRITE_TAC[CROSS_TRIPLE]
1334 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)`)
1335 THEN RESA_TAC
1336 THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
1337 THEN STRIP_TAC;
1338 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1339 THEN ASM_TAC
1340 THEN REWRITE_TAC[VECTOR_ARITH`&0 %A= vec 0/\ A + vec 0=A`]
1341 THEN REPEAT STRIP_TAC
1342 THEN SUBGOAL_THEN`y1 IN aff{vec 0, u:real^3}`ASSUME_TAC;
1343 REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
1344 THEN EXISTS_TAC`&1- v''':real`
1345 THEN EXISTS_TAC`v''':real`
1346 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - v''' + v''' = &1`]
1347 THEN VECTOR_ARITH_TAC;
1348 SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1349 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1350 THEN EXISTS_TAC`i':num`
1351 THEN ASM_REWRITE_TAC[];
1352 POP_ASSUM MP_TAC
1353 THEN RESA_TAC
1354 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`];
1355 SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1356 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1357 THEN EXISTS_TAC`i':num`
1358 THEN ASM_REWRITE_TAC[];
1359 POP_ASSUM MP_TAC
1360 THEN RESA_TAC
1361 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`]
1362 THEN SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {y1}` ASSUME_TAC;
1363 ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
1364 THEN EXISTS_TAC`&1 + (inv w''') *v''' - inv w''':real`
1365 THEN EXISTS_TAC`-- (inv w''') *v''':real`
1366 THEN EXISTS_TAC`inv w''':real`
1367 THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 + inv w''' * v''' - inv w''') + --inv w''' * v''' + inv w''' = &1`]
1368 THEN EXPAND_TAC"y1"
1369 THEN REWRITE_TAC[VECTOR_ARITH`(&1 + inv w''' * v''' - inv w''') % vec 0 +
1370  (--inv w''' * v''') % u +
1371  inv w''' % (v''' % u + w''' % w)
1372 = (inv w''' *w''') % w`]
1373 THEN MP_TAC(REAL_ARITH`&0< w'''==> ~(w'''= &0)`)
1374 THEN RESA_TAC
1375 THEN MRESAL1_TAC REAL_MUL_LINV`w''':real`[VECTOR_ARITH`A= &1 %A`]
1376 THEN MATCH_MP_TAC REAL_LE_INV
1377 THEN ASM_TAC
1378 THEN REAL_ARITH_TAC;
1379 REMOVE_THEN "THY4" MP_TAC
1380 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
1381 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
1382 THEN POP_ASSUM MP_TAC
1383 THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
1384 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1385 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1386 THEN STRIP_TAC
1387 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
1388 SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
1389 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1390 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1391 THEN STRIP_TAC
1392 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
1393 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1394 THEN POP_ASSUM MP_TAC
1395 THEN RESA_TAC
1396 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`];
1397 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`];
1398 SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
1399 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1400 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1401 THEN STRIP_TAC
1402 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
1403 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1404 THEN STRIP_TAC
1405 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
1406 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1407 THEN POP_ASSUM MP_TAC
1408 THEN RESA_TAC
1409 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
1410 THEN REMOVE_ASSUM_TAC
1411 THEN REMOVE_ASSUM_TAC
1412 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1413 THEN STRIP_TAC
1414 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1415 THEN ASM_TAC
1416 THEN SET_TAC[];
1417 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`];
1418 ASM_REWRITE_TAC[]
1419 THEN STRIP_TAC
1420 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
1421 THEN POP_ASSUM MP_TAC
1422 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1423 THEN ASM_REWRITE_TAC[]
1424 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1425 THEN ASM_REWRITE_TAC[]
1426 THEN STRIP_TAC
1427 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1428 THEN ASM_REWRITE_TAC[];
1429 DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
1430 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1431 THEN ASM_TAC
1432 THEN SET_TAC[];
1433 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
1434 THEN POP_ASSUM MP_TAC
1435 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1436 THEN RESA_TAC
1437 THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
1438 THEN RESA_TAC
1439 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
1440 EXISTS_TAC`w:real^3`
1441 THEN ASM_REWRITE_TAC[];
1442 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
1443 THEN REWRITE_TAC[FAN;fan7]
1444 THEN STRIP_TAC
1445 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])
1446 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
1447 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
1448 /\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
1449 /\ w IN aff_ge {vec 0} {u, y1}
1450 ==> vec 0= w:real^3`)
1451 THEN RESA_TAC]);;
1452
1453
1454
1455
1456 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/\
1457 {u,w} SUBSET V_SY(vecmats(l))
1458 /\ norm(u-w)<= cstab
1459 /\ &2<= norm(u-w)
1460 /\ ~({u,w} IN E_SY(vecmats l))
1461 /\l IN B_SY1 a b
1462 ==> (!x. x IN F_SY(vecmats l)==> aff_gt {vec 0}{u,w} SUBSET wedge_in_fan_gt x (E_SY (vecmats l))) `,
1463 [GEN_TAC THEN STRIP_TAC
1464 THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY]
1465 THEN REPEAT STRIP_TAC)
1466 THEN POP_ASSUM MP_TAC
1467 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
1468 THEN POP_ASSUM MP_TAC
1469 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1470 THEN POP_ASSUM(fun th-> MP_TAC th
1471 THEN REWRITE_TAC[convex_local_fan]
1472 THEN STRIP_TAC
1473 THEN POP_ASSUM MP_TAC
1474 THEN POP_ASSUM (fun th2-> ASSUME_TAC th2 THEN MP_TAC th2
1475 THEN REWRITE_TAC[local_fan]
1476 THEN LET_TAC
1477 THEN STRIP_TAC
1478 THEN POP_ASSUM MP_TAC
1479 THEN POP_ASSUM(fun th3-> ASSUME_TAC(SYM th3))
1480 THEN STRIP_TAC)
1481 THEN DISCH_THEN(LABEL_TAC"YEU")
1482 THEN ASSUME_TAC th)
1483 THEN STRIP_TAC
1484 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1485 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))`)
1486 THEN RESA_TAC
1487 THEN STRIP_TAC
1488 THEN POP_ASSUM(fun th-> MP_TAC th
1489 THEN REWRITE_TAC[F_SY;IN_ELIM_THM;]
1490 THEN STRIP_TAC
1491 THEN ASSUME_TAC th)
1492 THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))`
1493 THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
1494 THEN SUBGOAL_THEN `y IN V_SY (vecmats (l:real^(M,3)finite_product))`ASSUME_TAC;
1495 REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1496 THEN EXISTS_TAC`i:num`
1497 THEN ASM_REWRITE_TAC[];
1498 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))`;]
1499 THEN ASM_REWRITE_TAC[wedge_in_fan_gt;ARITH_RULE`2>1`]
1500 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)`]
1501 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))`]
1502 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0:real^3}`;`{u,w:real^3}`]
1503 THEN MP_TAC(SET_RULE`aff_gt {vec 0} {u, w} SUBSET aff_ge {vec 0} {u, w}
1504 /\ 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)
1505 ==> 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)`)
1506 THEN RESA_TAC
1507 THEN POP_ASSUM MP_TAC
1508 THEN REMOVE_THEN "YEU"(fun th-> MRESA1_TAC th`x:real^3#real^3`)
1509 THEN REMOVE_ASSUM_TAC
1510 THEN POP_ASSUM MP_TAC
1511 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)`]
1512 THEN ABBREV_TAC`y1=azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z`
1513 THEN REWRITE_TAC[REAL_ARITH`a<= b<=> a=b\/ a< b`]
1514 THEN STRIP_TAC;
1515 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`]
1516 THEN SUBGOAL_THEN`{y,row (SUC (i MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1517 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1518 THEN EXISTS_TAC`i:num`
1519 THEN ASM_REWRITE_TAC[];
1520 POP_ASSUM MP_TAC
1521 THEN RESA_TAC
1522 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`]
1523 THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
1524 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`]
1525 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
1526 THEN DISCH_THEN(LABEL_TAC"THY4")
1527 THEN REPEAT STRIP_TAC
1528 THEN REMOVE_THEN"THY4"(fun th-> MRESA1_TAC th`x'':real^3`)
1529 THEN SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y, z:real^3}` ASSUME_TAC;
1530 ASM_REWRITE_TAC[INTER;IN_ELIM_THM];
1531 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]
1532 THEN POP_ASSUM MP_TAC
1533 THEN POP_ASSUM MP_TAC
1534 THEN ASM_REWRITE_TAC[]
1535 THEN SET_TAC[];
1536 POP_ASSUM MP_TAC
1537 THEN SUBGOAL_THEN`{y,row (SUC (i MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1538 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1539 THEN EXISTS_TAC`i:num`
1540 THEN ASM_REWRITE_TAC[];
1541 POP_ASSUM MP_TAC
1542 THEN RESA_TAC
1543 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`]
1544 THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
1545 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`]
1546 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))`;]
1547 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)))
1548       (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
1549 THEN POP_ASSUM MP_TAC
1550 THEN RESA_TAC
1551 THEN STRIP_TAC
1552 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)`]
1553 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)))
1554       (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)))
1555       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
1556 ==> 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)))
1557       (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)))
1558       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
1559 &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)))
1560       (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)))
1561       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
1562 THEN ASM_REWRITE_TAC[azim]
1563 THEN STRIP_TAC;
1564 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)))
1565       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
1566 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))`]
1567 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))`]
1568 THEN POP_ASSUM MP_TAC
1569 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)}
1570 \/ ~(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)))})`);
1571 POP_ASSUM MP_TAC
1572 THEN RESA_TAC
1573 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
1574                  IN_INSERT; NOT_IN_EMPTY]
1575 THEN ARITH_TAC;
1576 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))`]
1577 THEN REMOVE_ASSUM_TAC
1578 THEN POP_ASSUM MP_TAC
1579 THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
1580 THEN REMOVE_ASSUM_TAC
1581 THEN REMOVE_ASSUM_TAC
1582 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
1583 MP_TAC(REAL_ARITH`
1584 &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)))
1585       (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)))
1586       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
1587       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)))
1588       (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)))
1589       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
1590       pi
1591 ==> ~(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)))
1592       (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)))
1593       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
1594       &0 \/
1595       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)))
1596       (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)))
1597       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
1598       pi)`)
1599 THEN RESA_TAC
1600 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)))
1601       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
1602 THEN POP_ASSUM MP_TAC
1603 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1604 THEN STRIP_TAC
1605 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)))
1606       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
1607 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1608 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)))
1609       (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`]
1610 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)))
1611       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
1612 THEN POP_ASSUM MP_TAC
1613 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1614 THEN RESA_TAC
1615 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1616 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)))
1617       (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`]
1618 THEN POP_ASSUM MP_TAC
1619 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
1620 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1621 THEN RESA_TAC
1622 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1623 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1624 THEN MRESA_TAC WEDGE_LUNE[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`]
1625 THEN POP_ASSUM MP_TAC
1626 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1627 THEN RESA_TAC
1628 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)))
1629       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
1630 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1631 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)))
1632       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
1633 THEN POP_ASSUM MP_TAC
1634 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1635 THEN RESA_TAC
1636 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1637 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)))
1638       (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`]
1639 THEN POP_ASSUM MP_TAC
1640 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
1641 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1642 THEN RESA_TAC
1643 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;INTER]
1644 THEN DISCH_THEN(LABEL_TAC"YEU1")
1645 THEN REPEAT STRIP_TAC;
1646 REMOVE_THEN "YEU1"(fun th-> MRESA1_TAC th`x'':real^3`)
1647 THEN REMOVE_ASSUM_TAC
1648 THEN POP_ASSUM MP_TAC
1649 THEN REWRITE_TAC[REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
1650 THEN STRIP_TAC;
1651 SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y, z:real^3}` ASSUME_TAC;
1652 ASM_REWRITE_TAC[INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
1653 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1654 THEN ASM_REWRITE_TAC[];
1655 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]
1656 THEN POP_ASSUM MP_TAC
1657 THEN POP_ASSUM MP_TAC
1658 THEN ASM_REWRITE_TAC[]
1659 THEN SET_TAC[];
1660 REMOVE_THEN "YEU1"(fun th-> MRESA1_TAC th`x'':real^3`)
1661 THEN POP_ASSUM MP_TAC
1662 THEN REWRITE_TAC[REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
1663 THEN STRIP_TAC;
1664 SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y1, y:real^3}` ASSUME_TAC;
1665 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y1:real^3`;`y:real^3`]
1666 THEN POP_ASSUM MP_TAC
1667 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1668 THEN RESA_TAC
1669 THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
1670 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1671 THEN ASM_REWRITE_TAC[];
1672 POP_ASSUM MP_TAC
1673 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`]
1674 THEN REMOVE_ASSUM_TAC
1675 THEN POP_ASSUM MP_TAC
1676 THEN REWRITE_TAC[F_SY;IN_ELIM_THM;PAIR_EQ]
1677 THEN STRIP_TAC
1678 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]
1679 THEN SET_TAC[]]);;
1680
1681
1682 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/\
1683 {u,w} SUBSET V_SY(vecmats(l))
1684 /\ norm(u-w)<= cstab
1685 /\ &2<= norm(u-w)
1686 /\ ~({u,w} IN E_SY(vecmats l))
1687 /\l IN B_SY1 a b
1688 ==> ~(collinear ({vec 0} UNION {u,w}))`,
1689 REPEAT STRIP_TAC
1690 THEN POP_ASSUM MP_TAC
1691 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)
1692 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
1693 THEN POP_ASSUM MP_TAC
1694 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1695 THEN POP_ASSUM MP_TAC
1696 THEN POP_ASSUM MP_TAC
1697 THEN POP_ASSUM MP_TAC
1698 THEN DISCH_THEN(LABEL_TAC"THY")
1699 THEN STRIP_TAC
1700 THEN STRIP_TAC
1701 THEN POP_ASSUM(fun th-> MP_TAC th
1702 THEN REWRITE_TAC[convex_local_fan]
1703 THEN STRIP_TAC
1704 THEN POP_ASSUM MP_TAC
1705 THEN POP_ASSUM(fun th1-> MP_TAC th1
1706 THEN REWRITE_TAC[local_fan]
1707 THEN LET_TAC
1708 THEN STRIP_TAC
1709 THEN POP_ASSUM MP_TAC
1710 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
1711 THEN STRIP_TAC
1712 THEN ASSUME_TAC th1)
1713 THEN DISCH_THEN(LABEL_TAC"THY1")
1714 THEN ASSUME_TAC th)
1715 THEN STRIP_TAC
1716 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1717 THEN MATCH_MP_TAC NONPARALLEL_BALL_ANNULUS
1718 THEN ASM_REWRITE_TAC[]
1719 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l)
1720 ==> u IN V_SY(vecmats l) /\ w IN V_SY(vecmats (l:real^(M,3)finite_product))`)
1721 THEN ASM_REWRITE_TAC[]
1722 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1723 THEN STRIP_TAC
1724 THEN REMOVE_THEN"THY" (fun th-> MRESA1_TAC th`i:num` THEN  MRESA1_TAC th`i':num` ));;
1725
1726 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/\
1727 {u,w} SUBSET V_SY(vecmats(l))
1728 /\ norm(u-w)<= cstab
1729 /\ &2<= norm(u-w)
1730 /\ ~({u,w} IN E_SY(vecmats l))
1731 /\l IN B_SY1 a b
1732 ==> ~(collinear ({vec 0} UNION {u,w}))
1733 /\ (!x. x IN F_SY(vecmats l)==> aff_gt {vec 0}{u,w} SUBSET wedge_in_fan_gt x (E_SY (vecmats l)))`,
1734 GEN_TAC
1735 THEN STRIP_TAC
1736 THEN STRIP_TAC
1737 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`];
1738 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`]]);;
1739
1740
1741 end;;
1742