(* ========================================================================== *)
(* 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`,

REWRITE_TAC[r_fan; r1_le_fan; r2_le_fan; r2_ge_fan; r3_le_fan; r3_ge_fan; INTER; IN_ELIM_THM]);;
  

 

let r1_ge_is_convex_fan = 
prove(`!a:real. convex (r1_ge_fan a)/\ open (r1_ge_fan a) `,
REWRITE_TAC[r1_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;

let r2_ge_is_convex_fan = 
prove(`!a:real. convex (r2_ge_fan a)/\ open (r2_ge_fan a)`,

REWRITE_TAC[r2_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;
let r3_ge_is_convex_fan = 
prove(`!a:real. convex (r3_ge_fan a) /\ open(r3_ge_fan a)`,

REWRITE_TAC[r3_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;
let r1_le_is_convex_fan = 
prove(`!a:real. convex (r1_le_fan a)/\  open (r1_le_fan a) `,

REWRITE_TAC[r1_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
let r2_le_is_convex_fan = 
prove(`!a:real. convex (r2_le_fan a)/\ open (r2_le_fan a) `,

REWRITE_TAC[r2_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
let r3_le_is_convex_fan = 
prove(`!a:real. convex (r3_le_fan a)/\ open (r3_le_fan a) `,

REWRITE_TAC[r3_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
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))))`,

MESON_TAC[not_empty_rw_dart_fan;continuous_set_fan;rw_dart_avoids_fan;connected_rw_dart_fan]);;



end;;