legacy/oldfan/VBTIKLP.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  Sum_azim_node = struct
  13
  14
  15
  16
  17 open Sphere;;
  18 open Fan_defs;;
  19 open Hypermap_of_fan;;
  20 open Tactic_fan;;
  21 open Lemma_fan;;
  22 open Fan;;
  23 open Hypermap_of_fan;;
  24 open Node_fan;;
  25 open Azim_node;;
  26
  27
  28
  29 (* ========================================================================== *)
  30 (*                   UNIONS IN  NODE OF FAN                        *)
  31 (* ========================================================================== *)
  32
  33
  34 (*wedge2_fan=aff_gt*)
  35
  36
  37 let lemma_disjiont_exists_fan2=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 n:num.
  38  ~(v=x) /\ ~(u=x) /\ (~(collinear {x, v, u})) /\ {v,u} IN E /\ (v IN V) /\ (u IN V) /\ fan (x,V,E)
  39  ==> if_azims_fan x V E v u (0) = &0`,
  40 REPEAT GEN_TAC THEN REWRITE_TAC[fan;fan1] THEN STRIP_TAC
  41   THEN MP_TAC(ISPECL [`v:real^3`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1)
  42   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  43   THEN SUBGOAL_THEN `(u:real^3) IN set_of_edge (v:real^3) (V:real^3->bool)(E:(real^3->bool)->bool)` ASSUME_TAC
  44   THENL[
  45     REWRITE_TAC[set_of_edge; IN_ELIM_THM] THEN ASM_REWRITE_TAC[];
  46     SUBGOAL_THEN ` ~( 0 = CARD (set_of_edge (v:real^3) (V:real^3->bool)(E:((real^3)->bool)->bool))) ` ASSUME_TAC
  47       THENL[
  48         STRIP_TAC
  49           THEN MP_TAC(ISPEC `set_of_edge (v:real^3) (V:real^3->bool) (E:((real^3)->bool)->bool)`CARD_EQ_0)
  50           THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[];
  51         SUBGOAL_THEN `azim (x:real^3) (v:real^3) (u:real^3) (u:real^3)= &0` ASSUME_TAC
  52         THENL[
  53           ASM_MESON_TAC[ AZIM_REFL];
  54           REWRITE_TAC[if_azims_fan; power_map_points;azim;] THEN ASM_REWRITE_TAC[]]]]);;
  55
  56
  57
  58
  59
  60
  61 let lemma_disjiont_exists_fan3=prove(
  62 `!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 y:real^3 n:num.
  63  ~(v=x) /\ ~(u=x) /\ (~(collinear {x, v, u})) /\ {v,u} IN E /\ (v IN V) /\ (u IN V) /\ fan (x,V,E)
  64  ==> (if_azims_fan x V E v u 0 <= azim x v u y)`,
  65 REPEAT GEN_TAC THEN STRIP_TAC
  66   THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `y:real^3`] azim)
  67   THEN STRIP_TAC
  68   THEN MP_TAC(ISPECL[`x:real^3` ; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)` ;`v:real^3` ;`u:real^3`; `n:num`]lemma_disjiont_exists_fan2)
  69   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[azim]);;
  70
  71
  72 let wedge2_fan=new_definition`wedge2_fan (x:real^3)  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) =
  73 {y:real^3 | ( if_azims_fan x V E v u i = azim x v u y)/\ ( y IN complement_set {x, v})}`;;
  74
  75
  76
  77 let aff_gt_subset_wedge_fan2=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 i:num.
  78  ~(i= CARD (set_of_edge v V E))
  79 /\  ~collinear {x,v,u} /\ ~collinear {x,v, power_map_points sigma_fan x V E v u i}
  80 ==>
  81  aff_gt {x , v} {power_map_points sigma_fan x V E v u i}  SUBSET wedge2_fan x V E v u i `,
  82
  83 REWRITE_TAC[SUBSET] THEN REPEAT GEN_TAC THEN
  84 ASSUME_TAC(affine_hull_2_fan)
  85 THEN STRIP_TAC THEN ASSUME_TAC(th3)
  86 THEN  POP_ASSUM (MP_TAC o ISPECL [`x:real^3`;`v:real^3`;`(power_map_points sigma_fan (x:real^3)  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))`])
  87 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  88 THEN ASSUME_TAC(AFF_GT_2_1)
  89   THEN  POP_ASSUM (MP_TAC o ISPECL [`x:real^3`;`v:real^3`;`(power_map_points sigma_fan (x:real^3)  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))`])
  90 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
  91 THEN GEN_TAC THEN REWRITE_TAC[wedge2_fan; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
  92 REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `~((t3:real) = &0)` ASSUME_TAC
  93 THENL
  94    [REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
  95 ASSUME_TAC(th1)
  96 THEN POP_ASSUM( MP_TAC o ISPECL[`x:real^3`;` v:real^3`;` u:real^3`;` power_map_points sigma_fan x V E v u i` ;`t1:real` ;`t2:real` ;`t3:real`])
  97   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
  98 SUBGOAL_THEN `t1 % x + t2 % v + t3 % power_map_points sigma_fan x V E v u i IN
  99  complement_set {x, v}` ASSUME_TAC
 100 THENL
 101       [ASM_MESON_TAC[COMPLEMENT_SET_FAN];
 102 ASM_REWRITE_TAC[] THEN REWRITE_TAC[if_azims_fan;]
 103 THEN ASM_MESON_TAC[REAL_ARITH`((t3:real)> &0) <=> (&0 < t3)`]]]);;
 104
 105
 106
 107 let wedge_fan2_subset_aff_gt=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 i:num.
 108  ~collinear {x,v,u} /\ ~collinear {x, v, power_map_points sigma_fan x V E v u i}
 109 /\  ~(i= CARD (set_of_edge v V E))
 110 ==>
 111 wedge2_fan x V E v u i SUBSET aff_gt {x , v} {power_map_points sigma_fan x V E v u i}`,
 112 REPEAT GEN_TAC THEN
 113 ASSUME_TAC(affine_hull_2_fan) THEN
 114 STRIP_TAC THEN ASSUME_TAC(th3)
 115 THEN  POP_ASSUM (MP_TAC o ISPECL [`x:real^3`;`v:real^3`;`(power_map_points sigma_fan (x:real^3)  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))`])
 116 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 117 THEN ASSUME_TAC(AFF_GT_2_1)
 118   THEN  POP_ASSUM (MP_TAC o ISPECL [`x:real^3`;`v:real^3`;`(power_map_points sigma_fan (x:real^3)  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))`])
 119 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 120  THEN REWRITE_TAC[SUBSET] THEN GEN_TAC
 121   THEN REWRITE_TAC[wedge2_fan;IN_ELIM_THM] THEN REWRITE_TAC[if_azims_fan; azim] THEN ASM_REWRITE_TAC[]
 122 THEN STRIP_TAC
 123   THEN ASSUME_TAC(th2) THEN POP_ASSUM(MP_TAC o ISPECL[`x:real^3`; `v:real^3`;`x':real^3`])
 124 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 125   THEN ASSUME_TAC(th)
 126 THEN POP_ASSUM (MP_TAC o SPECL [`x:real^3`;`v:real^3`;`u:real^3`;`(power_map_points sigma_fan x  (V:real^3->bool) (E:(real^3->bool)->bool) v u (i:num)):real^3`;]) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[EXTENSION] THEN DISCH_TAC
 127   THEN POP_ASSUM (MP_TAC o ISPEC `x':real^3`)THEN
 128  REWRITE_TAC[IN_ELIM_THM] THEN ASM_REWRITE_TAC[]);;
 129
 130
 131
 132 let wedge_fan2_equal_aff_gt=prove(
 133 ` !x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 i:num.
 134  ~collinear {x,v,u} /\ ~collinear {x, v, power_map_points sigma_fan x V E v u i}
 135 /\  ~(i= CARD (set_of_edge v V E))
 136 ==>
 137  wedge2_fan x V E v u i = aff_gt {x , v} {power_map_points sigma_fan x V E v u i}    `,
 138 REPEAT GEN_TAC THEN STRIP_TAC THEN
 139 SUBGOAL_THEN `wedge2_fan x V E v u i SUBSET aff_gt {x , v} {power_map_points sigma_fan x V E v u i}` ASSUME_TAC
 140 THENL
 141   [ ASM_MESON_TAC[ wedge_fan2_subset_aff_gt;aff_gt_subset_wedge_fan2];
 142    SUBGOAL_THEN `
 143       aff_gt {(x:real^3), (v:real^3)} {power_map_points sigma_fan (x:real^3)  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)}  SUBSET wedge2_fan (x:real^3) V E (v:real^3) (u:real^3) (i:num)` ASSUME_TAC
 144 THENL[ASM_MESON_TAC[aff_gt_subset_wedge_fan2];
 145       ASM_SET_TAC[]]]);;
 146
 147
 148 let wedge_fan2_equal_aff_gt_fan=prove(` !x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 i:num.
 149 FAN(x,V,E)/\ ({v,u} IN E)
 150 /\  ~(i= CARD (set_of_edge v V E))
 151 ==>
 152  wedge2_fan x V E v u i = aff_gt {x , v} {power_map_points sigma_fan x V E v u i}    `,
 153
 154  REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"a") THEN USE_THEN "a" MP_TAC
 155   THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "b")
 156   THEN REPEAT STRIP_TAC
 157 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (u:real^3)`]properties_of_set_of_edge_fan)
 158 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
 159 THEN
 160 MP_TAC(ISPECL[`(i:num)`; `(x:real^3)`;` (V:real^3->bool)`;
 161 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`] image_power_map_points) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 162 THEN
 163  MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)`]properties_of_set_of_edge_fan)
 164 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN USE_THEN "b" (fun th-> MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th))  THEN REMOVE_THEN "b" (fun th-> MP_TAC(ISPEC`{(v:real^3),(power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN DISCH_TAC THEN DISCH_TAC THEN ASM_MESON_TAC[wedge_fan2_equal_aff_gt]);;
 165
 166
 167 (*****wedge3_fan=w_dart_fan*******)
 168
 169 let wedge3_fan=new_definition`wedge3_fan (x:real^3)  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) =
 170 {y:real^3 | ( if_azims_fan x V E v u (i) < azim x v u y)/\
 171 (azim x v u y < if_azims_fan x V E v u (SUC i)) /\( y IN complement_set {x, v})}`;;
 172
 173
 174
 175
 176
 177
 178
 179
 180 let w_dart_eq_wedge3_fan=prove(` !x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 i:num.
 181  FAN(x,V,E) /\ ({v,u} IN E)
 182 /\  (i< CARD (set_of_edge v V E))
 183 /\ CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))> 1
 184 ==>
 185 w_dart_fan x V E (x,v,power_map_points sigma_fan x V E v u i, power_map_points sigma_fan x V E v u (SUC i))
 186 = wedge3_fan x V E v u i`,
 187
 188 REPEAT GEN_TAC THEN STRIP_TAC
 189   THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN USE_THEN "a" MP_TAC THEN REWRITE_TAC[FAN;fan6] THEN
 190 STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"1") THEN REPEAT STRIP_TAC
 191 THEN MP_TAC(ISPECL[`x:real^3 `;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;` v:real^3`]th4) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 192 THEN
 193 ASM_REWRITE_TAC[w_dart_fan;wedge;wedge3_fan;complement_set; IN_ELIM_THM;collinear_fan]
 194   THEN DISJ_CASES_TAC(ARITH_RULE`i=0 \/ 0< (i:num)`)
 195 THENL[
 196
 197 MP_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))  >  1 ==> ~(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))= 0)/\ ~(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))=1)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 198 ASM_REWRITE_TAC[power_map_points;if_azims_fan;ARITH_RULE`SUC 0 =1`;AZIM_REFL;]  THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[];
 199
 200 MP_TAC(ARITH_RULE`(i:num)<CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))==> ~(i=CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 201  MP_TAC(ISPECL[`x:real^3 `;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`;`i:num`]SUM_IF_AZIMS_FAN)
 202    THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC "bc") THEN ASM_REWRITE_TAC[if_azims_fan;EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC
 203 THENL[
 204
 205 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(REAL_ARITH`azim (x:real^3) (v:real^3) ( power_map_points sigma_fan (x:real^3)
 206  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)) (x':real^3) < azim (x:real^3) (v:real^3)
 207 ( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))
 208 (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 209  (power_map_points sigma_fan (x:real^3) (V:real^3->bool)
 210 (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)) )
 211 ==> azim (x:real^3) (v:real^3) (u:real^3) ( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)
 212  (v:real^3) (u:real^3) (i:num)) + azim (x:real^3) (v:real^3) ( power_map_points sigma_fan (x:real^3) (V:real^3->bool)
 213  (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)) (x':real^3)< azim (x:real^3) (v:real^3) (u:real^3)
 214 ( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))
 215  + azim (x:real^3) (v:real^3) ( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 216  (u:real^3) (i:num)) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 217 ( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)) )`)
 218   THEN ASM_REWRITE_TAC[]
 219 THEN REMOVE_THEN "bc" MP_TAC THEN  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o REDEPTH_CONV) [if_azims_fan;power_map_points]
 220  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 221 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]) THEN DISCH_TAC
 222   THEN ASSUME_TAC (ISPECL[`x:real^3 `;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`;`SUC i:num`]if_azims_works_fan)
 223   THEN MP_TAC(REAL_ARITH`azim (x:real^3) (v:real^3) (u:real^3) ( power_map_points sigma_fan (x:real^3)
 224  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)) + azim (x:real^3) (v:real^3)
 225 ( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))
 226 (x':real^3)< if_azims_fan  (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)
 227  (v:real^3) (u:real^3) (SUC(i:num)) /\ if_azims_fan  (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)
 228  (v:real^3) (u:real^3) (SUC(i:num)) <= &2 *pi ==>  azim (x:real^3) (v:real^3) (u:real^3)
 229 ( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))
 230  + azim (x:real^3) (v:real^3) ( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 231  (u:real^3) (i:num)) (x':real^3)< &2 * pi`)
 232   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`x':real^3`]collinear_fan) THEN ASM_REWRITE_TAC[]
 233   THEN DISCH_TAC
 234   THEN MP_TAC(ISPECL[`i:num`;`x:real^3 `;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`]IN2_ORBITS_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 235   THEN MP_TAC(ISPECL[`SUC(i:num)`;`x:real^3 `;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`]IN2_ORBITS_FAN) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 236   THEN REMOVE_THEN "1" (fun th-> MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)THEN ASSUME_TAC(th))
 237   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC`{(v:real^3),( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 238  (u:real^3) (i:num))}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a}UNION {b,c}={a,b,c}`]THEN DISCH_TAC THEN DISCH_TAC
 239   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 240  (u:real^3) (i:num))`; `x':real^3`]sum3_azim_fan) THEN ASM_REWRITE_TAC[]
 241   THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 242   THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real) < a +b <=> &0 < b`; REAL_ARITH`(a:real) + c< a +b<=> c< b`;];
 243
 244 STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 245   THEN DISCH_THEN(LABEL_TAC"ma1") THEN DISCH_THEN(LABEL_TAC"ma2") THEN DISCH_TAC
 246 THEN ASM_REWRITE_TAC[] THEN
 247 MP_TAC(REAL_ARITH`azim (x:real^3) (v:real^3) (u:real^3) ( power_map_points sigma_fan (x:real^3)
 248  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)) < azim (x:real^3) (v:real^3) (u:real^3)
 249 (x':real^3)
 250 ==> azim (x:real^3) (v:real^3) (u:real^3) ( power_map_points sigma_fan (x:real^3)
 251  (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)) <= azim (x:real^3) (v:real^3) (u:real^3)
 252 (x':real^3)
 253 `)
 254   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 255 THEN
 256  MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`x':real^3`]collinear_fan) THEN ASM_REWRITE_TAC[]
 257   THEN DISCH_TAC
 258   THEN MP_TAC(ISPECL[`i:num`;`x:real^3 `;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`]IN2_ORBITS_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 259   THEN MP_TAC(ISPECL[`SUC(i:num)`;`x:real^3 `;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`]IN2_ORBITS_FAN) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 260   THEN REMOVE_THEN "1" (fun th-> MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)THEN ASSUME_TAC(th))
 261   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC`{(v:real^3),( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 262  (u:real^3) (i:num))}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a}UNION {b,c}={a,b,c}`]THEN DISCH_TAC THEN DISCH_TAC
 263   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 264  (u:real^3) (i:num))`; `x':real^3`]sum4_azim_fan) THEN ASM_REWRITE_TAC[]
 265   THEN DISCH_TAC
 266   THEN REMOVE_THEN "ma1" MP_TAC THEN REMOVE_THEN "ma2" MP_TAC
 267 THEN ASM_REWRITE_TAC[power_map_points] THEN REAL_ARITH_TAC]]);;
 268
 269
 270
 271
 272
 273
 274
 275
 276 let UNION_FAN=prove(
 277 `!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (u:real^3).
 278 FAN(x,V,E)/\ ({v,u}IN E)
 279 ==>
 280  (UNIV:real^3->bool) = aff {x,v} UNION (UNIONS {wedge3_fan x V E v u i|i| 0 <= i /\ i< CARD(set_of_edge v V E) })
 281 UNION
 282  (UNIONS {wedge2_fan x V E v u i|i| 0 <= i /\ i< CARD(set_of_edge v V E) } )
 283 `,
 284
 285 REPEAT STRIP_TAC THEN REWRITE_TAC[EXTENSION; UNION;IN_ELIM_THM] THEN  GEN_TAC THEN EQ_TAC
 286 THENL(*1*)[
 287 STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`(x':real^3) IN aff {(x:real^3),(v:real^3)} \/ ~((x':real^3) IN aff {x,v})`)
 288 THENL(*2*)[
 289 ASM_SET_TAC[];(*2*)
 290
 291 ASM_REWRITE_TAC[]
 292   THEN DISJ_CASES_TAC(SET_RULE`(x':real^3) IN (UNIONS {wedge2_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)|i| 0 <= i /\ i< CARD(set_of_edge v V E)} )
 293  \/ ~((x':real^3) IN (UNIONS {wedge2_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)|i| 0 <= i/\ i< CARD(set_of_edge v V E)}) )`)
 294 THENL(*3*)[
 295 ASM_REWRITE_TAC[];(*3*)
 296 ASM_REWRITE_TAC[]
 297   THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[UNIONS;IN_ELIM_THM;NOT_EXISTS_THM;DE_MORGAN_THM;ARITH_RULE `(0 <= (i:num))`]
 298   THEN DISCH_TAC THEN SUBGOAL_THEN`!i:num. ~((x':real^3) IN wedge2_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))\/ ~(i< CARD(set_of_edge v V E)) ` ASSUME_TAC
 299 THENL(*4*)[
 300 ASM_SET_TAC[];(*4*)
 301
 302 POP_ASSUM MP_TAC THEN REWRITE_TAC[wedge2_fan;IN_ELIM_THM] THEN DISCH_THEN(LABEL_TAC"100")
 303   THEN SUBGOAL_THEN`(~((x':real^3) IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)))` ASSUME_TAC
 304 THENL(*5*)[
 305 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`]SIMP_ORBITS_POINTS_FAN) THEN ASM_REWRITE_TAC[]
 306   THEN DISCH_TAC
 307   THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
 308   THEN REWRITE_TAC[IN_ELIM_THM] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN STRIP_TAC
 309   THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPEC`i:num`th))
 310   THEN MP_TAC(ARITH_RULE`(i:num) < CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))==> ~(i=CARD(set_of_edge v V E))`)
 311   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 312   THEN ASM_REWRITE_TAC[if_azims_fan;complement_set; IN_ELIM_THM]
 313   THEN ASM_MESON_TAC[remark_power_map_points];(*5*)
 314
 315 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`]SIMP_ORBITS_POINTS_FAN) THEN ASM_REWRITE_TAC[]
 316   THEN DISCH_THEN(LABEL_TAC"a")
 317   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`x':real^3`]exists_inverse_in_orbits_sigma_fan) THEN ASM_REWRITE_TAC[azim1]
 318   THEN STRIP_TAC
 319   THEN POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC
 320   THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"b")
 321 THEN DISCH_TAC THEN DISCH_TAC
 322   THEN   REMOVE_THEN "b" MP_TAC
 323   THEN REMOVE_THEN  "a"(fun th->REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
 324   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN DISCH_TAC
 325   THEN REWRITE_TAC[IN_ELIM_THM]
 326   THEN STRIP_TAC
 327   THEN EXISTS_TAC`wedge3_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)`
 328   THEN STRIP_TAC
 329 THENL(*6*)[
 330 EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[];(*6*)
 331
 332 ASM_REWRITE_TAC[wedge3_fan; complement_set; IN_ELIM_THM;]
 333   THEN SUBGOAL_THEN`if_azims_fan x (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) < azim (x:real^3) v u (x':real^3)` ASSUME_TAC
 334 THENL(*7*)[
 335 MP_TAC(ARITH_RULE`(i:num) < CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))==> ~(i=CARD(set_of_edge v V E))`)
 336   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 337   THEN ASM_REWRITE_TAC[if_azims_fan;complement_set; IN_ELIM_THM]
 338   THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th)) THEN POP_ASSUM MP_TAC
 339 THEN DISJ_CASES_TAC(ARITH_RULE`(i:num)=0 \/ 0< i`)
 340 THENL(*8*)[
 341
 342 ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC THEN ASM_REWRITE_TAC[AZIM_REFL]
 343   THEN POP_ASSUM (fun th->REWRITE_TAC[])
 344   THEN POP_ASSUM (fun th->REWRITE_TAC[])
 345   THEN POP_ASSUM (fun th->REWRITE_TAC[])
 346   THEN POP_ASSUM (fun th->REWRITE_TAC[])
 347   THEN POP_ASSUM (fun th->REWRITE_TAC[])
 348   THEN POP_ASSUM (fun th->REWRITE_TAC[])
 349   THEN POP_ASSUM (fun th->REWRITE_TAC[])
 350   THEN POP_ASSUM (fun th->MP_TAC(ISPEC`0`th)) THEN DISCH_THEN(LABEL_TAC"a")
 351   THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[if_azims_fan;power_map_points;DE_MORGAN_THM; complement_set; IN_ELIM_THM;AZIM_REFL;ARITH_RULE`(~(0<a)<=> (0=a))`]
 352   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`]azim ) THEN POP_ASSUM MP_TAC
 353   THEN REAL_ARITH_TAC;(*8*)
 354
 355 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;] u_IN_ORBITS_FAN) THEN  DISCH_TAC
 356   THEN SUBGOAL_THEN `~(u=(x':real^3))` ASSUME_TAC
 357 THENL(*9*)[
 358 ASM_SET_TAC[];(*9*)
 359
 360  DISCH_TAC  THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[]
 361 THEN REWRITE_TAC[REAL_ARITH`(b:real)- a<= b-c <=> c <= a`]  THEN DISCH_THEN(LABEL_TAC"b1")
 362    THEN MP_TAC(ARITH_RULE`0< (i:num)/\ i <CARD(set_of_edge (v:real^3) V E)==> ~(0=CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 363   THEN DISCH_TAC
 364   THEN USE_THEN"100"(fun th-> MP_TAC(ISPEC`0`th)) THEN
 365 REWRITE_TAC[if_azims_fan] THEN ASM_REWRITE_TAC[power_map_points;AZIM_REFL;complement_set; IN_ELIM_THM]
 366    THEN MP_TAC(ARITH_RULE`i <CARD(set_of_edge (v:real^3) V E)==> ~(i=CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 367   THEN DISCH_TAC
 368   THEN USE_THEN"100"(fun th-> MP_TAC(ISPEC`i:num`th)) THEN
 369 REWRITE_TAC[if_azims_fan] THEN ASM_REWRITE_TAC[power_map_points;AZIM_REFL;complement_set; IN_ELIM_THM]
 370
 371   THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b <=> b=a`] THEN DISCH_TAC
 372 THEN
 373 DISJ_CASES_TAC(SET_RULE`collinear {(x:real^3),v,x'} \/ ~collinear {x,v,x'}`)
 374 THENL(*10*)[
 375
 376 POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [SET_RULE`{a,b,c}= {a,c,b}`]
 377   THEN REWRITE_TAC[COLLINEAR_3_EXPAND;]
 378   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;` (v:real^3)`] remark1_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 379   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 380   THEN SUBGOAL_THEN `(x':real^3) IN aff {x,v}` ASSUME_TAC
 381 THENL(*11*)[
 382 REWRITE_TAC[aff; AFFINE_HULL_2; IN_ELIM_THM] THEN EXISTS_TAC`u':real` THEN EXISTS_TAC`&1 -(u':real)` THEN ASM_REWRITE_TAC[]
 383   THEN REAL_ARITH_TAC;(*11*)
 384 ASM_MESON_TAC[]](*11*);(*10*)
 385
 386 STRIP_TAC
 387 THENL(*11*)[
 388 POP_ASSUM MP_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;` (v:real^3)`] remark1_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 389   THEN MP_TAC(ISPECL[`i:num`;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] remark_power_map_points) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 390 THEN
 391 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 392  (u:real^3) (i:num))`]AZIM_EQ_ALT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 393   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 394  (u:real^3) (i:num))`;`x':real^3`]AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 395   THEN DISCH_TAC THEN  MP_TAC(ISPECL[`(x:real^3) `;`(v:real^3)`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 396  (u:real^3) (i:num))`;` (x':real^3)`] AZIM_COMPL) THEN  ASM_REWRITE_TAC[]
 397   THEN MP_TAC(ISPECL[`(x:real^3) `;`(v:real^3)`;` (u:real^3)`;`(x':real^3)`] AZIM_COMPL) THEN  ASM_REWRITE_TAC[]  THEN DISCH_TAC THEN DISCH_TAC
 398   THEN REMOVE_THEN"b1" MP_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`b-a<= b-c <=> c<= a`]
 399   THEN DISCH_TAC
 400   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`; `( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 401  (u:real^3) (i:num))`;` (x':real^3)`]sum5_azim_fan)
 402   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 403   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 404  (u:real^3) (i:num))`;` (x':real^3)`]azim) THEN POP_ASSUM MP_TAC
 405   THEN POP_ASSUM(fun th->REWRITE_TAC[])
 406   THEN POP_ASSUM(fun th->REWRITE_TAC[])
 407   THEN POP_ASSUM(fun th->REWRITE_TAC[])
 408   THEN POP_ASSUM(fun th->REWRITE_TAC[])
 409   THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*11*)
 410 REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC](*11*)](*10*)](*9*)](*8*);(*7*)
 411
 412
 413 ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"b") THEN DISCH_THEN(LABEL_TAC"c")
 414   THEN  DISJ_CASES_TAC(ARITH_RULE`SUC (i:num)= CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))\/ ~(SUC (i)= CARD(set_of_edge v V E))`)
 415 THENL(*8*)[
 416
 417 ASM_REWRITE_TAC[if_azims_fan] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`]azim) THEN REAL_ARITH_TAC;
 418 (*8*)
 419 DISJ_CASES_TAC(ARITH_RULE`(i:num)=0 \/ 0<i `)
 420 THENL(*9*)[
 421 REMOVE_THEN "b" MP_TAC THEN
 422 ASM_REWRITE_TAC[if_azims_fan;power_map_points] THEN DISCH_TAC
 423   THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(SYM(th)))
 424   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;] u_IN_ORBITS_FAN) THEN ASM_REWRITE_TAC[] THEN  DISCH_TAC
 425 THEN
 426 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`w:real^3`] IN_ORBITS_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 427   THEN SUBGOAL_THEN `~(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 428  (w:real^3)=(x':real^3))` ASSUME_TAC
 429 THENL(*10*)[ASM_SET_TAC[];(*10*)
 430
 431 REMOVE_THEN "a" (fun th -> MP_TAC(ISPEC`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 432  (w:real^3)`th)) THEN ASM_REWRITE_TAC[REAL_ARITH`b-a<= b-c <=> c<= a`]THEN DISCH_THEN(LABEL_TAC"b1")
 433    THEN MP_TAC(ARITH_RULE`(i:num)=0/\ i <CARD(set_of_edge (v:real^3) V E)==> ~(0=CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 434   THEN DISCH_TAC
 435   THEN USE_THEN"100"(fun th-> MP_TAC(ISPEC`i:num`th)) THEN
 436 REWRITE_TAC[if_azims_fan] THEN ASM_REWRITE_TAC[power_map_points;AZIM_REFL;complement_set; IN_ELIM_THM]
 437
 438   THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b <=> b=a`] THEN DISCH_TAC
 439
 440    THEN MP_TAC(ARITH_RULE`(i:num)=0/\ ~(SUC(i) =CARD(set_of_edge (v:real^3) V E))==> ~(SUC(0)=CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 441   THEN DISCH_TAC
 442   THEN USE_THEN"100"(fun th-> MP_TAC(ISPEC`SUC(0):num`th)) THEN
 443 REWRITE_TAC[if_azims_fan] THEN ASM_REWRITE_TAC[power_map_points;AZIM_REFL;complement_set; IN_ELIM_THM]
 444
 445   THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b <=> b=a`] THEN REWRITE_TAC[power_map_points]
 446 THEN
 447 DISJ_CASES_TAC(SET_RULE`collinear {(x:real^3),v,x'} \/ ~collinear {x,v,x'}`)
 448 THENL(*11*)[
 449 POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [SET_RULE`{a,b,c}= {a,c,b}`]
 450   THEN REWRITE_TAC[COLLINEAR_3_EXPAND;]
 451   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;` (v:real^3)`] remark1_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 452   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 453   THEN SUBGOAL_THEN `(x':real^3) IN aff {x,v}` ASSUME_TAC
 454 THENL(*12*)[
 455 REWRITE_TAC[aff; AFFINE_HULL_2; IN_ELIM_THM] THEN EXISTS_TAC`u':real` THEN EXISTS_TAC`&1 -(u':real)` THEN ASM_REWRITE_TAC[]
 456   THEN REAL_ARITH_TAC;(*12*)
 457 ASM_MESON_TAC[]](*12*);(*11*)
 458
 459 STRIP_TAC THENL(*12*)[
 460
 461 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;` (v:real^3)`] remark1_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 462   THEN MP_TAC(SET_RULE`(u:real^3)=(w:real^3) /\ {v,u} IN (E:(real^3->bool)->bool)==> {v,w} IN E`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 463
 464   THEN MP_TAC(ISPECL[`SUC(0):num`;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] remark_power_map_points) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 465 THEN
 466 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 467  (u:real^3) (SUC(0):num))`]AZIM_EQ_ALT) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 468   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 469  (u:real^3) (SUC(0):num))`;`x':real^3`]AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 470   THEN MP_TAC(ISPECL[`(x:real^3) `;`(v:real^3)`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 471  (u:real^3) (SUC(0):num))`;` (x':real^3)`] AZIM_COMPL) THEN  ASM_REWRITE_TAC[power_map_points]
 472   THEN MP_TAC(ISPECL[`(x:real^3) `;`(v:real^3)`;` (u:real^3)`;`(x':real^3)`] AZIM_COMPL) THEN  ASM_REWRITE_TAC[]  THEN DISCH_TAC THEN DISCH_TAC
 473   THEN REMOVE_THEN"b1" MP_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`b-a<= b-c <=> c<= a`]
 474   THEN DISCH_TAC
 475   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 476  (u:real^3) (SUC(0):num))`;`w:real^3`;` (x':real^3)`]sum5_azim_fan)
 477   THEN ASM_REWRITE_TAC[power_map_points;REAL_ARITH`a=b+c <=> c=a-b`] THEN
 478 DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`a-b<c <=> a< b+c`]
 479   THEN MP_TAC(ARITH_RULE` (i:num) < (CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))) /\ ~(SUC(i)=CARD(set_of_edge v V E)) ==> SUC(i) < CARD(set_of_edge v V E)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 480   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`; `SUC(i):num`; `i:num`] cyclic_power_sigma_fan) THEN ASM_REWRITE_TAC[power_map_points;ARITH_RULE`0< SUC 0`; ] THEN DISCH_TAC
 481   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 482  (u:real^3))`; `w:real^3`; ] UNIQUE_AZIM_0_POINT_FAN) THEN ASM_REWRITE_TAC[power_map_points; ]
 483   THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`;` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 484  (u:real^3))`; `w:real^3`]AZIM_COMPL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`c<a+b-a <=> c<b`] THEN MESON_TAC[azim];(*12*)
 485
 486 REPEAT(POP_ASSUM MP_TAC) THEN ARITH_TAC](*12*)](*11*)](*10*);(*9*)
 487
 488 REMOVE_THEN "b" MP_TAC THEN
 489 ASM_REWRITE_TAC[if_azims_fan;power_map_points] THEN DISCH_TAC
 490   THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(SYM(th)))
 491   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`i:num`] i_IN_ORBITS_FAN) THEN ASM_REWRITE_TAC[] THEN  DISCH_TAC
 492 THEN
 493 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`w:real^3`] IN_ORBITS_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 494   THEN SUBGOAL_THEN `~(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 495  (w:real^3)=(x':real^3))` ASSUME_TAC
 496 THENL(*10*)[ ASM_SET_TAC[];(*10*)
 497
 498 REMOVE_THEN "a" (fun th -> MP_TAC(ISPEC`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 499  (w:real^3)`th)) THEN ASM_REWRITE_TAC[REAL_ARITH`b-a<= b-c <=> c<= a`]THEN DISCH_THEN(LABEL_TAC"b1")
 500    THEN MP_TAC(ARITH_RULE`i <CARD(set_of_edge (v:real^3) V E)==> ~(i=CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 501   THEN DISCH_TAC
 502   THEN USE_THEN"100"(fun th-> MP_TAC(ISPEC`i:num`th)) THEN
 503 REWRITE_TAC[if_azims_fan] THEN ASM_REWRITE_TAC[power_map_points;AZIM_REFL;complement_set; IN_ELIM_THM]
 504
 505   THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b <=> b=a`] THEN DISCH_TAC
 506   THEN USE_THEN"100"(fun th-> MP_TAC(ISPEC`SUC(i):num`th)) THEN
 507 REWRITE_TAC[if_azims_fan] THEN ASM_REWRITE_TAC[power_map_points;AZIM_REFL;complement_set; IN_ELIM_THM]
 508
 509   THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b <=> b=a`] THEN REWRITE_TAC[power_map_points]
 510 THEN
 511 DISJ_CASES_TAC(SET_RULE`collinear {(x:real^3),v,x'} \/ ~collinear {x,v,x'}`)
 512 THENL(*11*)[
 513 POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [SET_RULE`{a,b,c}= {a,c,b}`]
 514   THEN REWRITE_TAC[COLLINEAR_3_EXPAND;]
 515   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;` (v:real^3)`] remark1_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 516   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 517   THEN SUBGOAL_THEN `(x':real^3) IN aff {x,v}` ASSUME_TAC
 518 THENL(*12*)[
 519 REWRITE_TAC[aff; AFFINE_HULL_2; IN_ELIM_THM] THEN EXISTS_TAC`u':real` THEN EXISTS_TAC`&1 -(u':real)` THEN ASM_REWRITE_TAC[]
 520   THEN REAL_ARITH_TAC;(*12*)
 521 ASM_MESON_TAC[]](*12*);(*11*)
 522
 523 STRIP_TAC THENL(*12*)[
 524 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;` (v:real^3)`] remark1_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 525   THEN MP_TAC(ISPECL[`i:num`;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] remark_power_map_points) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 526   THEN MP_TAC(ISPECL[`SUC(i):num`;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] remark_power_map_points) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 527 THEN
 528 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 529  (u:real^3) (SUC(i):num))`]AZIM_EQ_ALT) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 530   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 531  (u:real^3) (SUC(i):num))`;`x':real^3`]AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 532   THEN
 533 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 534  (u:real^3) ((i):num))`]AZIM_EQ_ALT) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 535   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 536  (u:real^3) ((i):num))`;`x':real^3`]AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 537  THEN MP_TAC(ISPECL[`(x:real^3) `;`(v:real^3)`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 538  (u:real^3) (SUC(i):num))`;` (x':real^3)`] AZIM_COMPL) THEN  ASM_REWRITE_TAC[power_map_points]
 539   THEN MP_TAC(ISPECL[`(x:real^3) `;`(v:real^3)`;` (w:real^3)`;`(x':real^3)`] AZIM_COMPL) THEN  ASM_REWRITE_TAC[]  THEN DISCH_TAC THEN DISCH_TAC
 540 THEN
 541   REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[if_azims_fan] THEN DISCH_TAC THEN
 542 MP_TAC(REAL_ARITH`azim x v u w< azim (x:real^3) v u x'==> azim x v u w<= azim (x:real^3) v u x'`) THEN ASM_REWRITE_TAC[]
 543   THEN DISCH_TAC
 544     THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`(u:real^3)`;`w:real^3`;` (x':real^3)`]sum4_azim_fan)
 545   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 546   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`i:num`] SUM_IF_AZIMS_FAN) THEN ASM_REWRITE_TAC[if_azims_fan;power_map_points] THEN DISCH_TAC
 547  THEN ASM_REWRITE_TAC[REAL_ARITH`a+b<a+c <=> b<c`]
 548 THEN REMOVE_THEN"b1" MP_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`b-a<= b-c <=> c<= a`]
 549   THEN DISCH_TAC
 550   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 551  (u:real^3) (SUC(i):num))`;`w:real^3`;` (x':real^3)`]sum5_azim_fan)
 552   THEN ASM_REWRITE_TAC[power_map_points;REAL_ARITH`a=b+c <=> c=a-b`]
 553 THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`a-b<c <=> a< b+c`]
 554 THEN MP_TAC(ARITH_RULE` (i:num) < (CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))) /\ ~(SUC(i)=CARD(set_of_edge v V E)) ==> SUC(i) < CARD(set_of_edge v V E)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 555   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`; `SUC(i):num`; `i:num`] cyclic_power_sigma_fan) THEN ASM_REWRITE_TAC[power_map_points;ARITH_RULE`i< SUC i`; ] THEN DISCH_TAC
 556   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 557  (w:real^3))`; `w:real^3`; ] UNIQUE_AZIM_0_POINT_FAN) THEN ASM_REWRITE_TAC[power_map_points; ]
 558   THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`;` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 559  (w:real^3))`; `w:real^3`]AZIM_COMPL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`c<a+b-a <=> c<b`]
 560 THEN MESON_TAC[azim];(*12*)
 561
 562 REPEAT(POP_ASSUM MP_TAC) THEN ARITH_TAC](*12*)](*11*)]]]]]]]]];
 563 ASM_SET_TAC[]]);;
 564
 565 let eq_set_wdart_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (u:real^3).
 566 FAN(x,V,E)/\ ({v,u}IN E)
 567 ==>
 568 ({w_dart_fan x V E (x,v,w,(sigma_fan x V E v w))|w| {v,w} IN E }
 569 = {wedge3_fan x V E v u i|i| 0 <= i/\ i< CARD(set_of_edge v V E) })
 570 `,
 571
 572 (let lem= prove(`!x v u w.
 573 (&0 < azim x v u w) <=> ~(azim x v u w= &0)`,
 574 MESON_TAC[azim; REAL_ARITH`&0 <= a==> (&0 < a) <=> ~(a= &0)`]) in
 575 ( let lem1=prove(`!x v. ~(x = v)==>(!u. ~(u IN aff {x, v}) <=> ~collinear {x, v, u})`,
 576 MESON_TAC[collinear_fan]) in
 577 (let lem2=prove(`!v0 v1 w.
 578         ~collinear{v0,v1,w}  ==>
 579 !x. ( ~(azim v0 v1 w x = &0)/\ ~collinear{v0,v1,x} <=> ~(x IN aff_ge {v0,v1} {w}) /\ ~collinear{v0,v1,x})`,
 580 MESON_TAC[AZIM_EQ_0_GE_ALT]) in
 581
 582 REPEAT STRIP_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC
 583 THENL(*1*)[
 584 REWRITE_TAC[GSYM(EXTENSION)] THEN STRIP_TAC
 585   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] properties_of_set_of_edge_fan)
 586   THEN ASM_REWRITE_TAC[] THEN
 587 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] ORBITS_EQ_SET_EDGE_FAN)
 588   THEN ASM_REWRITE_TAC[] THEN
 589 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] SIMP_ORBITS_POINTS_FAN)
 590   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])THEN DISCH_TAC
 591 THEN POP_ASSUM(fun th->GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[th])
 592   THEN REWRITE_TAC[IN_ELIM_THM;] THEN STRIP_TAC THEN EXISTS_TAC `i:num` THEN
 593 ASM_REWRITE_TAC[ARITH_RULE`0<= (i:num)`]
 594   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 595 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`]CARD_SET_OF_ORBITS_POINTS_FAN)
 596   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 597 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
 598 THEN
 599 DISJ_CASES_TAC(ARITH_RULE`(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))>1 \/ ~((CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))> 1)`)
 600 THENL[
 601 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`i:num`] w_dart_eq_wedge3_fan)
 602   THEN ASM_REWRITE_TAC[power_map_points];
 603
 604 MP_TAC(ARITH_RULE`(i:num)<CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) /\ ~(CARD(set_of_edge v V E)>1)==> i=0`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 605 ASM_REWRITE_TAC[w_dart_fan;wedge3_fan;if_azims_fan;power_map_points]
 606   THEN DISJ_CASES_TAC(ARITH_RULE` 0= CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) \/ ~(0=CARD(set_of_edge v V E))`)
 607 THENL[
 608
 609 REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC;
 610
 611 MP_TAC(ARITH_RULE`~(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))>1) /\ ~(0=CARD(set_of_edge v V E))==> SUC (0)=CARD(set_of_edge v V E)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 612 ASM_REWRITE_TAC[complement_set;IN_ELIM_THM;AZIM_REFL;azim]
 613
 614   THEN ASM_REWRITE_TAC[] THEN
 615 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] ORBITS_EQ_SET_EDGE_FAN)
 616   THEN ASM_REWRITE_TAC[] THEN
 617 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] SIMP_ORBITS_POINTS_FAN)
 618   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])THEN
 619  POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]) THEN REWRITE_TAC[ARITH_RULE`(a:num) < SUC 0 <=> a=0`;SET_RULE`{f i| i=0}={f 0}`;
 620 power_map_points] THEN DISCH_TAC THEN
 621 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;` (v:real^3)`] remark1_fan)
 622   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 623 MP_TAC(ISPECL[`x:real^3`;`v:real^3`]lem1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 624 THEN ASM_REWRITE_TAC[lem] THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 625   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]lem2) THEN POP_ASSUM (fun th-> REWRITE_TAC[th] THEN ASSUME_TAC(th))
 626 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]aff_subset_aff_ge)
 627   THEN  POP_ASSUM (fun th-> REWRITE_TAC[th] THEN ASSUME_TAC(th)) THEN DISCH_TAC
 628   THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th;collinear_fan;]) THEN ASM_REWRITE_TAC[GSYM(DE_MORGAN_THM);]
 629   THEN ASM_SET_TAC[]]];
 630
 631 REWRITE_TAC[GSYM(EXTENSION)] THEN STRIP_TAC
 632 THEN EXISTS_TAC`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 633  (u:real^3) ((i):num)) ` THEN
 634 MP_TAC(ISPECL[`i:num`;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] remark_power_map_points) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[th])
 635   THEN DISJ_CASES_TAC(ARITH_RULE`(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))>1 \/ ~((CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))> 1)`)
 636 THENL[
 637 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`i:num`] w_dart_eq_wedge3_fan)
 638   THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[th]);
 639
 640 MP_TAC(ARITH_RULE`(i:num)<CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) /\ ~(CARD(set_of_edge v V E)>1)==> i=0`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 641 ASM_REWRITE_TAC[w_dart_fan;wedge3_fan;if_azims_fan;power_map_points]
 642   THEN DISJ_CASES_TAC(ARITH_RULE` 0= CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) \/ ~(0=CARD(set_of_edge v V E))`)
 643 THENL[
 644 REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC;
 645
 646 MP_TAC(ARITH_RULE`~(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))>1) /\ ~(0=CARD(set_of_edge v V E))==> SUC (0)=CARD(set_of_edge v V E)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 647 ASM_REWRITE_TAC[complement_set;IN_ELIM_THM;AZIM_REFL;azim]
 648
 649   THEN ASM_REWRITE_TAC[] THEN
 650 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] ORBITS_EQ_SET_EDGE_FAN)
 651   THEN ASM_REWRITE_TAC[] THEN
 652 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] SIMP_ORBITS_POINTS_FAN)
 653   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])THEN
 654  POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]) THEN REWRITE_TAC[ARITH_RULE`(a:num) < SUC 0 <=> a=0`;SET_RULE`{f i| i=0}={f 0}`;
 655 power_map_points] THEN DISCH_TAC THEN
 656 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;` (v:real^3)`] remark1_fan)
 657   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 658 MP_TAC(ISPECL[`x:real^3`;`v:real^3`]lem1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 659 THEN ASM_REWRITE_TAC[lem] THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 660   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]lem2) THEN POP_ASSUM (fun th-> REWRITE_TAC[th] THEN ASSUME_TAC(th))
 661 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]aff_subset_aff_ge)
 662   THEN  POP_ASSUM (fun th-> REWRITE_TAC[th] THEN ASSUME_TAC(th)) THEN DISCH_TAC
 663   THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th;collinear_fan;]) THEN ASM_REWRITE_TAC[GSYM(DE_MORGAN_THM);]
 664   THEN ASM_SET_TAC[]]]]))));;
 665
 666
 667
 668
 669 let eq_set_aff_gt=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (u:real^3).
 670 FAN(x,V,E)/\ ({v,u}IN E)
 671 ==> {aff_gt {x,v} {w} |w| {v,w} IN E}
 672 ={wedge2_fan x V E v u i|i| 0 <= i /\ i< CARD(set_of_edge v V E) }`,
 673
 674 REPEAT STRIP_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC
 675 THENL[
 676 REWRITE_TAC[GSYM(EXTENSION)] THEN STRIP_TAC
 677   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] properties_of_set_of_edge_fan)
 678   THEN ASM_REWRITE_TAC[] THEN
 679 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] ORBITS_EQ_SET_EDGE_FAN)
 680   THEN ASM_REWRITE_TAC[] THEN
 681 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] SIMP_ORBITS_POINTS_FAN)
 682   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])THEN DISCH_TAC
 683 THEN POP_ASSUM(fun th->GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[th])
 684   THEN REWRITE_TAC[IN_ELIM_THM;] THEN STRIP_TAC THEN EXISTS_TAC `i:num` THEN
 685   ASM_REWRITE_TAC[ARITH_RULE`0 <= i`]
 686
 687   THEN MP_TAC(ARITH_RULE`(i:num) < CARD(set_of_edge v V E) ==> ~(i= CARD(set_of_edge (v:real^3) (V:real^3->bool)(E:(real^3->bool)->bool)))`)
 688   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 689   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`i:num`] wedge_fan2_equal_aff_gt_fan)
 690
 691   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]);
 692
 693 REWRITE_TAC[GSYM(EXTENSION)] THEN STRIP_TAC
 694 THEN EXISTS_TAC`( power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)
 695  (u:real^3) ((i):num)) ` THEN
 696 MP_TAC(ISPECL[`i:num`;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`] remark_power_map_points) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[th])
 697
 698   THEN MP_TAC(ARITH_RULE`(i:num) < CARD(set_of_edge v V E) ==> ~(i= CARD(set_of_edge (v:real^3) (V:real^3->bool)(E:(real^3->bool)->bool)))`)
 699   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 700   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`;`i:num`] wedge_fan2_equal_aff_gt_fan)
 701
 702   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])]);;
 703
 704
 705
 706
 707
 708
 709 let UNION1_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (u:real^3).
 710
 711 FAN(x,V,E)/\ ({v,u}IN E)
 712 ==>
 713  (UNIV:real^3->bool) = aff {x,v} UNION (UNIONS {w_dart_fan x V E (x,v,w,(sigma_fan x V E v w))|w| {v,w} IN E })
 714 UNION
 715  (UNIONS {aff_gt {x,v} {w} |w| {v,w} IN E} )
 716 `,
 717
 718 REPEAT STRIP_TAC
 719   THEN MP_TAC (ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`]UNION_FAN) THEN ASM_REWRITE_TAC[]
 720   THEN MP_TAC (ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`]eq_set_wdart_fan) THEN ASM_REWRITE_TAC[]
 721   THEN DISCH_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
 722   THEN MP_TAC (ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (u:real^3)`]eq_set_aff_gt   ) THEN ASM_REWRITE_TAC[]
 723   THEN DISCH_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN ASM_SET_TAC[]);;
 724
 725
 726
 727 (* ========================================================================== *)
 728 (*                   DISJOINT IN  NODE OF FAN                        *)
 729 (* ========================================================================== *)
 730
 731
 732
 733 let disjoint_set_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
 734 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E)
 735 ==>
 736  w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
 737  aff_gt {x,v} {w1}={}`,
 738
 739 (let lem =prove(`!x:real^3.
 740  FINITE {x}
 741 ==>
 742 CARD {x} = 1`,MESON_TAC[CARD_SING]) in
 743 (let lem1=prove(`!x v. ~(x = v)==>(!u. ~(u IN aff {x, v}) <=> ~collinear {x, v, u})`,
 744 MESON_TAC[collinear_fan]) in
 745 (let lem2=prove(`!v0 v1 w.
 746         ~collinear{v0,v1,w}  ==>
 747 !x. ( &0 = azim v0 v1 w x /\ ~collinear{v0,v1,x} <=> (x IN aff_ge {v0,v1} {w}) /\ ~collinear{v0,v1,x})`,
 748 MESON_TAC[AZIM_EQ_0_GE_ALT]) in
 749
 750
 751 REPEAT STRIP_TAC    THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w1:real^3)`] properties_of_set_of_edge_fan)
 752   THEN ASM_REWRITE_TAC[] THEN
 753 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] ORBITS_EQ_SET_EDGE_FAN)
 754   THEN ASM_REWRITE_TAC[] THEN
 755 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] SIMP_ORBITS_POINTS_FAN)
 756   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])THEN DISCH_TAC
 757 THEN POP_ASSUM(fun th->GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[th])
 758   THEN REWRITE_TAC[IN_ELIM_THM;] THEN STRIP_TAC
 759   THEN ASM_REWRITE_TAC[]
 760   THEN MP_TAC(ARITH_RULE`i< CARD(set_of_edge (v:real^3) V E)==> ~(i=CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 761   THEN DISCH_TAC
 762   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`i:num`] wedge_fan2_equal_aff_gt_fan)
 763
 764   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
 765   THEN DISJ_CASES_TAC(ARITH_RULE`(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))>1 \/ ~((CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))> 1)`)
 766 THENL(*1*)[
 767  MP_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) V E)>1==> 0< CARD(set_of_edge v V E)`) THEN ASM_REWRITE_TAC[]
 768    THEN DISCH_TAC THEN
 769   MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`0:num`] w_dart_eq_wedge3_fan)
 770   THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 771 THEN REWRITE_TAC[wedge2_fan;wedge3_fan;EXTENSION] THEN GEN_TAC THEN
 772 REWRITE_TAC[INTER; EMPTY;IN_ELIM_THM]
 773    THEN DISJ_CASES_TAC(ARITH_RULE`(i:num)=0 \/ (0< i)`)
 774 THENL(*2*)[
 775 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;(*2*)
 776
 777  MP_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) V E)>1==> ~(0= CARD(set_of_edge v V E))/\  ~(SUC 0= CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 778    THEN DISCH_TAC THEN
 779 ASM_REWRITE_TAC[if_azims_fan]
 780 THEN
 781 MP_TAC(ARITH_RULE` (0< i)==> SUC (0)= i \/ SUC 0 <i`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 782 THENL(*3*)[
 783 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;(*3*)
 784
 785 DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w} \/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w})`)
 786 THENL(*4*)[
 787  MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`;` (v:real^3)`]remark1_fan)
 788     THEN ASM_REWRITE_TAC[IN_SING] THEN DISCH_TAC THEN ASM_REWRITE_TAC[power_map_points] THEN REAL_ARITH_TAC;(*4*)
 789
 790 MP_TAC(ISPECL[`i:num`;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`SUC (0):num`]  AZIM_LE_POWER_SIGMA_FAN)
 791   THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC](*4*)](*3*)](*2*);(*1*)
 792
 793
 794  MP_TAC(ARITH_RULE`~(CARD(set_of_edge (v:real^3) V E)>1) /\ (i< CARD(set_of_edge v V E))==> i=0/\ ~(0=CARD(set_of_edge (v:real^3) V E))`) THEN ASM_REWRITE_TAC[]
 795  THEN STRIP_TAC THEN ASM_REWRITE_TAC[]
 796 THEN ASM_REWRITE_TAC[wedge2_fan;w_dart_fan;if_azims_fan;power_map_points;complement_set;AZIM_REFL;EXTENSION] THEN GEN_TAC THEN
 797 REWRITE_TAC[DIFF;INTER;IN_ELIM_THM;GSYM(EXTENSION);COND_ELIM_THM]
 798  THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;` (v:real^3)`] remark1_fan)
 799   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 800   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;]lem1) THEN ASM_REWRITE_TAC[]
 801   THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
 802
 803   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]lem2) THEN ASM_REWRITE_TAC[]
 804 THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th] ) THEN ASM_REWRITE_TAC[collinear_fan]
 805 THEN
 806 DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w} \/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w})`)
 807
 808
 809 THENL(*2*)[
 810 ASM_SET_TAC[];(*2*)
 811
 812 MP_TAC(ARITH_RULE`~(CARD(set_of_edge (v:real^3) V E)>1) /\ ~(0= CARD(set_of_edge v V E))==> (1=CARD(set_of_edge (v:real^3) V E))`) THEN ASM_REWRITE_TAC[]
 813      THEN DISCH_TAC
 814   THEN MP_TAC(SET_RULE`w IN set_of_edge (v:real^3) V E==> {w} SUBSET set_of_edge (v:real^3) V E`) THEN ASM_REWRITE_TAC[]
 815   THEN DISCH_TAC
 816   THEN MP_TAC(ISPECL[`{(w:real^3)}`;`set_of_edge (v:real^3) V E`] FINITE_SUBSET) THEN ASM_REWRITE_TAC[]
 817  THEN DISCH_TAC THEN
 818 MP_TAC(ISPEC`w:real^3`lem) THEN ASM_REWRITE_TAC[]
 819   THEN DISCH_TAC
 820   THEN MP_TAC(ISPECL[`{(w:real^3)}`;`set_of_edge (v:real^3) V E`]CARD_SUBSET_EQ)
 821   THEN ASM_REWRITE_TAC[]]]))));;
 822
 823
 824 let disjiont1_cor6dot1 = prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 i:num.
 825 wedge3_fan x V E v u i INTER aff {x,v}={}`,
 826 REPEAT GEN_TAC THEN REWRITE_TAC[wedge3_fan; INTER] THEN REWRITE_TAC[complement_set; FUN_EQ_THM; EMPTY] THEN
 827 GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 828   THEN MESON_TAC[]);;
 829
 830
 831
 832 let disjoint_fan1=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3).
 833 FAN(x,V,E)/\ ({v,w}IN E)
 834 ==>
 835  w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER aff {x,v}={}`,
 836 REPEAT STRIP_TAC
 837   THEN DISJ_CASES_TAC(ARITH_RULE`(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))>1 \/ ~((CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))> 1)`)
 838
 839 THENL[
 840  MP_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) V E)>1==> (0<CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 841    THEN DISCH_TAC THEN
 842 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`0:num`] w_dart_eq_wedge3_fan)
 843   THEN ASM_REWRITE_TAC[power_map_points;] THEN DISCH_TAC THEN ASM_REWRITE_TAC[disjiont1_cor6dot1];
 844
 845  MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;` (v:real^3)`] remark1_fan)
 846   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 847   THEN ASM_REWRITE_TAC[w_dart_fan;INTER; IN_ELIM_THM;COND_ELIM_THM]
 848   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]aff_subset_aff_ge) THEN ASM_REWRITE_TAC[]
 849    THEN ASM_SET_TAC[]]);;
 850
 851
 852
 853
 854
 855
 856
 857 let disjoint_fan2=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
 858 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E) /\ ~(w=w1)
 859 ==>
 860  w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
 861  w_dart_fan x V E (x,v,w1,(sigma_fan x V E v w1))={}`,
 862 REPEAT STRIP_TAC    THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w1:real^3)`] properties_of_set_of_edge_fan)
 863   THEN ASM_REWRITE_TAC[] THEN
 864 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] ORBITS_EQ_SET_EDGE_FAN)
 865   THEN ASM_REWRITE_TAC[] THEN
 866 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] SIMP_ORBITS_POINTS_FAN)
 867   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])THEN DISCH_TAC
 868 THEN POP_ASSUM(fun th->GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[th])
 869   THEN REWRITE_TAC[IN_ELIM_THM;] THEN STRIP_TAC
 870   THEN ASM_REWRITE_TAC[]
 871 THEN DISJ_CASES_TAC(ARITH_RULE`(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))>1 \/ ~((CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))> 1)`)
 872 THENL(*1*)[
 873  MP_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) V E)>1==> 0< CARD(set_of_edge v V E)`) THEN ASM_REWRITE_TAC[]
 874    THEN DISCH_TAC THEN
 875   MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`0:num`] w_dart_eq_wedge3_fan)
 876   THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 877    THEN
 878   MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`i:num`] w_dart_eq_wedge3_fan)
 879   THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC THEN ASM_REWRITE_TAC[wedge3_fan;INTER]
 880    THEN POP_ASSUM(fun th -> REWRITE_TAC[])
 881    THEN POP_ASSUM(fun th -> REWRITE_TAC[])
 882    THEN POP_ASSUM MP_TAC
 883    THEN POP_ASSUM MP_TAC
 884    THEN POP_ASSUM MP_TAC THEN DISJ_CASES_TAC(ARITH_RULE`i:num =0 \/ SUC(0) <= i`)
 885 THENL(*2*)[
 886 ASM_REWRITE_TAC[power_map_points];(*2*)
 887
 888 DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[if_azims_fan] THEN
 889 MP_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) V E)>1==> ~(SUC 0= CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 890    THEN DISCH_TAC THEN
 891 MP_TAC(ARITH_RULE`i<CARD(set_of_edge (v:real^3) V E)==> ~(i= CARD(set_of_edge v V E))`) THEN ASM_REWRITE_TAC[]
 892    THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 893   THEN MP_TAC(ARITH_RULE`SUC 0<= i ==> i:num = SUC 0 \/ SUC(0) < i`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 894 THENL(*3*)[
 895 ASM_REWRITE_TAC[EMPTY;EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN REAL_ARITH_TAC;(*3*)
 896
 897  MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;` (v:real^3)`] remark1_fan)
 898   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 899 DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) V E ={w} \/ ~(set_of_edge (v:real^3) V E ={w})`)
 900 THENL(*4*)[
 901 MP_TAC(ISPECL[`w:real^3`;`set_of_edge (v:real^3) V E`]CARD_SING) THEN ASM_REWRITE_TAC[] THEN
 902 POP_ASSUM(fun th->REWRITE_TAC[SYM(th)]) THEN REPEAT(POP_ASSUM MP_TAC) THEN ARITH_TAC;(*4*)
 903
 904 MP_TAC(ISPECL[`i:num`;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`SUC (0):num`]  AZIM_LE_POWER_SIGMA_FAN)
 905   THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[EMPTY;EXTENSION;IN_ELIM_THM]  THEN REAL_ARITH_TAC]]];
 906
 907 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN DISCH_TAC THEN
 908 MP_TAC(ARITH_RULE`~(CARD(set_of_edge (v:real^3) V E)>1) /\ (i < CARD(set_of_edge v V E))
 909 ==> (i:num =0)`) THEN ASM_REWRITE_TAC[]
 910      THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[power_map_points]]);;
 911
 912
 913 let disjoint_fan3=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3).
 914 FAN(x,V,E)/\ ({v,w}IN E)
 915 ==>aff{x,v} INTER aff_gt {x,v} {w}={}`,
 916 REPEAT STRIP_TAC THEN  MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;` (v:real^3)`] remark1_fan)
 917 THEN ASM_REWRITE_TAC[]  THEN DISCH_TAC
 918   THEN DISJ_CASES_TAC(SET_RULE`aff{(x:real^3),(v:real^3)} INTER aff_gt {x,v} {(w:real^3)}={} \/ (?(u:real^3). u IN aff{x,v} INTER aff_gt {x,v} {w})`)
 919   THENL[
 920 ASM_SET_TAC[];
 921
 922 POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC
 923 THEN
 924                 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GT_2_1)
 925                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 926                   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`]affine_hull_2_fan)
 927                 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"a") THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM;]
 928   THEN STRIP_TAC
 929 THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1 % x + t2 % v = t1' % x + t2' % v + t3 % w <=>  t3 % w = (t1 - t1') % x +  (t2 -t2') % v`]
 930   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 931   THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM(th);REAL_ARITH`a+b+c=d+e <=>  c = (d-a)+ (e-b)`])
 932 THEN DISCH_TAC THEN MP_TAC(REAL_ARITH`&0 < (t3:real) ==> ~(t3= &0)`)
 933     THEN ASM_REWRITE_TAC[]THEN DISCH_TAC
 934   THEN MP_TAC(ISPEC`t3:real`REAL_MUL_LINV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 935   THEN  DISCH_TAC
 936   THEN MP_TAC(SET_RULE` (t3:real) = (t1- t1') + (t2-t2') ==> (inv t3) *(t3:real) = (inv t3) * ((t1- t1')+ (t2-t2'))`)
 937  THEN ASM_REWRITE_TAC[REAL_ARITH`a*(b+c)= a *b + a*c`] THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
 938   THEN DISCH_TAC THEN DISCH_TAC
 939  THEN MP_TAC(SET_RULE` (t3:real) % w= (t1- t1') % (x:real^3) + (t2-t2') % v ==> (inv t3) % ((t3:real)% w) = (inv t3) % ((t1- t1') %x+ (t2-t2') % v)`)
 940 THEN ASM_REWRITE_TAC[VECTOR_ARITH`m% (n% p)=a%(b % x + c % v)<=> (m*n) %p = (a *b)%x + (a*c)% v`]
 941 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
 942   THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(SYM(th))) THEN REWRITE_TAC[VECTOR_ARITH`&1 %w=w`]
 943   THEN DISCH_TAC
 944   THEN SUBGOAL_THEN`w IN aff{(x:real^3),v}` ASSUME_TAC
 945 THENL[
 946 REMOVE_THEN"a"(fun th-> REWRITE_TAC[th;IN_ELIM_THM]) THEN EXISTS_TAC`inv t3 * (t1-t1')` THEN EXISTS_TAC`inv t3 * (t2-t2')`
 947   THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
 948   THEN POP_ASSUM(fun th-> REWRITE_TAC[th]);
 949 ASM_SET_TAC[]]]);;
 950
 951
 952
 953
 954
 955 let remark3_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
 956 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E) /\ ~(w=w1)
 957 ==>
 958  aff_gt{x,v} {w} INTER
 959  aff_gt {x,v} {w1}={}`,
 960 REPEAT STRIP_TAC    THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w1:real^3)`] properties_of_set_of_edge_fan)
 961   THEN ASM_REWRITE_TAC[] THEN
 962 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] ORBITS_EQ_SET_EDGE_FAN)
 963   THEN ASM_REWRITE_TAC[] THEN
 964 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`] SIMP_ORBITS_POINTS_FAN)
 965   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])THEN DISCH_TAC
 966 THEN POP_ASSUM(fun th->GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[th])
 967   THEN REWRITE_TAC[IN_ELIM_THM;] THEN STRIP_TAC
 968   THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN  DISJ_CASES_TAC(ARITH_RULE`i:num =0 \/ 0 < i`)
 969 THENL[
 970 ASM_REWRITE_TAC[power_map_points];
 971
 972  MP_TAC(ARITH_RULE`i<CARD(set_of_edge (v:real^3) V E)/\ (0<i)==> ~(i= CARD(set_of_edge v V E)) /\ ~(0=CARD(set_of_edge (v:real^3) V E))`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 973   THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`i:num`] wedge_fan2_equal_aff_gt_fan)
 974    THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`0:num`] wedge_fan2_equal_aff_gt_fan)
 975    THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC THEN DISCH_TAC
 976    THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
 977    THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
 978
 979    THEN ASM_REWRITE_TAC[wedge2_fan;if_azims_fan;power_map_points;INTER;IN_ELIM_THM;AZIM_REFL;]
 980    THEN DISCH_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
 981  THEN DISJ_CASES_TAC(REAL_ARITH`azim x v w w1 = &0 \/ ~(azim x v w w1 = &0)`)
 982 THENL[
 983  MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w:real^3)`;`w1:real^3`] UNIQUE_AZIM_0_POINT_FAN)
 984    THEN ASM_REWRITE_TAC[];
 985 ASM_REWRITE_TAC[EMPTY;EXTENSION;IN_ELIM_THM] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]]);;
 986
 987
 988 let VBTIKLP=prove(`(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (u:real^3).
 989 FAN(x,V,E)/\ ({v,u}IN E)
 990 ==>
 991  (UNIV:real^3->bool) = aff {x,v} UNION (UNIONS {w_dart_fan x V E (x,v,w,(sigma_fan x V E v w))|w| {v,w} IN E })
 992 UNION
 993  (UNIONS {aff_gt {x,v} {w} |w| {v,w} IN E} ))
 994 /\
 995 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3).
 996 FAN(x,V,E)/\ ({v,w}IN E)
 997 ==>
 998  w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER aff {x,v}={})
 999 /\
1000 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
1001 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E)
1002 ==>
1003  w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
1004  (aff_gt {x,v} {w1})={})
1005 /\
1006 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
1007 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E) /\ ~(w=w1)
1008 ==>
1009  w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
1010  w_dart_fan x V E (x,v,w1,(sigma_fan x V E v w1))={})
1011 /\
1012 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
1013 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E) /\ ~(w=w1)
1014 ==>
1015  aff_gt{x,v} {w} INTER
1016  aff_gt {x,v} {w1}={})
1017 /\ (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3).
1018 FAN(x,V,E)/\ ({v,w}IN E)
1019 ==>aff{x,v} INTER aff_gt {x,v} {w}={})
1020 `,
1021 MESON_TAC[UNION1_FAN;disjoint_set_fan;disjoint_fan1;disjoint_fan2;remark3_fan;disjoint_fan3]);;
1022
1023
1024
1025 end;;