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




module  Lead_fan = struct



open Sphere;;
open Fan_defs;;
open Hypermap_of_fan;;
open Tactic_fan;;
open Lemma_fan;;		
open Fan;;
open Hypermap_of_fan;;
open Node_fan;;
open Azim_node;;
open Sum_azim_node;;
open Disjoint_fan;;

(* ========================================================================== *)
(*                   DISJOINT IN   FAN                        *) 
(* ========================================================================== *)




let exist_fan=
prove(`(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3). FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E ==> ?h:real. (&0 < h) /\ (!y1:real^3 y2:real^3. (y1 IN aff_ge {x} {v} INTER ballnorm_fan x) /\ y2 IN (aff_ge {x} {v1, w1} INTER ballnorm_fan x) ==> h <= dist(y1,y2) ))`,
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) THEN RES_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`; ` (v1:real^3)`] remark1_fan) THEN RES_TAC THEN MATCH_MP_TAC( ISPECL [`aff_ge {(x:real^3)} {(v:real^3)} INTER ballnorm_fan x`; `aff_ge {(x:real^3)} {(v1:real^3), (w1:real^3)} INTER ballnorm_fan x`] SEPARATE_CLOSED_COMPACT) THEN MP_TAC(ISPECL[`(x:real^3) `;` (v:real^3)`;` (w:real^3)`]closed_point_fan) THEN RESA_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;` (v1:real^3)`;` (w1:real^3)`]compact_aff_ge_ballnorm_fan) THEN RESA_TAC THEN FIND_ASSUM(MP_TAC)`FAN(x:real^3,V,E)` THEN REWRITE_TAC[FAN;fan7] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPECL[`{(v:real^3)}`;`{(v1:real^3),(w1:real^3)}`]th)) THEN ASM_REWRITE_TAC[UNION; IN_ELIM_THM;] THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[EXTENSION;] THEN ASM_REWRITE_TAC[IN_SING; SET_RULE`(!x. x = v <=> x = v') <=> v =v'`;SET_RULE`(?v'. v' IN V /\ v = v')<=> v IN V`] THEN SUBGOAL_THEN `{v:real^3} INTER {v1,w1} ={}` ASSUME_TAC THENL[ REWRITE_TAC[INTER;IN_SING; EXTENSION; EMPTY; IN_ELIM_THM] THEN ASM_SET_TAC[]; ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; SET_RULE`(A INTER C) INTER (B INTER C)= (A INTER B) INTER C`;] THEN ASSUME_TAC(AFFINE_SING) THEN MP_TAC(ISPEC`{ (x:real^3) }` AFFINE_HULL_EQ ) THEN RESA_TAC THEN RESA_TAC THEN REWRITE_TAC[ballnorm_fan;INTER; IN_SING; EXTENSION;EMPTY;IN_ELIM_THM; ] THEN GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[DIST_REFL ] THEN REAL_ARITH_TAC]);;
let ballsets_fan=new_definition`ballsets_fan (s:real^3->bool) (h:real)= {y:real^3| ?x:real^3. dist(x,y) < h /\ x IN s} `;;
let exists_ballsets_fan =
prove( `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3). FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E ==> ?h:real. (&0 < h) /\ (ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h INTER (aff_ge {x} {v1, w1} INTER ballnorm_fan x) = {}) )`,
REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (v1:real^3)`;` (w1:real^3)`] exist_fan) THEN RES_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ballsets_fan; INTER; IN_ELIM_THM] THEN DISCH_TAC THEN EXISTS_TAC`h:real` THEN ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;] THEN GEN_TAC THEN EQ_TAC THENL[ POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN STRIP_TAC THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPECL[`x'':real^3`;`x':real^3`]th)) THEN ASM_REWRITE_TAC[EMPTY;IN_ELIM_THM] THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; REWRITE_TAC[EMPTY;IN_ELIM_THM]]);;
(*-------------------------------------------------------------------------------------------*) (* cone_ge_fan_inter_aff_ge_is_empty *) (*-------------------------------------------------------------------------------------------*)
let cone_ge_fan=new_definition`cone_ge_fan (x:real^3) (s:real^3->bool)= {y:real^3| ?a:real z:real^3. (&0 <= a)/\(z IN s) /\ (y =a % (z - x) + x)}`;;
let cone_ge_fan_inter_aff_ge_is_empty=
prove( `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3). FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E ==> ?h:real. (h > &0) /\ (cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} = {x}) )`,
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) THEN RES_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`; `(v1:real^3)`] remark1_fan) THEN RES_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`; `(w:real^3)`;` (v1:real^3)`;` (w1:real^3)`] exists_ballsets_fan) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THENL(*1*)[ ASM_REWRITE_TAC[REAL_ARITH`a> &0 <=> &0< a`];(*1*) REWRITE_TAC [cone_ge_fan; EXTENSION; IN_SING; INTER; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THENL(*2*)[ ASM_CASES_TAC `(x':real^3)=(x:real^3)` THENL(*3*)[ASM_REWRITE_TAC[];(*3*) MP_TAC (ISPECL [`x':real^3`; `x:real^3`] imp_norm_not_zero_fan) THEN RES_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ABBREV_TAC `(x1:real^3)= inv (norm ((x':real^3)-(x:real^3))) % (x'-x) + x` THEN SUBGOAL_THEN `(x1:real^3) IN ballnorm_fan (x:real^3)` ASSUME_TAC THENL(*4*)[ REWRITE_TAC[ballnorm_fan; IN_ELIM_THM] THEN EXPAND_TAC "x1" THEN REWRITE_TAC[dist] THEN REWRITE_TAC[VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --(a)`; VECTOR_ARITH `-- ((a:real)% (v:real^3))=(-- a) % v`; NORM_MUL;REAL_ABS_NEG; REAL_ABS_INV; REAL_ABS_NORM] THEN USE_THEN "a" MP_TAC THEN MP_TAC(ISPEC `norm ((x':real^3)-(x:real^3))` REAL_MUL_LINV) THEN ASM_MESON_TAC[];(*4*) SUBGOAL_THEN `(x1:real^3) IN aff_ge {(x:real^3)} {(v1:real^3),(w1:real^3)}` ASSUME_TAC THENL(*5*)[REMOVE_THEN "a" MP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v1:real^3`;`w1:real^3`]AFF_GE_1_2) THEN RESA_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC `&1 - inv (norm((x':real^3)-(x:real^3))) + inv (norm (x' - x)) * (t1:real) ` THEN EXISTS_TAC `inv (norm((x':real^3)-(x:real^3))) * (t2:real) ` THEN EXISTS_TAC `inv (norm((x':real^3)-(x:real^3))) * (t3:real) ` THEN EXPAND_TAC "x1" THEN REWRITE_TAC[VECTOR_ARITH`((a:real)-(b:real)+(c:real))%(v:real^3)=(a:real) % v -(b:real)% v+(c:real) %(v:real^3)`; VECTOR_ARITH `&1 % (x:real^3)=x`; VECTOR_ARITH `((a:real)*(b:real)) % (v:real^3)= (a % (b % v))`; VECTOR_ARITH `(x - inv (norm (x' - x)) % x + inv (norm (x' - x)) % t1 % x) + inv (norm (x' - x)) % t2 % v1 + inv (norm (x' - x)) % t3 % w1 =(inv (norm ((x':real^3)- x))) % ( t1 % x + t2 % v1+ t3% w1 -x)+ (x:real^3)` ] THEN STRIP_TAC THENL(*6*)[SUBGOAL_THEN `&0 <= inv (norm ((x':real^3)-(x:real^3))) ` ASSUME_TAC THENL(*7*)[ MATCH_MP_TAC REAL_LE_INV THEN MESON_TAC[NORM_POS_LE];(*7*) ASM_MESON_TAC[REAL_LE_MUL]](*7*);(*6*) STRIP_TAC THENL(*7*)[ SUBGOAL_THEN `&0 <= inv (norm ((x':real^3)-(x:real^3))) ` ASSUME_TAC THENL(*8*)[ MATCH_MP_TAC REAL_LE_INV THEN MESON_TAC[NORM_POS_LE];(*8*) ASM_MESON_TAC[REAL_LE_MUL; REAL_ARITH `(a:real)>= &0 <=> &0 <= a`]](*8*);(*7*) REWRITE_TAC[REAL_ARITH `(&1 - inv (norm (x' - x)) + inv (norm (x' - x)) * t1) + inv (norm (x' - x)) * t2 + inv (norm (x' - x)) * t3= &1 - inv (norm (x' - x)) + inv (norm (x' - x)) * (t1 + t2 + t3)`] THEN STRIP_TAC THENL(*8*)[ ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `(a:real) * &1 = a`; REAL_ARITH `&1 - (a:real) +(a:real) = &1`];(*8*) SUBGOAL_THEN `(x':real^3) -(x:real^3)= (t1:real) % (x:real^3) + (t2:real) % (v1:real^3) + (t3:real) % (w1:real^3) -(x:real^3)` ASSUME_TAC THENL(*9*)[ ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC;(*9*) SUBGOAL_THEN `inv (norm ((x':real^3) -(x:real^3)) ) % ((x':real^3) -(x:real^3)) = inv (norm ((x':real^3) -(x:real^3)) ) % ((t1:real) % (x:real^3) + (t2:real) % (v1:real^3) + (t3:real) % (w1:real^3) -(x:real^3))` ASSUME_TAC THENL(*10*)[ASM_MESON_TAC[ VECTOR_MUL_LCANCEL ];(*10*) ASM_MESON_TAC[]](*10*)](*9*)](*8*)](*7*)](*6*); (*5*) SUBGOAL_THEN `(x1:real^3) IN ballsets_fan (aff_ge {(x:real^3)} {(v:real^3)} INTER ballnorm_fan x) (h:real)` ASSUME_TAC THENL(*6*)[ SUBGOAL_THEN `norm ((z:real^3)-(x:real^3))= &1` ASSUME_TAC THENL(*7*)[FIND_ASSUM(MP_TAC)`z IN ballnorm_fan (x:real^3)` THEN REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; NORM_SUB];(*7*) POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "k") THEN SUBGOAL_THEN `(x':real^3)- (x:real^3)= (a:real) % ((z:real^3)-x )` ASSUME_TAC THENL(*8*)[ FIND_ASSUM(MP_TAC)`x'=a %(z-x) +x:real^3` THEN VECTOR_ARITH_TAC;(*8*) SUBGOAL_THEN `norm((x':real^3)- (x:real^3))= norm((a:real) % ((z:real^3)-x ))` ASSUME_TAC THENL(*9*)[ASM_SET_TAC[];(*9*) POP_ASSUM MP_TAC THEN REWRITE_TAC[NORM_MUL] THEN POP_ASSUM MP_TAC THEN USE_THEN "k" (fun th -> REWRITE_TAC[th]) THEN REDUCE_ARITH_TAC THEN SUBGOAL_THEN `abs (a:real)=a`ASSUME_TAC THENL(*10*)[FIND_ASSUM(MP_TAC)`&0 <= a:real` THEN REAL_ARITH_TAC;(*10*) POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN DISCH_THEN(LABEL_TAC"l") THEN DISCH_THEN (LABEL_TAC "n") THEN REMOVE_THEN "l" MP_TAC THEN USE_THEN "n" (fun th-> REWRITE_TAC[SYM th]) THEN DISCH_THEN (LABEL_TAC "l") THEN SUBGOAL_THEN `(inv (norm (x'- x))) % ((x':real^3)- (x:real^3)) = (inv (norm (x' - x))) % (norm (x' - x) % ((z:real^3)- x ))` ASSUME_TAC THENL(*11*)[POP_ASSUM MP_TAC THEN MESON_TAC[];(*11*) POP_ASSUM MP_TAC THEN REWRITE_TAC[VECTOR_ARITH `(a:real)%(b:real)%(v:real^3)=(a*b)%v`] THEN MP_TAC(ISPEC`norm((x':real^3)-(x:real^3))`REAL_MUL_LINV) THEN FIND_ASSUM(fun th ->REWRITE_TAC[th]) `~(norm((x':real^3)-(x:real^3))= &0)` THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN REDUCE_VECTOR_TAC THEN REWRITE_TAC[VECTOR_ARITH `((a:real^3)=(z:real^3)-(x:real^3))<=>(a+x=z)`] THEN FIND_ASSUM(fun th-> REWRITE_TAC[th])`inv (norm (x' - x)) % (x' - x) + x = x1:real^3` THEN DISCH_TAC THEN ASM_REWRITE_TAC[INTER]](*11*)](*10*)](*9*)](*8*)](*7*);(*6*) ASM_SET_TAC[]](*6*)](*5*)](*4*)](*3*);(*2*) STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL(*2*)[ EXISTS_TAC `&0` THEN EXISTS_TAC`inv (norm ((v:real^3)-(x:real^3))) % (v-x) + x` THEN REDUCE_VECTOR_TAC THEN STRIP_TAC THENL(*3*)[ REAL_ARITH_TAC;(*3*) STRIP_TAC THENL(*4*)[ REWRITE_TAC[ballsets_fan; IN_ELIM_THM] THEN EXISTS_TAC `inv(norm((v:real^3)-(x:real^3))) % (v-x)+x` THEN REWRITE_TAC[dist; VECTOR_ARITH `(a)-a= vec 0`; NORM_0] THEN STRIP_TAC THENL(*5*)[ ASM_SET_TAC[];(*5*) STRIP_TAC THENL(*6*)[ MP_TAC(ISPECL[`x:real^3`;`v:real^3`]AFF_GE_1_1) THEN RESA_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&1 - inv (norm ((v:real^3)-(x:real^3)))` THEN EXISTS_TAC `inv (norm ((v:real^3)-(x:real^3)))` THEN STRIP_TAC THENL(*7*)[ MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan) THEN RES_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*7*) STRIP_TAC THENL(*8*)[ REAL_ARITH_TAC;(*8*) VECTOR_ARITH_TAC](*8*)](*7*);(*6*) REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ] THEN SUBGOAL_THEN `inv(norm((v:real^3)-(x:real^3))) > &0 ` ASSUME_TAC THENL(*7*)[MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_gl_zero_fan) THEN RESA_TAC;(*7*) SUBGOAL_THEN `abs(inv(norm((v:real^3)-(x:real^3))))=inv(norm((v:real^3)-(x:real^3)))` ASSUME_TAC THENL(*8*)[ASM_REWRITE_TAC[REAL_ABS_REFL] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*8*) POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN SUBGOAL_THEN `~ (norm ((v:real^3)-(x:real^3))= &0)` ASSUME_TAC THENL(*9*)[MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_not_zero_fan) THEN RESA_TAC;(*9*) POP_ASSUM MP_TAC THEN MESON_TAC[REAL_MUL_RINV;REAL_MUL_SYM]](*9*)](*8*)](*7*)](*6*)](*5*);(*4*) REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ] THEN SUBGOAL_THEN `inv(norm((v:real^3)-(x:real^3))) > &0 ` ASSUME_TAC THENL(*5*)[ MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_gl_zero_fan) THEN RESA_TAC;(*5*) SUBGOAL_THEN `abs(inv(norm((v:real^3)-(x:real^3))))=inv(norm((v:real^3)-(x:real^3)))` ASSUME_TAC THENL(*6*)[ASM_REWRITE_TAC[REAL_ABS_REFL] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*6*) POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN SUBGOAL_THEN `~ (norm ((v:real^3)-(x:real^3))= &0)` ASSUME_TAC THENL(*7*)[ MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_not_zero_fan) THEN RESA_TAC;(*7*) POP_ASSUM MP_TAC THEN MESON_TAC[REAL_MUL_RINV;REAL_MUL_SYM]](*7*)](*6*)](*5*)](*4*)](*3*);(*2*) MP_TAC(ISPECL[`x:real^3`;`v1:real^3`;`w1:real^3`]AFF_GE_1_2) THEN RESA_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [REAL_ARITH_TAC; STRIP_TAC THENL [REAL_ARITH_TAC; STRIP_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]]]]]]);;
let subset_by_inequality_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3) (h:real) (h1:real). FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E /\ h < h1 ==> cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} SUBSET cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h1)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} `,
REPEAT STRIP_TAC THEN SUBGOAL_THEN` cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x) SUBSET cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h1)INTER ballnorm_fan x ) ` ASSUME_TAC THENL[ REWRITE_TAC[cone_ge_fan; SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC`a:real` THEN EXISTS_TAC`z:real^3` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ballsets_fan;INTER; IN_ELIM_THM] THEN RESA_TAC THEN EXISTS_TAC`x'':real^3` THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; ASM_SET_TAC[]]);;
let cone_ge_fan_inter_aff_ge_is_empty_fan=
prove( `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3). FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E ==> ?h:real. (&1> h) /\ (h > &0) /\ (cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} SUBSET {x}) )`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `; `(w:real^3) `;`(v1:real^3)`;` (w1:real^3)`]cone_ge_fan_inter_aff_ge_is_empty) THEN RESA_TAC THEN DISJ_CASES_TAC(REAL_ARITH `(h >= &1) \/ (&1 > h)` ) THENL[ MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `; `(w:real^3) `;`(v1:real^3)`;` (w1:real^3)`; `&1/ &2`; `(h:real)`]subset_by_inequality_fan) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(REAL_ARITH`h>= &1==> &1 / &2 <h`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN EXISTS_TAC `&1/ &2` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; EXISTS_TAC `h:real` THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]]);;
let rcone_subset_cone=
prove( `!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) h:real. FAN(x,V,E) /\ {v,w} IN E /\(&0< h) /\ (h< &1) ==> ?h1:real. &1 > h1 /\ h1> &0 /\ (rcone_fan x v h1) SUBSET cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x )`,
REWRITE_TAC[rcone_fan;cone_ge_fan; SUBSET;IN_ELIM_THM;dist] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`(&2 -(h:real) pow 2)/ &2` THEN STRIP_TAC THENL[ REWRITE_TAC[REAL_ARITH`&1 > (&2 -(h:real) pow 2)/ &2 <=> h pow 2> &0`] THEN MP_TAC (ISPECL[`h:real`;`2`]REAL_POW_LT) THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; STRIP_TAC THENL[ REWRITE_TAC[REAL_ARITH`(&2 -h pow 2)/ &2> &0<=> &2 > h pow 2`] THEN MATCH_MP_TAC(REAL_ARITH` h pow 2<= &1 ==> &2 > h pow 2`) THEN MATCH_MP_TAC (ISPECL[`2`;`h:real`;]REAL_POW_1_LE) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; REPEAT STRIP_TAC THEN EXISTS_TAC `norm ((x':real^3)-(x:real^3))` THEN EXISTS_TAC `inv(norm ((x':real^3)-(x:real^3)))%(x'-x)+x` THEN REWRITE_TAC[NORM_POS_LE] THEN POP_ASSUM MP_TAC THEN DISJ_CASES_TAC(SET_RULE`((x':real^3)-(x:real^3)= vec 0) \/ ~((x':real^3)-(x:real^3)= vec 0)`) THENL(*1*)[ ASM_REWRITE_TAC[NORM_0;DOT_LZERO;] THEN REDUCE_ARITH_TAC THEN REAL_ARITH_TAC;(*1*) REWRITE_TAC[VECTOR_ARITH`(A+B)-B=A:real^3`;VECTOR_MUL_ASSOC] THEN MP_TAC(ISPEC`x':real^3- x`NORM_EQ_0) THEN RESA_TAC THEN MP_TAC(ISPEC`norm(x':real^3- x)`REAL_MUL_LINV) THEN ASM_REWRITE_TAC[REAL_MUL_SYM] THEN RESA_TAC THEN REDUCE_VECTOR_TAC THEN REWRITE_TAC[VECTOR_ARITH`A-B+B=A:real^3`] THEN SUBGOAL_THEN` inv (norm (x' - x)) % (x' - x) + x IN ballnorm_fan (x:real^3)` ASSUME_TAC THENL(*2*)[ REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ] THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]imp_norm_ge_zero_fan) THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`(a:real^3)=b <=> a - b = vec 0`] THEN RESA_TAC THEN MP_TAC(ISPEC`inv(norm((x':real^3)-(x:real^3)))`REAL_ABS_REFL) THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`&0<= (a:real) <=> a >= &0`] THEN RESA_TAC;(*2*) STRIP_TAC THEN SUBGOAL_THEN` inv (norm (x' - x)) % (x' - x) + x IN ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan (x:real^3)) (h:real)` ASSUME_TAC THENL(*3*)[ REWRITE_TAC[ballsets_fan;IN_ELIM_THM;dist] THEN EXISTS_TAC`inv (norm (v - x)) % (v - x) + (x:real^3)` THEN STRIP_TAC THENL(*4*)[ REWRITE_TAC[VECTOR_ARITH`((v:real^3)+b)-(u+b)= (v-u)`;] THEN SUBGOAL_THEN`norm(inv(norm(v-x))%(v:real^3-x)-inv(norm(x'-x))%(x'-x)) pow 2< h pow 2` ASSUME_TAC THENL(*5*)[ REWRITE_TAC[NORM_POW_2;DOT_LSUB;DOT_RSUB] THEN REWRITE_TAC[DOT_RMUL;DOT_LMUL;DOT_SQUARE_NORM; REAL_ARITH`a-b-(c-d)=a+d-b-c`; REAL_ARITH`a*a*b pow 2=(a*b) pow 2`;DOT_SYM;REAL_ARITH`a+b-e*d*c-d*e*c=a+b- &2 * d*e *c`] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(w:real^3)`; `(v:real^3)`;] remark1_fan) THEN RES_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3)`;] imp_norm_not_zero_fan) THEN REWRITE_TAC[NORM_SUB] THEN RES_TAC THEN MP_TAC(ISPEC`norm(v:real^3- x)`REAL_MUL_LINV) THEN RES_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`&1 pow 2= &1`; REAL_ARITH`&1+ &1 - &2 * a< h pow 2 <=> a > (&2- h pow 2)/ &2`] THEN MP_TAC (ISPEC `(v:real^3)-(x:real^3)` NORM_POS_LE) THEN DISCH_TAC THEN SUBGOAL_THEN `norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC THENL(*6*)[ REPEAT( POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*) MP_TAC (ISPEC `(x':real^3)-(x:real^3)` NORM_POS_LE) THEN DISCH_TAC THEN SUBGOAL_THEN ` norm((x:real^3)-(x':real^3))> &0 ` ASSUME_TAC THENL(*7*)[ ONCE_REWRITE_TAC[NORM_ARITH`norm (x:real^3- x')> &0 <=> norm(x'-x)> &0`] THEN REPEAT( POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*7*) MP_TAC(ISPECL[`(&2 - (h:real) pow 2) / &2`; `inv (norm (x:real^3 - x')) * inv (norm (v - x)) * ((v - x) dot (x' - x))`; `norm (x:real^3 - x')`]REAL_LT_LMUL_EQ) THEN REWRITE_TAC[REAL_ARITH`a<b <=> b>a`] THEN POP_ASSUM(fun th->REWRITE_TAC[th]) THEN POP_ASSUM(fun th->REWRITE_TAC[]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`(A<=>B)<=>(B<=>A)`] THEN DISCH_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[th]) THEN MP_TAC(ISPECL[`norm (x:real^3 - x') * (&2 - (h:real) pow 2) / &2`; `norm (x:real^3 - x')*inv (norm (x:real^3 - x')) * inv (norm (v - x)) * ((v - x) dot (x' - x))`; `norm (v:real^3 - x)`]REAL_LT_LMUL_EQ) THEN REWRITE_TAC[REAL_ARITH`a<b <=> b>a`] THEN POP_ASSUM(fun th->REWRITE_TAC[th]) THEN POP_ASSUM(fun th->REWRITE_TAC[]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`(A<=>B)<=>(B<=>A)`] THEN DISCH_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C*D*E>a*b*c<=>(C*B)*(D*A)*E>b*c*a`] THEN ONCE_REWRITE_TAC[NORM_ARITH`norm (x:real^3- x')= norm(x'-x)`] THEN ASM_REWRITE_TAC[] THEN REDUCE_ARITH_TAC THEN GEN_REWRITE_TAC(RAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[NORM_SUB] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DOT_SYM] THEN ASM_REWRITE_TAC[]](*7*)](*6*)(*5*); ASM_REWRITE_TAC[NORM_LT_SQUARE;DOT_SQUARE_NORM]](*5*);(*4*) MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(w:real^3)`; `(v:real^3)`;] remark1_fan) THEN RES_TAC THEN SUBGOAL_THEN`inv(norm(v-x:real^3)) % (v-x) +x IN aff_ge {x} {v}` ASSUME_TAC THENL(*5*)[ MP_TAC(ISPECL[`x:real^3`;`v:real^3`]AFF_GE_1_1) THEN RESA_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&1 - inv (norm ((v:real^3)-(x:real^3)))` THEN EXISTS_TAC `inv (norm ((v:real^3)-(x:real^3)))` THEN STRIP_TAC THENL(*6*)[ MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan) THEN RES_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*6*) STRIP_TAC THENL(*7*)[ REAL_ARITH_TAC; VECTOR_ARITH_TAC]](*6*);(*5*) SUBGOAL_THEN` inv (norm (v- x)) % (v - x) + x IN ballnorm_fan (x:real^3)` ASSUME_TAC THENL(*6*)[ REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ] THEN MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan) THEN ASM_REWRITE_TAC[VECTOR_ARITH`v-x=vec 0<=> v=x`] THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`(a:real^3)=b <=> a - b = vec 0`] THEN RESA_TAC THEN MP_TAC(ISPEC`inv(norm((v:real^3)-(x:real^3)))`REAL_ABS_REFL) THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`&0<= (a:real) <=> a >= &0`] THEN RESA_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3)`;] imp_norm_not_zero_fan) THEN REWRITE_TAC[NORM_SUB] THEN RES_TAC THEN MP_TAC(ISPEC`norm(v:real^3- x)`REAL_MUL_LINV) THEN RES_TAC THEN ASM_REWRITE_TAC[];(*6*) ASM_SET_TAC[]](*6*)](*5*)](*4*);(*3*) ASM_SET_TAC[]]]]]]);;
let inter_is_empty=
prove(` !(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3). FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E ==> ?h1:real. &1 > h1 /\ h1> &0 /\ rcone_fan x v h1 INTER aff_ge {x} {v1, w1} = {} `,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3) ` ;`(w:real^3)`;` (v1:real^3) `;`(w1:real^3)`]cone_ge_fan_inter_aff_ge_is_empty_fan) THEN RESA_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool) `;`(v:real^3)`; `(w:real^3)`;` h:real`]rcone_subset_cone) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_ARITH`&0<h<=> h> &0`; REAL_ARITH`h< &1 <=> &1 >h`] THEN RES_TAC THEN SUBGOAL_THEN`(rcone_fan x v h1 INTER aff_ge {x} {v1, w1}) SUBSET {x:real^3}` ASSUME_TAC THENL[ ASM_SET_TAC[]; MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (h1:real)`]origin_not_in_rcone_fan) THEN REPEAT STRIP_TAC THEN EXISTS_TAC`h1:real` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET; IN_SING;EXTENSION;EMPTY] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN REMOVE_THEN "a" (fun th->MP_TAC(ISPEC`x':real^3`th)) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN`x:real^3 IN rcone_fan x v h1` ASSUME_TAC THENL[ASM_SET_TAC[]; ASM_SET_TAC[]]; ASM_SET_TAC[]]]);;
let avoids_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3)(w2:real^3). FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E ==> ?h:real. &1 >h /\ h> &0 /\ rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),(w2:real^3)) h INTER aff_ge {x} {v1, w1} = {} `,
REPEAT STRIP_TAC THEN REWRITE_TAC[rw_dart_fan] THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (v1:real^3)` ;`(w1:real^3)`]inter_is_empty) THEN RESA_TAC THEN EXISTS_TAC`h1:real` THEN ASM_SET_TAC[] );;
let avoids1_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (w1:real^3). FAN(x,V,E) /\ {v,w} IN E /\ {v,w1} IN E ==> ?h:real. &1 > h /\ h > &0 /\ rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER aff_ge {x} {v, w1} = {}`,
REPEAT STRIP_TAC THEN REWRITE_TAC[rw_dart_fan] THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`; ` (w:real^3)`;`(w1:real^3)`]IBZWFFH) THEN RESA_TAC THEN EXISTS_TAC`&1/ &2` THEN REWRITE_TAC[REAL_ARITH`&1/ &2 > &0`;REAL_ARITH`&1 > &1/ &2`] THEN ASM_SET_TAC[]);;
let finish_avoids_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3). FAN(x,V,E) /\ {v,w} IN E /\ {v1,w1} IN E ==> ?h:real. &1 >h /\ h> &0/\ rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER aff_ge {x} {v1, w1} = {}`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~(v:real^3 IN {v1,w1})\/ (v=v1\/ v=w1)`) THENL[ MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`(v1:real^3)`;`w1:real^3`;` (sigma_fan x V E v w:real^3)`]avoids_fan) THEN RESA_TAC THEN ASM_SET_TAC[]; POP_ASSUM MP_TAC THEN STRIP_TAC THENL[ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"A") THEN DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN POP_ASSUM( fun th-> REWRITE_TAC[SYM(th)]) THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`w1:real^3`]avoids1_fan) THEN RESA_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"A") THEN DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN POP_ASSUM( fun th-> REWRITE_TAC[SYM(th)]) THEN ONCE_REWRITE_TAC[SET_RULE`{X,Y}={Y,X}`] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`v1:real^3`]avoids1_fan) THEN RESA_TAC]]);;
let continuous_set_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (h:real) (h1:real). FAN(x,V,E) /\ {v,w} IN E /\ h1 <= h ==> rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h SUBSET rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h1`,
REPEAT STRIP_TAC THEN REWRITE_TAC[rw_dart_fan] THEN SUBGOAL_THEN `rcone_fan x v h SUBSET rcone_fan x v h1` ASSUME_TAC THENL[ REWRITE_TAC[rcone_fan;SUBSET; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE) THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE) THEN MP_TAC(ISPECL[`dist((v:real^3),x)`;`h1:real`;`h:real`] REAL_LE_LMUL) THEN RESA_TAC THEN MP_TAC(ISPECL[`dist((x':real^3),x)`;`dist((v:real^3),x)* (h1:real)`;`dist((v:real^3),x)* (h:real)`] REAL_LE_LMUL) THEN RESA_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; ASM_SET_TAC[]]);;
let finish_avoids1_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (E':(real^3->bool)->bool) (v:real^3) (w:real^3). FAN(x,V,E) /\ {v,w} IN E /\ E' SUBSET E ==> ?h:real. &1> h /\ h> &0 /\ rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER {v | ?e. e IN E' /\ v IN aff_ge {x} e}={}`,
REPEAT STRIP_TAC THEN REWRITE_TAC[xfan; IN_ELIM_THM] THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]set_edges_is_finite_fan) THEN RESA_TAC THEN MP_TAC(ISPECL [`(E':(real^3->bool)->bool)`;`(E:(real^3->bool)->bool)`] FINITE_SUBSET) THEN RESA_TAC THEN ABBREV_TAC`n=CARD (E':(real^3->bool)->bool)` THEN REPEAT(POP_ASSUM MP_TAC) THEN SPEC_TAC (`(E':(real^3->bool)->bool)`,`(E':(real^3->bool)->bool)`) THEN SPEC_TAC (`n:num`,`n:num`) THEN INDUCT_TAC THENL(*1*)[ REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`E':(real^3->bool)->bool`]CARD_EQ_0) THEN RESA_TAC THEN EXISTS_TAC`&1 / &2` THEN REWRITE_TAC[REAL_ARITH`&1/ &2 > &0`;REAL_ARITH`&1 > &1/ &2`] THEN ASM_SET_TAC[];(*1*) REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT STRIP_TAC THEN MP_TAC(ISPEC`(E':(real^3->bool)->bool)` CHOOSE_SUBSET) THEN RESA_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`n:num `th)) THEN REWRITE_TAC[ARITH_RULE `n:num <= SUC n`; HAS_SIZE] THEN STRIP_TAC THEN MP_TAC(SET_RULE` t SUBSET E' /\ E' SUBSET E ==> (t:(real^3->bool)->bool) SUBSET E`) THEN RESA_TAC THEN REMOVE_THEN "A" (fun th-> MP_TAC(ISPEC`(t:(real^3->bool)->bool)`th)) THEN RESA_TAC THEN SUBGOAL_THEN `~((E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)= {})` ASSUME_TAC THENL(*2*)[ STRIP_TAC THEN MP_TAC(SET_RULE`(E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)={} /\ t SUBSET E' ==> t= E'`) THEN RESA_TAC THEN FIND_ASSUM MP_TAC`CARD (t:(real^3->bool)->bool)=n` THEN POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;(*2*) SUBGOAL_THEN`?e. e IN (E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)` ASSUME_TAC THENL(*3*)[ ASM_SET_TAC[];(*3*) POP_ASSUM MP_TAC THEN STRIP_TAC THEN MP_TAC(SET_RULE`e IN (E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)/\ (E':(real^3->bool)->bool) SUBSET (E:(real^3->bool)->bool) /\ t SUBSET E' ==> e IN E'/\ e IN E/\ ~(e IN t) /\ {e} UNION t SUBSET E'`) THEN RESA_TAC THEN MP_TAC(ISPECL [`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;`(E':(real^3->bool)->bool)`] FINITE_SUBSET) THEN RESA_TAC THEN ASSUME_TAC(SET_RULE`e IN {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`) THEN MP_TAC(ISPECL[`e:real^3->bool`;`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;]CARD_DELETE) THEN RESA_TAC THEN MP_TAC(SET_RULE `e IN {e:(real^3->bool)} UNION (t:(real^3->bool)->bool) ==> ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e PSUBSET {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`) THEN RESA_TAC THEN MP_TAC(ISPECL[`({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))DELETE e`;`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`]CARD_PSUBSET) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN FIND_ASSUM MP_TAC`FINITE ( {e:(real^3->bool)} UNION (t:(real^3->bool)->bool))` THEN DISCH_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN DISCH_TAC THEN MP_TAC(ARITH_RULE`CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) < CARD ( {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) /\ CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) = CARD ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))-1 <=>CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) +1= CARD ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))`) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;]) THEN REWRITE_TAC[ARITH_RULE`A=A`; ] THEN MP_TAC(SET_RULE`~(e IN t)==>({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e=t`) THEN RESA_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN FIND_ASSUM MP_TAC`(CARD (E':(real^3->bool)->bool)=SUC n)` THEN REWRITE_TAC[ARITH_RULE`SUC n=(n:num) +1`] THEN DISCH_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)]) THEN DISCH_TAC THEN MP_TAC(ISPECL[`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;`E':(real^3->bool)->bool`]CARD_SUBSET_EQ) THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)]) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"MA") THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(e:real^3->bool)`]expand_edge_graph_fan) THEN RESA_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3)`;`(w:real^3)`; `(v':real^3)`;` (w':real^3)`]finish_avoids_fan) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th)) THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN STRIP_TAC THEN ABBREV_TAC`h1= max (h:real) (h':real)` THEN EXISTS_TAC`h1:real` THEN STRIP_TAC THENL(*4*)[ POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]) THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*4*) STRIP_TAC THENL(*5*)[ POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]) THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*5*) REMOVE_THEN "MA" MP_TAC THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th)) THEN REWRITE_TAC[UNION;IN_ELIM_THM;EXTENSION; INTER;] THEN GEN_TAC THEN EQ_TAC THENL(*6*)[ ASM_REWRITE_TAC[IN_SING] THEN STRIP_TAC THENL[ POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)` ;`(h1:real)`;` (h':real)`]continuous_set_fan) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN EXPAND_TAC"h1" THEN REWRITE_TAC[REAL_ARITH`h'<= max (h:real) (h':real)`] THEN RESA_TAC THEN ASM_SET_TAC[]; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)` ;`(h1:real)`;` (h:real)`]continuous_set_fan) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN EXPAND_TAC"h1" THEN REWRITE_TAC[REAL_ARITH`h<= max (h:real) (h':real)`] THEN RESA_TAC THEN ASM_SET_TAC[]]; ASM_SET_TAC[]]]]]]]);;
let rw_dart_avoids_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3). FAN(x,V,E) /\ {v,w} IN E ==> ?h:real. &1> h /\ h> &0 /\ rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h SUBSET yfan(x,V,E) `,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]finish_avoids1_fan) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`A SUBSET A`;yfan;xfan] THEN RESA_TAC THEN EXISTS_TAC`h:real` THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);;
(*------------------------------------------------------------------------*) (*------------------------------------------------------------------------*)
let r_fan=new_definition`r_fan (a:real) (b:real) (c:real) = { y:real^3 | y$1 > &0  /\  y$2 > a  /\ y$2 < b /\ y$3 > &0 /\ y$3 < c}`;;
let r1_le_fan=new_definition`r1_le_fan (a:real)={ y:real^3 | y$1 > a}`;;
let r2_le_fan=new_definition`r2_le_fan (a:real)={ y:real^3 |  y$2 > a}`;;
let r3_le_fan=new_definition`r3_le_fan (a:real)={ y:real^3 | y$3 > a}`;;
let r1_ge_fan=new_definition`r1_ge_fan (a:real)={ y:real^3 |  y$1 < a}`;;
let r2_ge_fan=new_definition`r2_ge_fan (a:real)={ y:real^3 |  y$2 < a}`;;
let r3_ge_fan=new_definition`r3_ge_fan (a:real)={ y:real^3 |  y$3 < a}`;;
let r_fan_is_inter_halfspace=
prove(`!a:real b:real c:real. r_fan a b c = r1_le_fan (&0) INTER r2_le_fan a INTER r2_ge_fan b INTER r3_le_fan (&0) INTER r3_ge_fan c`,
let r1_ge_is_convex_fan = 
prove(`!a:real. convex (r1_ge_fan a)/\ open (r1_ge_fan a) `,
let r2_ge_is_convex_fan = 
prove(`!a:real. convex (r2_ge_fan a)/\ open (r2_ge_fan a)`,
let r3_ge_is_convex_fan = 
prove(`!a:real. convex (r3_ge_fan a) /\ open(r3_ge_fan a)`,
let r1_le_is_convex_fan = 
prove(`!a:real. convex (r1_le_fan a)/\ open (r1_le_fan a) `,
let r2_le_is_convex_fan = 
prove(`!a:real. convex (r2_le_fan a)/\ open (r2_le_fan a) `,
let r3_le_is_convex_fan = 
prove(`!a:real. convex (r3_le_fan a)/\ open (r3_le_fan a) `,
let r_is_connected_fan=
prove(`!a:real b:real c:real. connected (r_fan a b c)/\convex (r_fan a b c) /\ open (r_fan a b c)`,
(
let lemma = prove(`!a:real b:real c:real. convex (r_fan a b c)/\ open (r_fan a b c)`,
ASSUME_TAC (r_fan_is_inter_halfspace) THEN ASM_REWRITE_TAC[] THEN
ASSUME_TAC (r1_ge_is_convex_fan) THEN ASSUME_TAC ( r2_ge_is_convex_fan) THEN
ASSUME_TAC (r3_ge_is_convex_fan) THEN ASSUME_TAC(r1_le_is_convex_fan) THEN
ASSUME_TAC(r2_le_is_convex_fan) THEN ASSUME_TAC( r3_le_is_convex_fan) THEN
ASM_MESON_TAC[CONVEX_INTER;OPEN_INTER]) 
    in
SUBGOAL_THEN `!a:real b:real c:real. convex (r_fan a b c)/\ open (r_fan a b c) ` ASSUME_TAC 
THENL [MESON_TAC[lemma];
       ASM_MESON_TAC[CONVEX_CONNECTED]]));;
let rw_dart_is_image_set_spherical_coordinate=
prove(`(!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 h:real. FAN(x,V,E)/\ {v,u} IN E/\ &0 <h /\ h< pi/ &2 ==> IMAGE (change_spherical_coordinate_fan x v u) (r_fan (azim x v u u) (azim_fan x V E v u) h)= rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))) `,
(
let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,ASM_SET_TAC[]) in
( let lem1=prove(`!x v u. {x,v,u}= {v,x,u}`,SET_TAC[]) in

REWRITE_TAC[azim_fan;r_fan; rw_dart_fan; change_spherical_coordinate_fan;IMAGE;INTER;
w_dart_fan;rcone_fan;EXTENSION;IN_ELIM_THM]
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) 
THEN REPEAT STRIP_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 RESA_TAC
THEN FIND_ASSUM MP_TAC`~collinear {(x:real^3),(v:real^3),(u:real^3)}`
THEN GEN_REWRITE_TAC( LAND_CONV  o ONCE_DEPTH_CONV)[lem1]
THEN ONCE_REWRITE_TAC[COLLINEAR_3]
THEN RESA_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]orthonormal_e1_e2_e3_fan)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th))
THEN REWRITE_TAC[orthonormal]
THEN STRIP_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate)
THEN RESA_TAC
THEN EQ_TAC
THENL(*1*)[
STRIP_TAC
THEN MP_TAC(ISPEC`(x'':real^3)$3`SIN_POS_PI2)
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`A /\ B <=> B /\ A`]
THEN STRIP_TAC
THENL(*2*)[




REWRITE_TAC[dist;vector_norm;VECTOR_ARITH`(A+B)-A=(B:real^3)`; DOT_LADD;DOT_RADD;DOT_RMUL;DOT_LMUL;]
THEN ONCE_REWRITE_TAC[DOT_SYM]
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN ONCE_REWRITE_TAC[DOT_SYM]
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN REWRITE_TAC[REAL_ARITH`((x'':real^3)$1 * cos (x''$2) * sin (x''$3)) * x''$1 * cos (x''$2) * sin (x''$3) +
  (x''$1 * sin (x''$2) * sin (x''$3)) * x''$1 * sin (x''$2) * sin (x''$3) +
  (x''$1 * cos (x''$3)) * x''$1 * cos (x''$3)=(x''$1 * x''$1)* (( sin (x''$2) pow 2 +(cos (x''$2) pow 2)) * (sin (x''$3) pow 2)+ cos (x''$3) pow 2)`]
THEN ASSUME_TAC(ISPEC`(x'':real^3)$2`SIN_CIRCLE)
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN ASSUME_TAC(ISPEC`(x'':real^3)$3`SIN_CIRCLE)
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN MP_TAC(ISPEC`(x'':real^3)$1`SQRT_POW_2)
THEN MP_TAC(REAL_ARITH`(x'':real^3)$1> &0==> &0 <= (x'':real^3)$1`)
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ISPECL[`(x'':real^3)$1`;`(x'':real^3)$1`]SQRT_MUL)
THEN RESA_TAC
THEN REWRITE_TAC[REAL_ARITH`A*(A:real)=A pow 2`]
THEN ASM_REWRITE_TAC[e3_fan;DOT_LMUL]
THEN ONCE_REWRITE_TAC[GSYM vector_norm;]
THEN ASSUME_TAC(ISPEC`(v:real^3)-(x:real^3)`DOT_SQUARE_NORM)
THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN REWRITE_TAC[REAL_ARITH`(A*B)*C *D pow 2=A*D*B *(C*D)`]
THEN SUBGOAL_THEN`~(norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
THENL(*3*)[

ASM_REWRITE_TAC[NORM_EQ_0;VECTOR_ARITH`v-x=vec 0<=> x=v`];(*3*)	

MP_TAC(ISPEC`norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN MP_TAC(ISPEC`((v:real^3)-(x:real^3))`NORM_POS_LT)
THEN ASM_REWRITE_TAC[VECTOR_ARITH`v-x=vec 0<=> x=v`;REAL_ARITH`A>B<=> B<A`]
THEN DISCH_TAC
THEN MATCH_MP_TAC REAL_LT_LMUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0 < A<=> A> &0`]
THEN MATCH_MP_TAC REAL_LT_LMUL
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC COS_MONO_LT
THEN REPEAT(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC];(*2*)



SUBGOAL_THEN`azim (x:real^3) (v:real^3) (u:real^3)
 (x +
  (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
  (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
  (x''$1 * cos (x''$3)) % e3_fan x v u)= (x'':real^3)$2 ` ASSUME_TAC
THENL(*3*)[

MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x +
  (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
  (x''$1 * sin (x''$2) * sin ((x'':real^3)$3)) % e2_fan x v u +
  (x''$1 * cos (x''$3)) % e3_fan (x:real^3) (v:real^3) (u:real^3))`;
  `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
  `(x''$1 * cos ((x'':real^3)$3)) * (inv (norm((v:real^3)-(x:real^3))))`;
`((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;
`x''$1 * sin ((x'':real^3)$3)`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`(x'':real^3)$2`]AZIM_UNIQUE)
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;]
THEN STRIP_TAC
THENL(*4*)[

MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;]AZIM_REFL)
THEN REPEAT(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;(*4*)

STRIP_TAC
THENL(*5*)[

MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`] azim)
THEN REPEAT(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;(*5*)

STRIP_TAC
THENL(*6*)[

MATCH_MP_TAC REAL_LT_MUL
THEN REPEAT(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;(*6*)

STRIP_TAC
THENL(*7*)[

REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN ONCE_REWRITE_TAC[GSYM e3_fan]
THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
 ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
THEN REDUCE_ARITH_TAC
THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
THEN REDUCE_VECTOR_TAC
THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[e1_fan]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
THEN ONCE_REWRITE_TAC[DOT_SYM]
THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
THEN ONCE_REWRITE_TAC[GSYM e2_fan]
THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN REWRITE_TAC[DOT_RZERO]
THEN REAL_ARITH_TAC;(*7*)

REWRITE_TAC[e3_fan]
THEN VECTOR_ARITH_TAC](*7*)](*6*)](*5*)](*4*);(*3*)




SUBGOAL_THEN`~collinear
  {(x:real^3), (v:real^3), x +
         (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v (u:real^3) +
         (x''$1 * sin (x''$2) * sin ((x'':real^3)$3)) % e2_fan x v u +
         (x''$1 * cos (x''$3)) % e3_fan x v u}`ASSUME_TAC
THENL(*4*)[

ONCE_REWRITE_TAC[lem]
THEN REWRITE_TAC[collinear1_fan]
THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2; IN_ELIM_THM; REAL_ARITH`A+B= &1<=>A= &1-B`]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN REWRITE_TAC[VECTOR_ARITH`A+B=(&1-c) % A+ c % D<=>B=c%(D-A)`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`((x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
      (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
      (x''$1 * cos ((x'':real^3)$3)) % e3_fan x v (u:real^3)) dot e1_fan x v u =
      ((v':real) % ((v:real^3) - (x:real^3))) dot e1_fan x v u` ASSUME_TAC
THENL(*5*)[
ASM_REWRITE_TAC[];(*5*)

POP_ASSUM MP_TAC
THEN REWRITE_TAC[DOT_LADD;DOT_LMUL]
THEN ASM_REWRITE_TAC[DOT_SYM]
THEN REDUCE_ARITH_TAC
THEN SUBGOAL_THEN`((x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
      (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
      (x''$1 * cos ((x'':real^3)$3)) % e3_fan x v (u:real^3)) dot e2_fan x v u =
      ((v':real) % ((v:real^3) - (x:real^3))) dot e2_fan x v u` ASSUME_TAC
THENL(*6*)[
ASM_REWRITE_TAC[];(*6*)

POP_ASSUM MP_TAC
THEN REWRITE_TAC[DOT_LADD;DOT_LMUL]
THEN ASM_REWRITE_TAC[DOT_SYM]
THEN REDUCE_ARITH_TAC
THEN REWRITE_TAC[REAL_ENTIRE]
THEN STRIP_TAC
THENL(*7*)[

REPEAT (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;(*7*)

STRIP_TAC
THENL(*8*)[

REPEAT (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;(*8*)


MP_TAC(ISPEC`(x'':real^3)$2`SIN_CIRCLE)
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;

REPEAT (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC];

REPEAT (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC](*7*)](*6*)](*5*);(*4*)


REPEAT(POP_ASSUM MP_TAC)
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)`)
THENL(*5*)[
ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[wedge;IN_ELIM_THM]
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN ASM_REWRITE_TAC[]
THEN FIND_ASSUM MP_TAC`(x'':real^3)$2 > azim (x:real^3) (v:real^3) u (u:real^3)`
THEN REWRITE_TAC[AZIM_REFL]
THEN REAL_ARITH_TAC;(*5*)

	
ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
THEN MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]one_edge_fan)
THEN RESA_TAC
THEN REWRITE_TAC[DIFF;IN_ELIM_THM]
THEN STRIP_TAC
THENL(*6*)[

ASM_SET_TAC[];(*6*)

STRIP_TAC
THEN  MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x:real^3) +
  (x''$1 * cos (x''$2) * sin ((x'':real^3)$3)) % e1_fan x (v:real^3) (u:real^3) +
  (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
  (x''$1 * cos (x''$3)) % e3_fan x v u`]AZIM_EQ_0_GE_ALT)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;]AZIM_REFL)
THEN REPEAT(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC](*6*)](*5*)](*4*)](*3*)](*2*);(*1*)



ONCE_REWRITE_TAC[GSYM EXTENSION]
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)`)
THENL(*2*)[
ASM_REWRITE_TAC[wedge;IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC 
THEN DISCH_THEN(LABEL_TAC"A")
THEN EXISTS_TAC`vector[(dist((x:real^3),(x':real^3)));(azim (x:real^3) (v:real^3) (u:real^3) (x':real^3));(arcV (x:real^3) (x':real^3) (v:real^3))]:real^3`
THEN ASM_REWRITE_TAC[VECTOR_3;AZIM_REFL;REAL_ARITH`A> &0 <=> &0 <A`]
THEN SUBGOAL_THEN `~((x:real^3)=(x':real^3))` ASSUME_TAC
THENL(*3*)[


 STRIP_TAC
THEN REMOVE_THEN "A" MP_TAC
THEN ASM_REWRITE_TAC[DIST_REFL;VECTOR_ARITH`A-A= vec 0`;DOT_LZERO]
THEN REDUCE_ARITH_TAC
THEN REAL_ARITH_TAC;(*3*)


MP_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_EQ_0)
THEN RESA_TAC
THEN ASSUME_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_POS_LE)
THEN MP_TAC(REAL_ARITH`~(dist((x:real^3),(x':real^3))= &0)/\ &0 <= dist((x:real^3),(x':real^3))==> &0 < dist((x:real^3),(x':real^3))`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THENL(*4*)[
STRIP_TAC
THENL(*5*)[

REWRITE_TAC[ARCV_ANGLE; angle;]
THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]VECTOR_ANGLE_RANGE)
THEN STRIP_TAC
THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]COLLINEAR_VECTOR_ANGLE)
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-B= vec 0<=> B=A`;]
THEN ONCE_REWRITE_TAC[GSYM COLLINEAR_3;]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]
THEN DISCH_TAC
THEN FIND_ASSUM MP_TAC `~collinear {(x:real^3),(v:real^3),(x':real^3)}`
THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN REWRITE_TAC[DE_MORGAN_THM]
THEN REPEAT(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;(*5*)

MP_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_EQ_0)
THEN RESA_TAC
THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE)
THEN MP_TAC(REAL_ARITH`~(dist((v:real^3),(x:real^3))= &0)/\ &0 <= dist((v:real^3),(x:real^3))==> &0 < dist((v:real^3),(x:real^3))`)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_EQ_0)
THEN RESA_TAC
THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE)
THEN MP_TAC(REAL_ARITH`~(dist((x':real^3),(x:real^3))= &0)/\ &0 <= dist((x':real^3),(x:real^3))==> &0 < dist((x':real^3),(x:real^3))`)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`dist ((v:real^3),(x:real^3)) * cos (h:real)`;`((x':real^3) - x) dot ((v:real^3) - (x:real^3))`; `dist((x':real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3)) )/ dist ((x':real^3),(x:real^3)) `; `dist((v:real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[REAL_ARITH`(A*B)*C =C* A*B`]
THEN REWRITE_TAC[REAL_ARITH`A<B <=> B>A`;]
THEN ASM_REWRITE_TAC[real_div;REAL_ARITH`(A*B)*C =A*(B *C)`]
THEN ONCE_REWRITE_TAC[GSYM REAL_INV_MUL;]
THEN ONCE_REWRITE_TAC[GSYM real_div;]
THEN REWRITE_TAC[dist;arcV]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0 < (h:real) /\ h< pi/ &2==> &0<= h /\ h<=pi`)
THEN RESA_TAC
THEN MP_TAC(ISPEC`h:real`ACS_COS)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3))) / (norm (x' - x) * norm (v - x))` ;]ACS_MONO_LT)
THEN RESA_TAC
THEN REWRITE_TAC[REAL_ARITH`A>B<=> B<A`]
THEN POP_ASSUM MATCH_MP_TAC
THEN REWRITE_TAC[COS_BOUNDS]
THEN ASM_REWRITE_TAC[REAL_ARITH`A<B<=> B>A`]
THEN MP_TAC(ISPECL[`(x':real^3)-(x:real^3)`;`(v:real^3)-(x:real^3)`]NORM_CAUCHY_SCHWARZ_DIV)
THEN MP_TAC(ISPEC`(((x':real^3)-(x:real^3)) dot ((v:real^3)-(x:real^3))) / (norm (x' - x) * norm (v - x))`REAL_ABS_LE)
THEN REAL_ARITH_TAC](*5*);(*4*)


MATCH_MP_TAC(ISPECL[`u:real^3`;`x:real^3`;`v:real^3`;`x':real^3`;`e1_fan (x:real^3) (v:real^3) (u:real^3)`;
`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`dist((x:real^3),(x':real^3))`;`arcV (x:real^3) (x':real^3) (v:real^3)`;`azim (x:real^3) (v:real^3) (u:real^3) (x':real^3)`]SPHERICAL_COORDINATES)
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`azim x v u (x+e1_fan (x:real^3) (v:real^3) (u:real^3))= &0` ASSUME_TAC
THENL(*5*)[

MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`;
  `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
  `&0`;
`((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;`&1`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`&0`]AZIM_UNIQUE)
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;REAL_ARITH`&0<= &0/\ &0 < &1`]
THEN STRIP_TAC
THENL(*6*)[
MP_TAC(PI_WORKS)
THEN REAL_ARITH_TAC;(*6*)

STRIP_TAC
THENL(*7*)[

REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN ONCE_REWRITE_TAC[GSYM e3_fan]
THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
 ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
THEN REDUCE_ARITH_TAC
THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
THEN REDUCE_VECTOR_TAC
THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[e1_fan]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
THEN ONCE_REWRITE_TAC[DOT_SYM]
THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
THEN ONCE_REWRITE_TAC[GSYM e2_fan]
THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN REWRITE_TAC[DOT_RZERO]
THEN REAL_ARITH_TAC;(*7*)

REWRITE_TAC[SIN_0;COS_0]
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN VECTOR_ARITH_TAC](*7*)](*6*);(*5*)


MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`]AZIM_EQ_0_ALT)
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN ONCE_REWRITE_TAC[COLLINEAR_3]
THEN REWRITE_TAC[ VECTOR_ARITH`((A:real^3)+(B:real^3))-A=B`;]
THEN ONCE_REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL]
THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2= &0`;REAL_ARITH `A=B:real <=> B=A`]
THEN REDUCE_ARITH_TAC
THEN ASM_REWRITE_TAC[DOT_EQ_0;VECTOR_ARITH`A-B=vec 0<=> A=B:real^3`]](*5*)](*4*)](*3*);(*2*)







ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
THEN MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]one_edge_fan)
THEN RESA_TAC
THEN REWRITE_TAC[DIFF;IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC 
THEN DISCH_THEN(LABEL_TAC"A")
THEN EXISTS_TAC`vector[(dist((x:real^3),(x':real^3)));(azim (x:real^3) (v:real^3) (u:real^3) (x':real^3));(arcV (x:real^3) (x':real^3) (v:real^3))]:real^3`
THEN ASM_REWRITE_TAC[VECTOR_3;AZIM_REFL;REAL_ARITH`A> &0 <=> &0 <A`]
THEN SUBGOAL_THEN `~((x:real^3)=(x':real^3))` ASSUME_TAC
THENL(*3*)[

STRIP_TAC
THEN REMOVE_THEN "A" MP_TAC
THEN ASM_REWRITE_TAC[DIST_REFL;VECTOR_ARITH`A-A= vec 0`;DOT_LZERO]
THEN REDUCE_ARITH_TAC
THEN REAL_ARITH_TAC;(*3*)

MP_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_EQ_0)
THEN RESA_TAC
THEN ASSUME_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_POS_LE)
THEN MP_TAC(REAL_ARITH`~(dist((x:real^3),(x':real^3))= &0)/\ &0 <= dist((x:real^3),(x':real^3))==> &0 < dist((x:real^3),(x':real^3))`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[azim]
THEN SUBGOAL_THEN`~collinear{(x:real^3),(v:real^3),(x':real^3)}` ASSUME_TAC
THENL(*4*)[

POP_ASSUM (fun th-> REWRITE_TAC[])
THEN POP_ASSUM (fun th-> REWRITE_TAC[])
THEN POP_ASSUM (fun th-> REWRITE_TAC[])
THEN POP_ASSUM (fun th-> REWRITE_TAC[])
THEN POP_ASSUM (fun th-> REWRITE_TAC[])
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"MA")
THEN ONCE_REWRITE_TAC[lem1]
THEN ASM_REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA;VECTOR_ARITH`v-x=vec 0<=> v=x`]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]AFF_GE_2_1)
THEN RESA_TAC
THEN STRIP_TAC
THENL(*5*)[

REMOVE_THEN "MA" MP_TAC
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`&1`
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&0`
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN REAL_ARITH_TAC;(*5*)

REMOVE_THEN "MA" MP_TAC
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`&1- (c:real)`
THEN EXISTS_TAC`c:real`
THEN EXISTS_TAC`&0`
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(x':real^3)=(&1 - (c:real)) % (x:real^3)+ c % (v:real^3)<=>x'-x=c%(v-x)`]
THEN REAL_ARITH_TAC](*5*);(*4*)



STRIP_TAC
THENL(*5*)[
STRIP_TAC
THENL(*6*)[

MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`]AZIM_EQ_0_GE_ALT)
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`]azim)
THEN REAL_ARITH_TAC;(*6*)


STRIP_TAC
THENL(*7*)[

REWRITE_TAC[ARCV_ANGLE; angle;]
THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]VECTOR_ANGLE_RANGE)
THEN STRIP_TAC
THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]COLLINEAR_VECTOR_ANGLE)
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-B= vec 0<=> B=A`;]
THEN ONCE_REWRITE_TAC[GSYM COLLINEAR_3;]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]
THEN DISCH_TAC
THEN FIND_ASSUM MP_TAC `~collinear {(x:real^3),(v:real^3),(x':real^3)}`
THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN REWRITE_TAC[DE_MORGAN_THM]
THEN REPEAT(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;(*7*)

MP_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_EQ_0)
THEN RESA_TAC
THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE)
THEN MP_TAC(REAL_ARITH`~(dist((v:real^3),(x:real^3))= &0)/\ &0 <= dist((v:real^3),(x:real^3))==> &0 < dist((v:real^3),(x:real^3))`)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_EQ_0)
THEN RESA_TAC
THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE)
THEN MP_TAC(REAL_ARITH`~(dist((x':real^3),(x:real^3))= &0)/\ &0 <= dist((x':real^3),(x:real^3))==> &0 < dist((x':real^3),(x:real^3))`)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`dist ((v:real^3),(x:real^3)) * cos (h:real)`;`((x':real^3) - x) dot ((v:real^3) - (x:real^3))`; `dist((x':real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3)) )/ dist ((x':real^3),(x:real^3)) `; `dist((v:real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[REAL_ARITH`(A*B)*C =C* A*B`]
THEN REWRITE_TAC[REAL_ARITH`A<B <=> B>A`;]
THEN ASM_REWRITE_TAC[real_div;REAL_ARITH`(A*B)*C =A*(B *C)`]
THEN ONCE_REWRITE_TAC[GSYM REAL_INV_MUL;]
THEN ONCE_REWRITE_TAC[GSYM real_div;]
THEN REWRITE_TAC[dist;arcV]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0 < (h:real) /\ h< pi/ &2==> &0<= h /\ h<=pi`)
THEN RESA_TAC
THEN MP_TAC(ISPEC`h:real`ACS_COS)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3))) / (norm (x' - x) * norm (v - x))` ;]ACS_MONO_LT)
THEN RESA_TAC
THEN REWRITE_TAC[REAL_ARITH`A>B<=> B<A`]
THEN POP_ASSUM MATCH_MP_TAC
THEN REWRITE_TAC[COS_BOUNDS]
THEN ASM_REWRITE_TAC[REAL_ARITH`A<B<=> B>A`]
THEN MP_TAC(ISPECL[`(x':real^3)-(x:real^3)`;`(v:real^3)-(x:real^3)`]NORM_CAUCHY_SCHWARZ_DIV)
THEN MP_TAC(ISPEC`(((x':real^3)-(x:real^3)) dot ((v:real^3)-(x:real^3))) / (norm (x' - x) * norm (v - x))`REAL_ABS_LE)
THEN REAL_ARITH_TAC](*7*)](*6*);(*5*)

MATCH_MP_TAC(ISPECL[`u:real^3`;`x:real^3`;`v:real^3`;`x':real^3`;`e1_fan (x:real^3) (v:real^3) (u:real^3)`;
`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`dist((x:real^3),(x':real^3))`;`arcV (x:real^3) (x':real^3) (v:real^3)`;`azim (x:real^3) (v:real^3) (u:real^3) (x':real^3)`]SPHERICAL_COORDINATES)
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`azim x v u (x+e1_fan (x:real^3) (v:real^3) (u:real^3))= &0` ASSUME_TAC
THENL(*6*)[

MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`;
  `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
  `&0`;
`((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;`&1`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`&0`]AZIM_UNIQUE)
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;REAL_ARITH`&0<= &0/\ &0 < &1`]
THEN STRIP_TAC
THENL(*7*)[
MP_TAC(PI_WORKS)
THEN REAL_ARITH_TAC;(*7*)

STRIP_TAC
THENL(*8*)[

REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN ONCE_REWRITE_TAC[GSYM e3_fan]
THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
 ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
THEN REDUCE_ARITH_TAC
THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
THEN REDUCE_VECTOR_TAC
THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[e1_fan]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
THEN ONCE_REWRITE_TAC[DOT_SYM]
THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
THEN ONCE_REWRITE_TAC[GSYM e2_fan]
THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN REWRITE_TAC[DOT_RZERO]
THEN REAL_ARITH_TAC;(*8*)

REWRITE_TAC[SIN_0;COS_0]
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN VECTOR_ARITH_TAC](*8*)](*7*);(*6*)


MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`]AZIM_EQ_0_ALT)
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN ONCE_REWRITE_TAC[COLLINEAR_3]
THEN REWRITE_TAC[ VECTOR_ARITH`((A:real^3)+(B:real^3))-A=B`;]
THEN ONCE_REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL]
THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2= &0`;REAL_ARITH `A=B:real <=> B=A`]
THEN REDUCE_ARITH_TAC
THEN ASM_REWRITE_TAC[DOT_EQ_0;VECTOR_ARITH`A-B=vec 0<=> A=B:real^3`]](*6*)](*5*)](*4*)](*3*)](*2*)](*1*))));;
let connected_rw_dart_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 h:real. FAN(x,V,E)/\ {v,u} IN E/\ &0 <h /\ h< pi/ &2 ==>connected(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h)))`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool) `;`v:real^3`; ` u:real^3` ;`h:real`]rw_dart_is_image_set_spherical_coordinate) THEN RESA_TAC THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC(ISPECL[`(azim (x:real^3) (v:real^3) (u:real^3) u)`; `(azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) `;`h:real`] r_is_connected_fan) THEN MP_TAC(ISPECL[`change_spherical_coordinate_fan (x:real^3) (v:real^3) (u:real^3)`;`r_fan (azim x v u u) (azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) (h:real)`]CONTINUOUS_ON_EQ_CONTINUOUS_AT) THEN RESA_TAC THEN MP_TAC(ISPECL[`change_spherical_coordinate_fan (x:real^3) (v:real^3) (u:real^3)`;`r_fan (azim x v u u) (azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) (h:real)`] CONNECTED_CONTINUOUS_IMAGE) THEN RESA_TAC THEN POP_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`; `u:real^3`;`x':real^3`]continuous_change_spherical_coordinate_fan) THEN REWRITE_TAC[change_spherical_coordinate_fan] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN DISCH_TAC THEN MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[CONTINUOUS_CONST]);;
let not_empty_rw_dart_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3. FAN(x,V,E)/\ {v,u} IN E ==> (!h:real. &0<h /\ h< pi/ &2 ==> ~(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))={}))`,
REPEAT STRIP_TAC THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`] THEN MRESA_TAC rw_dart_is_image_set_spherical_coordinate[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`h:real`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IMAGE_EQ_EMPTY;r_fan;EXTENSION;IN_ELIM_THM;IN;EMPTY;NOT_FORALL_THM;AZIM_REFL;azim_fan] THEN DISJ_CASES_TAC(ARITH_RULE`~(CARD (set_of_edge (v:real^3) V E) > 1)\/ CARD (set_of_edge v V E) > 1`) THENL[ ASM_REWRITE_TAC[] THEN EXISTS_TAC`vector[&1; pi; h/ &2]:real^3` THEN SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH] THEN MP_TAC PI_WORKS THEN ASM_TAC THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge v V E = {u:real^3})\/ ~(set_of_edge v V E = {u})`) THENL[ MRESA_TAC CARD_SING[`u:real^3`; `(set_of_edge v V E):real^3->bool`] THEN FIND_ASSUM MP_TAC `CARD ((set_of_edge v V E):real^3->bool) >1` THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun TH-> REWRITE_TAC[TH]) THEN ARITH_TAC; DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))= &0) \/ ~(azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) = &0)`) THENL[ MRESA_TAC SIGMA_FAN[`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(v:real^3)`;`(u:real^3)`] THEN MRESA_TAC UNIQUE_AZIM_0_POINT_FAN[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`] THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;`v:real^3`]; MRESA_TAC azim[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`] THEN EXISTS_TAC`vector[&1; (azim x v u ((sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))))/ &2;h/ &2]:real^3` THEN SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH] THEN ASM_TAC THEN REAL_ARITH_TAC]]]);;
let JGIYDLE=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3. FAN(x,V,E)/\ {v,u} IN E ==> (!h:real. &0<h /\ h< pi/ &2 ==> ~(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))={})) /\(!h:real h1:real. h1 <= h ==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h SUBSET rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h1)) /\ (?h:real. &1> h /\ h> &0 /\ rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h SUBSET yfan(x,V,E)) /\ (!h:real. &0 <h /\ h< pi/ &2 ==> connected(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))))`,
end;;