HOL html


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



flyspeck_needs "general/sphere.hl";;


module Fan  = struct


(*
# use "/home/truong/Desktop/googlecode/hol_light/hol.ml";;
needs "/home/truong/Desktop/googlecode/hol_light/Multivariate/flyspeck.ml";;
needs "/home/truong/Desktop/googlecode/flyspeck/text_formalization/general/sphere.hl";;
*)

		
		
open Sphere;;
open Fan_defs;;
open Hypermap;;


let ASM_TAC=REPEAT(POP_ASSUM MP_TAC);;
let RED_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC;;
let RES_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC;;
let REDA_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[];;
let RESA_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[];;
let REDAL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN DISCH_TAC THEN ASM_REWRITE_TAC th;;
let RESAL_TAC (th: thm list) = ASM_REWRITE_TAC th THEN STRIP_TAC THEN ASM_REWRITE_TAC th;;
let REMOVE_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[]);;
let SYM_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]);;
let SYM_ASSUM1_TAC=POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(th));;
let RESP_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[th]);;
let RESPL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN STRIP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC [th]);;
let REDUCE_ARITH_TAC=REWRITE_TAC[REAL_ARITH`&0 * a= &0`; REAL_ARITH`a * &0 = &0`; REAL_ARITH`a + &0 = a`; 
REAL_ARITH`a- &0 =a`;REAL_ARITH`&0 +a =a`;REAL_ARITH`&1 * a =a`;REAL_ARITH`a * &1 =a`;REAL_ARITH`(A+B)-B=A`];;
let REDUCE_VECTOR_TAC=REWRITE_TAC[VECTOR_ARITH`&0 % a= vec 0`; VECTOR_ARITH`a % vec 0= vec 0`;VECTOR_ARITH`a + vec 0 = a`; 
VECTOR_ARITH`vec 0 +a =a`; VECTOR_ARITH`a- vec 0 =a`;VECTOR_ARITH`&1 % a =a`;VECTOR_ARITH`a- b =vec 0<=> a=b`];;

let MRESA_TAC th1 (th: term list) = MP_TAC(ISPECL th th1) THEN RESA_TAC;;
let MRESA1_TAC th1 th = MP_TAC(ISPEC th th1) THEN RESA_TAC;;

let MRESAL_TAC th1 (th: term list) (th2: thm list) =MP_TAC(ISPECL th th1) THEN ASM_REWRITE_TAC th2 THEN STRIP_TAC THEN ASM_REWRITE_TAC th2;;

let MRESAL1_TAC th1 th (th2: thm list) =MP_TAC(ISPEC th th1) THEN ASM_REWRITE_TAC th2 THEN STRIP_TAC THEN ASM_REWRITE_TAC th2;;

let ASM_SET_TAC l = 
    (TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ))) THEN SET_TAC l;;



let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
let fan1 = new_definition`fan1(x,V,E):bool <=>  FINITE V /\ ~(V SUBSET {}) `;;
let fan2 = new_definition`fan2(x,V,E):bool <=>   ~(x IN V)`;;
let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
let fan4 = new_definition`fan4(x,V,E):bool<=>  (!e. (e IN E) ==> (aff_gt {x} e  INTER V={}))`;;
let fan5 = new_definition`fan5(x,V,E):bool<=> (!e f. (e IN E)/\ (f IN E) /\ ~(e=f) ==> (aff_gt {x} e INTER aff_gt {x} f ={}))`;;
(* Deprecated, 2011-08-01, thales
let fan = new_definition`fan(x,V,E)<=>  ((UNIONS E) SUBSET V) /\ graph(E)/\ fan1(x,V,E)/\ fan2(x,V,E)/\ fan3(x,V,E)/\ fan4 (x,V,E) /\ fan5(x,V,E)`;;
*)

let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;
let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;

let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
let fan7= new_definition`fan7(x,V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;


let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
fan6(x,V,E)/\ fan7(x,V,E)`;;

(* ************************************************* *)
(* Invariance theorems *)

let GRAPH = prove
 (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
  REWRITE_TAC[graph; IN]);;
let CYCLIC_SET = prove
 (`cyclic_set W v w <=>
         ~(v = w) /\
         FINITE W /\
         (!p q h. p IN W /\ q IN W /\ p - q = h % (v - w) ==> p = q) /\
         W INTER affine hull {v, w} = {}`,
  REWRITE_TAC[cyclic_set; IN; VECTOR_ARITH `p - q:real^N = r <=> p = q + r`]);;
let CYCLIC_SET_TRANSLATION_EQ = prove
 (`!a:real^N s x y.
    cyclic_set (IMAGE (\x. a + x) s) (a + x) (a + y) <=> cyclic_set s x y`,
  REWRITE_TAC[CYCLIC_SET] THEN GEOM_TRANSLATE_TAC[]);;
let CYCLIC_SET_LINEAR_IMAGE = prove
 (`!f:real^M->real^N s x y.
        linear f /\ (!x y. f x = f y ==> x = y)
        ==> (cyclic_set (IMAGE f s) (f x) (f y) <=> cyclic_set s x y)`,
  GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
   [CYCLIC_SET; RIGHT_FORALL_IMP_THM; IMP_CONJ; FORALL_IN_IMAGE] THEN
  GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];;

add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;

let GRAPH_TRANSLATION_EQ = prove
 (`!a:real^N E. graph (IMAGE (IMAGE (\x. a + x)) E) <=> graph E`,
  REWRITE_TAC[GRAPH] THEN GEOM_TRANSLATE_TAC[]);;
let GRAPH_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (graph(IMAGE (IMAGE f) E) <=> graph E)`,
  REWRITE_TAC[GRAPH] THEN GEOM_TRANSFORM_TAC[]);;
let FAN1_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
        fan1(x,V,E)`,
  REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
let FAN1_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (fan1(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan1(x,V,E))`,
  REWRITE_TAC[fan1] THEN GEOM_TRANSFORM_TAC[]);;
let FAN2_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
        fan2(x,V,E)`,
  REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
let FAN2_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (fan2(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan2(x,V,E))`,
  REWRITE_TAC[fan2] THEN GEOM_TRANSFORM_TAC[]);;
let FAN3_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
        fan3(x,V,E)`,
  REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
let FAN3_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (fan3(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan3(x,V,E))`,
  let lemma = prove
   (`{w | {a,w} IN IMAGE (IMAGE f) s} =
     IMAGE f {w |w| {a,f w} IN IMAGE (IMAGE f) s}`,
    MATCH_MP_TAC(SET_RULE
     `(!y. P y ==> ?x. y = f x) ==> {w | P w} = IMAGE f {w | P(f w)}`) THEN
    REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
    MESON_TAC[]) in
  REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
let FAN4_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
        fan4(x,V,E)`,
  REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
let FAN4_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (fan4(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan4(x,V,E))`,
  REWRITE_TAC[fan4] THEN GEOM_TRANSFORM_TAC[]);;
let FAN5_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
        fan5(x,V,E)`,
  REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
let FAN5_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (fan5(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan5(x,V,E))`,
  GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
   [fan5; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
  GEOM_TRANSFORM_TAC[]);;
let FAN6_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
        fan6(x,V,E)`,
  REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
let FAN6_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (fan6(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan6(x,V,E))`,
  REWRITE_TAC[fan6] THEN GEOM_TRANSFORM_TAC[]);;
let FAN7_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
        fan7(x,V,E)`,
  REWRITE_TAC[fan7] THEN
  REWRITE_TAC[SET_RULE
   `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN
  GEOM_TRANSLATE_TAC[]);;
let FAN7_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (fan7(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan7(x,V,E))`,
  REWRITE_TAC[fan7; IN_UNION] THEN
  REWRITE_TAC[LEFT_OR_DISTRIB; RIGHT_OR_DISTRIB;
              TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
  GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
   [FORALL_AND_THM; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP] THEN
  GEOM_TRANSFORM_TAC[]);;
add_translation_invariants
 [GRAPH_TRANSLATION_EQ;
  FAN1_TRANSLATION_EQ;
  FAN2_TRANSLATION_EQ;
  FAN3_TRANSLATION_EQ;
  FAN4_TRANSLATION_EQ;
  FAN5_TRANSLATION_EQ;
  FAN6_TRANSLATION_EQ;
  FAN7_TRANSLATION_EQ];;

add_linear_invariants
 [GRAPH_LINEAR_IMAGE_EQ;
  FAN1_LINEAR_IMAGE_EQ;
  FAN2_LINEAR_IMAGE_EQ;
  FAN3_LINEAR_IMAGE_EQ;
  FAN4_LINEAR_IMAGE_EQ;
  FAN5_LINEAR_IMAGE_EQ;
  FAN6_LINEAR_IMAGE_EQ;
  FAN7_LINEAR_IMAGE_EQ];;

let FAN_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
        FAN(x,V,E)`,
  REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
let FAN_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
    linear f /\ (!x y. f x = f y ==> x = y)
    ==> (FAN(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> FAN(x,V,E))`,
  REWRITE_TAC[FAN] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [FAN_TRANSLATION_EQ];;
add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;

let BASE_POINT_FAN_TRANSLATION_EQ = prove
 (`!a x V E.
    base_point_fan(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) =
    a + base_point_fan(x,V,E)`,
  REWRITE_TAC[base_point_fan]);;
let BASE_POINT_FAN_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
        linear f
        ==> base_point_fan(f x,IMAGE f V,IMAGE (IMAGE f) E) =
            f(base_point_fan(x,V,E))`,
  REWRITE_TAC[base_point_fan]);;
let SET_OF_EDGE_TRANSLATION_EQ = prove
 (`!a:real^N x V E.
        set_of_edge (a + x) (IMAGE (\x. a + x) V)
                    (IMAGE (IMAGE (\x. a + x)) E) =
        IMAGE (\x. a + x) (set_of_edge x V E)`,
  REWRITE_TAC[set_of_edge] THEN GEOM_TRANSLATE_TAC[]);;
let SET_OF_EDGE_LINEAR_IMAGE_EQ = prove
 (`!f:real^M->real^N x V E.
        linear f /\ (!x y. f x = f y ==> x = y)
        ==> set_of_edge (f x) (IMAGE f V) (IMAGE (IMAGE f) E) =
            IMAGE f (set_of_edge x V E)`,
  let lemma = prove
   (`{w | {a,w} IN IMAGE (IMAGE f) s /\ P w} =
     {f w |w| {a,f w} IN IMAGE (IMAGE f) s /\ P(f w)}`,
    MATCH_MP_TAC(SET_RULE
     `(!y. P y ==> ?x. y = f x) ==> {w | P w} = {f w |w| P(f w)}`) THEN
    REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
    MESON_TAC[]) in
  REWRITE_TAC[set_of_edge; lemma] THEN
  GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
add_translation_invariants
 [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];;

add_linear_invariants
 [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];;




(*H2k hypermap*)
(*let hk=new_definition`hk((D:A->bool),(f:A->A),(n:A->A),(e:A->A),(k:num)) <=>

CARD D = 2 * k /\ (f permutes D) /\ (n permutes D) /\ (e permutes D ) 
/\ (e o n o f= I)
/\ (?x:A y:A. (x IN D) /\ (y IN D) /\ (orbit_map (f:A->A)  (x) INTER orbit_map (f)  (y)={})
   /\ (D = orbit_map (f:A->A)  (x) UNION orbit_map (f)  (y)) 
/\ (IMAGE n (orbit_map (f:A->A)  (x)))= orbit_map (f)  (y))`;;
*)





(* ************************************************* *)
(* Proof remark rem:fan *)

let set_edges_is_finite_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)==> FINITE E`,
REPEAT GEN_TAC
THEN REWRITE_TAC[FAN;fan1;graph]
THEN STRIP_TAC
THEN MP_TAC(ISPEC `V:real^3->bool`FINITE_POWERSET)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`UNIONS (E:(real^3->bool)->bool) SUBSET (V:real^3->bool)==> E SUBSET {t| t SUBSET V}`) 
THEN RESA_TAC
  THEN MP_TAC(ISPECL [`(E:(real^3->bool)->bool)`;`{t| t SUBSET (V:real^3->bool)}`] FINITE_SUBSET)
THEN ASM_SET_TAC[]);;

let remark_fan1=prove(`!v w V E. (v IN V) /\ (w IN V) ==>((w IN set_of_edge v V E)<=>(v IN set_of_edge w V E))`, 
(let lemma=prove(`{w,v}={v,w}`, SET_TAC[]) in
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM]  THEN ASM_REWRITE_TAC[] THEN MESON_TAC[lemma]));;
let remark_finite_fan1=prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FINITE V ==> FINITE (set_of_edge v V E)`,
REPEAT GEN_TAC THEN DISCH_TAC 
  THEN MP_TAC(ISPECL [`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`; `V:real^3->bool`] FINITE_SUBSET) 
  THEN ASM_REWRITE_TAC[]
  THEN REWRITE_TAC[set_of_edge] THEN SET_TAC[] );;
let properties_of_set_of_edge=prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) u:real^3.  UNIONS E SUBSET V
==>
({v,u} IN E <=> u IN set_of_edge v V E)`,
REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM] 
THEN STRIP_TAC
 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC
  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
let properties_of_set_of_edge_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 <=> u IN set_of_edge v V E)`,
REWRITE_TAC[FAN] THEN REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM] 
THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"a") THEN STRIP_TAC 
 THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC
  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;


let properties_of_graph=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). 
FAN(x,V,E) /\{v,u} IN E==> v IN V`,

REPEAT GEN_TAC THEN REWRITE_TAC[FAN] THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT STRIP_TAC THEN
REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS; SUBSET; IN_ELIM_THM] THEN DISCH_TAC 
  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`v:real^3` th)) THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `{(v:real^3),(u:real^3)}` THEN ASM_TAC THEN SET_TAC[]);;
 

let th3a12=prove(`!x v u.(~ collinear {x,v,u} ==> DISJOINT {x,u} {v})`,
   (let th=prove(`{x,v,u}={x,v,u}`, SET_TAC[]) in
REPEAT GEN_TAC THEN REWRITE_TAC[th;IN_DISJOINT] THEN MATCH_MP_TAC MONO_NOT THEN 
REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; IN_SING] THEN STRIP_TAC 
  THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC 
THEN ASM_REWRITE_TAC[] THEN SET_TAC[]));; 


let th3a=prove(`!x v u.(~ collinear {x,v,u} ==> DISJOINT {x,v} {u})`,
   (let th=prove(`{x,v,u}={x,u,v}`, SET_TAC[]) in
REPEAT GEN_TAC THEN REWRITE_TAC[th;IN_DISJOINT] THEN MATCH_MP_TAC MONO_NOT THEN 
REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; IN_SING] THEN STRIP_TAC 
  THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC 
THEN ASM_REWRITE_TAC[] THEN SET_TAC[]));; 
   let th3b=prove(`!x v u. ~ collinear {x,v,u} ==> ~(x=v) `,
REPEAT GEN_TAC THEN REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; DE_MORGAN_THM] THEN SET_TAC[]);; 
let th3b1=prove(`!x v u. ~ collinear {x,v,u} ==> ~(x=u) `,
(let th=prove(`{x,v,u}={x,u,v}`, SET_TAC[]) in
REWRITE_TAC[th;th3b]));; 

   let th3c= prove(`!x v u. ~ collinear {x,v,u} ==> ~(u IN aff {x,v})`,
REPEAT GEN_TAC THEN MATCH_MP_TAC MONO_NOT 
THEN REWRITE_TAC[aff; AFFINE_HULL_2; IN_ELIM_THM;COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; DE_MORGAN_THM] 
THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ARITH `u'+v'= &1 <=> v'= &1 -u'`] 
  THEN DISCH_TAC THEN ASM_REWRITE_TAC[] 
THEN REWRITE_TAC[VECTOR_ARITH`(u = u' % x + (&1 - u') % v) <=> (u - v = u' % (x-v))`] THEN SET_TAC[]);;   

let th3d=prove(`!x v u. ~(x=v)/\ ~(x=u) ==> DISJOINT {x} {v,u}`,
SET_TAC[]);;
let th3=prove(`!x v u. ~ collinear {x,v,u} ==> ~ (x=v) /\ ~(x=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\DISJOINT {x} {v,u} /\ ~(u IN aff {x,v})`, 
MESON_TAC[th3a;th3b;th3b1;th3c;th3d;th3a12]);;

let collinear1_fan=prove(`!x v u. ~ collinear {x,u,v} <=> ~(u IN aff {x,v})/\ ~ (x=v)`,
(let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
REPEAT GEN_TAC THEN EQ_TAC
THENL[
MESON_TAC[th3;lem];
REWRITE_TAC[SET_RULE`~(t1) /\ ~ t2<=> ~(t2\/ t1)`;COLLINEAR_3_EXPAND;aff; AFFINE_HULL_2;IN_ELIM_THM] 
THEN MATCH_MP_TAC MONO_NOT  THEN MATCH_MP_TAC MONO_OR THEN STRIP_TAC 
THENL[
REWRITE_TAC[];

STRIP_TAC THEN EXISTS_TAC`u':real` THEN EXISTS_TAC`&1- (u':real)` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]));;

let collinear_fan=prove(`!x v u. ~ collinear {x,v,u} <=> ~(u IN aff {x,v})/\ ~ (x=v)`,
(let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
MESON_TAC[collinear1_fan;lem]));;
  let th4=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). 
FAN(x,V,E) /\{v,u} IN E==> ~(x=v)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`; `(v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[FAN;fan2] THEN SET_TAC[]);;
let remark4_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). 
FAN(x,V,E) /\ {v,u} IN E==> ~ (x=v) /\ ~(x=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\ DISJOINT {x} {v,u} /\ ~(u IN aff {x,v})`,

REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT DISCH_TAC THEN REMOVE_THEN"a"(fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REWRITE_TAC[th3]);;

let collinears_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). 
FAN(x,V,E) /\{v,u} IN E==>( ~ collinear {x,v,u} <=> ~(u IN aff {x,v}))`,
MESON_TAC[remark4_fan;collinear_fan]);;
let remark1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). 
FAN(x,V,E) ==>
FINITE (set_of_edge v V E) 
/\({v,u} IN E <=> u IN set_of_edge v V E)/\
({v,u} IN E==>
~ collinear {x,v,u}/\
~ (x=v) /\ ~(x=u)/\ ~(v=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\DISJOINT {x} {v,u}  /\ ~(u IN aff {x,v}) /\ v IN V/\ ( ~ collinear {x,v,u} <=> ~(u IN aff {x,v})))`,
MESON_TAC[FAN;fan1;remark_finite_fan1;remark4_fan; properties_of_graph; SET_RULE`DISJOINT {x,v} {u} ==> ~(v=u)`;collinears_fan;properties_of_set_of_edge_fan]);;


(***************SIGMA_FAN*****************)



let sigma_fan=new_definition`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=  
(if (set_of_edge v V E = {u} ) then u 
    else (@(w:real^3).  (w IN (set_of_edge v V E)) /\ ~(w=u) /\
(!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`;;

(* This extends sigma to have a larger domain
   of R^3 rather than just V.  It is the
   identity outside V (compare the definition
   of `permutes` ).   *)




let extension_sigma_fan=new_definition`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=  
(if ~(u IN set_of_edge v V E ) then u 
    else (sigma_fan x V E v u))`;;




let exists_sigma_fan=prove(`
(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
~ (set_of_edge v V E= {u} ) 
/\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
==>
(?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
(!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))
`,

(let lemma = prove
   (`!X:real->bool. 
          FINITE X /\ ~(X = {}) 
          ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
    MESON_TAC[INF_FINITE]) in


MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC (ISPECL[`(v:real^3)` ;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
  
SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
THENL[(*2*)
ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)

DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
THENL[(*3*)
POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
  THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
THENL[(*4*)
ASM_TAC THEN SET_TAC[];(*4*)
ASM_TAC THEN SET_TAC[]](*4*);(*3*)
SUBGOAL_THEN`~(IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))={})` ASSUME_TAC
THENL[(*4*)
REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)

SUBGOAL_THEN` FINITE (IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` ASSUME_TAC
THENL[(*5*)
ASM_MESON_TAC[FINITE_IMAGE];(*5*)
REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` th)) 
  THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`x':real^3`
  THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
](*5*)](*4*)](*3*)](*2*)(*1*)));;

let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;

let exists_inverse_sigma_fan_alt=prove(`
(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
~ (set_of_edge v V E= {u} ) 
/\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
==>
(?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
(!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim1 x v u w <=  azim1 x v u w1)))
`,
(let lemma = prove
   (`!X:real->bool. 
          FINITE X /\ ~(X = {}) 
          ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
    MESON_TAC[INF_FINITE]) in
MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC (ISPECL[`(v:real^3)` ;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
THENL[(*2*)

ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
THENL[(*3*)
POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
  THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
THENL[(*4*)
ASM_TAC THEN SET_TAC[];(*4*)
ASM_TAC THEN SET_TAC[](*4*)];

SUBGOAL_THEN`~(IMAGE ( azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))={})` ASSUME_TAC
THENL[(*4*)
REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
SUBGOAL_THEN` FINITE (IMAGE (azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` ASSUME_TAC
THENL[(*5*)
ASM_MESON_TAC[FINITE_IMAGE];(*5*)
REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` th)) 
  THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM]THEN STRIP_TAC
THEN EXISTS_TAC`x':real^3`
  THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
](*5*)](*4*)](*3*)](*2*)(*1*)));;







let SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
~ (set_of_edge v V E= {u} ) 
/\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
==>
((sigma_fan x V E v u) IN (set_of_edge v V E)) /\ ~((sigma_fan x V E v u)=u) /\
(!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u (sigma_fan x V E v u) <= azim x v u w1)`,

REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[sigma_fan]
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]exists_sigma_fan)  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);;



let sigma_fan_in_set_of_edge=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
FAN(x,V,E) /\ (u IN (set_of_edge v V E))
==>
((sigma_fan x V E v u) IN (set_of_edge v V E))`,

REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~ (set_of_edge v V E= {u:real^3} )\/ (set_of_edge v V E= {u} )`)
THENL[
 MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]SIGMA_FAN) 
THEN ASM_TAC 
THEN SET_TAC[];
ASM_REWRITE_TAC[sigma_fan;IN_SING]]);;



let AFF_GE_2_1 = prove
 (`!x v w.
        DISJOINT {x,v} {w}
        ==> aff_ge {x,v} {w} =
             {y | ?t1 t2 t3.
                     &0 <= t3 /\
                     t1 + t2 + t3 = &1 /\
                     y = t1 % x + t2 % v + t3 % w}`,
  AFF_TAC);;
let AFF_GE_1_2 = prove
 (`!x v w.
        DISJOINT {x} {v,w}
        ==> aff_ge {x} {v,w} =
             {y | ?t1 t2 t3.
                     &0 <= t2 /\ &0 <= t3 /\
                     t1 + t2 + t3 = &1 /\
                     y = t1 % x + t2 % v + t3 % w}`,
  AFF_TAC);;
let AFF_GE_1_1 = prove
 (`!x v w.
        DISJOINT {x} {v}
        ==> aff_ge {x} {v} =
             {y | ?t1 t2.
                     &0 <= t2 /\
                     t1 + t2 = &1 /\
                     y = t1 % x + t2 % v }`,
  AFF_TAC);;



let UNIQUE_FOINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\
 ~(aff_ge {x} {v,u} INTER aff_ge {x} {v,w}=aff_ge {x} {v}) 
==> u=w`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan7;fan6] THEN STRIP_TAC 
  THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
  THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT STRIP_TAC
  THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v:real^3),(w:real^3)}`]th)) 
  THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
  THEN DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ ((u:real^3)=(w:real^3))`)
THENL
[  MP_TAC(SET_RULE`~((u:real^3)=(w:real^3))==> {(v:real^3),(u:real^3)} INTER {(v:real^3),(w:real^3)}={v}`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[];
ASM_TAC THEN SET_TAC[]]);;
 







let UNIQUE1_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ w IN aff_gt {x,v} {u} 
==> u=w`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC UNIQUE_FOINT_FAN THEN 
EXISTS_TAC `x:real^3` THEN EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `E:(real^3->bool)->bool` THEN EXISTS_TAC `v:real^3`
	   THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC)
	   THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7] THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC)
	   THEN DISCH_TAC THEN  DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
	   THEN DISCH_THEN (LABEL_TAC "a")
	   THEN DISCH_THEN (LABEL_TAC "b") THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) 
  THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th))
  THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
	   THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c")
	   THEN DISCH_TAC THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]th3) THEN ASM_REWRITE_TAC[]
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]th3) THEN ASM_REWRITE_TAC[]
	   THEN DISCH_TAC THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[]
	   THEN DISCH_TAC THEN REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC
	   THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(v:real^3)} SUBSET aff {x,v}` ASSUME_TAC
THENL (*1*)[
MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_1) 
THEN MP_TAC(SET_RULE`~((x:real^3) = (v:real^3))==> DISJOINT {x} {v}`)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN ASM_REWRITE_TAC[]
  THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*1*)
	   
SUBGOAL_THEN `~((w:real^3) IN aff_ge {x} {v})` ASSUME_TAC 
THENL (*2*)[
ASM_TAC THEN SET_TAC[];(*2*)

POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "d") THEN DISJ_CASES_TAC(REAL_ARITH `(&0 <= (t2:real))\/ (&0 <= (-- (t2:real)))`)
THENL (*3*)[
 SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
THENL (*4*)[
 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2) 
   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC `t1:real` 
  THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real` THEN ASM_REWRITE_TAC[]
    THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*4*)

 SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
THENL (*5*)[
 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2) 
   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC `&0:real` 
  THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real`  THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &0 % v + &1 % w `] THEN REAL_ARITH_TAC;(*5*)

ASM_TAC THEN SET_TAC[]](*5*)](*4*);(*3*)

 SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
THENL (*4*)[
 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2) 
   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC `inv(t3:real) *(--(t1:real))` 
  THEN EXISTS_TAC `inv(t3:real)*(--(t2:real))` THEN EXISTS_TAC `inv(t3:real)` 
THEN MP_TAC(ISPEC `t3:real` REAL_LT_INV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(REAL_ARITH`&0< inv(t3:real)==> (&0 <= inv(t3:real))`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL [`inv (t3:real)`;`(--(t2:real))`] REAL_LE_MUL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`inv(t3:real) * -- (t1:real)+ inv(t3) * --(t2:real) +inv (t3)=inv (t3)*(&1-t1-t2)`] THEN
MP_TAC(REAL_ARITH`(t1:real)+(t2:real)+(t3:real)= &1 ==> &1 - t1- t2=t3`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
MP_TAC(REAL_ARITH`&0<(t3:real)==> ~(t3= &0)`) THEN ASM_REWRITE_TAC[VECTOR_ARITH`
 (inv t3 * --t1) % x +
 (inv t3 * --t2) % v +
 inv t3 % (t1 % x + t2 % v + t3 % u)= (inv t3 * t3) % u `
] THEN DISCH_TAC
THEN MP_TAC(ISPEC `t3:real` REAL_MUL_LINV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH ` v= &1 % v`];(*4*)

 SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
THENL (*5*)[
 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2) 
   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC `&0:real` 
  THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real`  THEN REWRITE_TAC[VECTOR_ARITH`u= &0 % x+ &0 % v + &1 % u `] THEN REAL_ARITH_TAC;(*5*)
ASM_TAC THEN SET_TAC[]](*5*)](*4*)](*3*)](*2*)](*1*));;

let UNIQUE_AZIM_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3 w1:real^3.
FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ { v, w1} IN E /\ (azim x v u w =azim x v u w1) 
==> w=w1`,

REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN  REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC
  THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
  THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w1:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
  THEN REPEAT STRIP_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`;` w1:real^3`] AZIM_EQ) 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)`;` w1:real^3`]UNIQUE1_POINT_FAN) THEN ASM_REWRITE_TAC[]      );;

let UNIQUE_AZIM_0_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ (azim x v u w = &0) 
==> u=w`,

REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN  REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC
  THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
  THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
  THEN REPEAT STRIP_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`] AZIM_EQ_0_ALT) 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)`;` (u:real^3)`;` w:real^3`]UNIQUE1_POINT_FAN) THEN ASM_REWRITE_TAC[]	       );;



let UNIQUE_SIGMA_FAN=prove(`
(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
~ (set_of_edge v V E= {u} ) 
/\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
/\ (w IN (set_of_edge v V E)) /\ ~(w=u) /\
(!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)
==> sigma_fan x V E v u=w)`,

	(   let th=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)
==> (w IN aff_gt {x,v} {u} ==> u=w)`, MESON_TAC[UNIQUE1_POINT_FAN]
) in

ASSUME_TAC(th) THEN
REPEAT GEN_TAC  THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"123") THEN 
DISCH_TAC  THEN DISCH_THEN(LABEL_TAC "1") 
  THEN DISCH_THEN(LABEL_TAC "2") THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_THEN(LABEL_TAC "4") 
  THEN DISCH_THEN(LABEL_TAC"a") 
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)` ;`(v:real^3)`; `(u:real^3)`]SIGMA_FAN) 
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN REMOVE_THEN "a" (fun th->MP_TAC(ISPEC `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)` th)) 
  THEN ASM_REWRITE_TAC[]
  THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `w:real^3` th)) THEN ASM_REWRITE_TAC[] 
  THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"b")
  THEN REPEAT DISCH_TAC
  THEN SUBGOAL_THEN `azim x v u (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) = azim x v u (w:real^3)` ASSUME_TAC
THENL[
REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
REMOVE_THEN "123" (fun th->MP_TAC (ISPECL[`(x:real^3)`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`; `(v:real^3)` ; `(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;`(w:real^3)`]th)) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
REMOVE_THEN"1" MP_TAC 
THEN  REWRITE_TAC[FAN;fan6;fan7] THEN STRIP_TAC THEN
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_THEN (LABEL_TAC "d")
  THEN REMOVE_THEN"2" MP_TAC THEN REMOVE_THEN"3" MP_TAC THEN REMOVE_THEN"b" MP_TAC 
  THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT STRIP_TAC
  THEN REMOVE_THEN "c" MP_TAC THEN DISCH_TAC
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))}`th) THEN ASSUME_TAC(th))
  THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC  
  THEN 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))`; `(w:real^3)`]AZIM_EQ )
  THEN ASM_REWRITE_TAC[]
  THEN ASM_MESON_TAC[]]));; 


let CYCLIC_SET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
FAN(x,V,E) /\ v IN V 
==> cyclic_set (set_of_edge v V E) x v`,
REPEAT GEN_TAC 
THEN STRIP_TAC 
THEN REPEAT (POP_ASSUM MP_TAC) 
THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) 
THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN; cyclic_set;fan1;fan2;fan6;fan7] THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC
  THENL(*1*)[ASM_TAC THEN SET_TAC[];(*1*)
STRIP_TAC
  THENL (*2*)[ASM_TAC THEN SET_TAC[remark_finite_fan1];(*2*)
 STRIP_TAC THENL(*3*)[

ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN
REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
  DISCH_THEN(LABEL_TAC "a") THEN   DISCH_THEN(LABEL_TAC "b")
THEN STRIP_TAC THEN STRIP_TAC THEN
REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (p:real^3)}` th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3), (q:real^3)}` th))
  THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]th3) THEN ASM_REWRITE_TAC[]
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (q:real^3)`]th3) THEN ASM_REWRITE_TAC[]
  THEN POP_ASSUM (fun th-> REWRITE_TAC[])
  THEN POP_ASSUM (fun th-> REWRITE_TAC[])
  THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
  THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(q:real^3) IN aff_gt {(x:real^3),(v:real^3)} {(p:real^3)}` ASSUME_TAC

THENL (*4*)[
 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[]
	   THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
   THEN EXISTS_TAC `--(h:real)` THEN EXISTS_TAC `(h:real)` THEN EXISTS_TAC `&1` THEN REWRITE_TAC[VECTOR_ARITH`q= (-- (h:real)) % x + (h:real) % v + &1 % (q+ h% (x-v))`] THEN REAL_ARITH_TAC;(*4*)

ASM_MESON_TAC[UNIQUE1_POINT_FAN]](*4*);(*3*)

REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM] THEN GEN_TAC 
THEN SUBGOAL_THEN`(x':real^3) IN set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ==> ~(x' IN aff {x,v})`
ASSUME_TAC
THENL(*4*)[
ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN
REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
  DISCH_THEN(LABEL_TAC "a") THEN   DISCH_THEN(LABEL_TAC "b")
THEN STRIP_TAC THEN STRIP_TAC THEN
REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (x':real^3)}` th) )
  THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN STRIP_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (x':real^3)`]th3) THEN ASM_MESON_TAC[]; (*4*)

EQ_TAC THENL(*5*)[

POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN STRIP_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[aff];(*5*)

ASM_TAC THEN SET_TAC[]](*5*)](*4*)] (*3*)]]);; 

let subset_cyclic_set_fan=prove(`!x:real^3 v:real^3 V:real^3->bool W:real^3->bool.
V SUBSET W /\ cyclic_set W x v ==> cyclic_set V x v`,

REPEAT GEN_TAC THEN REWRITE_TAC[cyclic_set] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] 
  THEN MP_TAC(ISPECL[`V:real^3->bool`;`W:real^3->bool`]FINITE_SUBSET) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN SET_TAC[]);;


let property_of_cyclic_set=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 cyclic_set {u, w1, w2} x v
==> ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x}`,

(let th= prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN {x,w1,w2}`, SET_TAC[]) in

(let th1=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN  affine hull {x,v}
`,REPEAT GEN_TAC THEN REWRITE_TAC[AFFINE_HULL_2;INTER; IN_ELIM_THM] THEN EXISTS_TAC`&1` THEN EXISTS_TAC `&0` THEN
 MESON_TAC[REAL_ARITH`&1+ &0= &1`; VECTOR_ARITH`x= &1 % x + &0 % v`])
in

(let th2=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN {x,w1,w2} INTER affine hull {x,v}
`, REWRITE_TAC[INTER;IN_ELIM_THM] THEN REWRITE_TAC[th;th1]) in


REPEAT GEN_TAC THEN 
REWRITE_TAC[COLLINEAR_LEMMA;DE_MORGAN_THM;VECTOR_ARITH`a-b=vec 0 <=> a=b`;cyclic_set;] THEN STRIP_TAC 
  THEN ASM_REWRITE_TAC[VECTOR_ARITH`(v:real^3)=(x:real^3) <=> x=v`] THEN STRIP_TAC
THENL[ STRIP_TAC  THEN
  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 ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`] th2) THEN ASM_TAC THEN SET_TAC[];

STRIP_TAC THENL[

STRIP_TAC  THEN
  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 ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`] th2) THEN ASM_TAC THEN SET_TAC[];

STRIP_TAC 
THEN 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 MP_TAC 
THEN REWRITE_TAC[VECTOR_ARITH`(c:real) % ((v:real^3)-(x:real^3))=(u:real^3)-x <=> u =  (&1 - c) % x+c % v`] 
THEN DISCH_TAC 
THEN SUBGOAL_THEN `(u:real^3) IN affine hull {(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[
REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM] 
THEN EXISTS_TAC `&1 - (c:real)` 
THEN EXISTS_TAC`c:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - (c:real) +c= &1`;];

MP_TAC(ISPECL[`u:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`]th) 
THEN DISCH_TAC 
THEN ASM_TAC 
THEN SET_TAC[INTER]
]]]))));;

let property_of_cyclic_set1=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 cyclic_set {u, w1, w2} x v ==> ~collinear {x, v, w1}`,
				 
(let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in

REPEAT GEN_TAC THEN DISCH_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`;`u:real^3`; `w2:real^3`] property_of_cyclic_set) THEN ASM_REWRITE_TAC[th] THEN STRIP_TAC THEN ASM_REWRITE_TAC[COLLINEAR_3]));;
let property_of_cyclic_set2=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 cyclic_set {u, w1, w2} x v
==> ~collinear {x, v, w2}`,			 
( let th=prove(`{u,w1,w2}={w2,w1,u}`,SET_TAC[]) in
( let th1=prove(`{u,w1,w2}={w1,w2,u}`,SET_TAC[]) in

REPEAT GEN_TAC THEN DISCH_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w2:real^3`;`w1:real^3`; `u:real^3`] property_of_cyclic_set)
THEN ASM_REWRITE_TAC[th] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN MESON_TAC[th1;COLLINEAR_3])));;
let property_of_cyclic_set3=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 cyclic_set {u, w1, w2} x v
==> ~ collinear {x, v, u}`,
( let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in

REPEAT GEN_TAC THEN DISCH_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_MESON_TAC[COLLINEAR_3;th]));;


let properties_of_cyclic_set=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 cyclic_set {u, w1, w2} x v
==> ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x}
/\ ~collinear {x, v, u}
/\ ~collinear {x, v, w1}
/\  ~collinear {x, v, w2}`,

MESON_TAC[property_of_cyclic_set;property_of_cyclic_set2;property_of_cyclic_set1;property_of_cyclic_set3]);;


let XOHLED=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
FAN(x,V,E) /\ v IN V 
==> cyclic_set (set_of_edge v V E) x v`,
MESON_TAC[CYCLIC_SET_EDGE_FAN]);;



let d1_fan =new_definition`
d1_fan (x,V,E) ={(x':real^3,v:real^3,w:real^3,w1:real^3)| (x'=x) /\ ({v,w} IN  E)/\ (w1 = sigma_fan x V E v w)}`;;
(* d2_fan not yet used *)

let d2_fan=new_definition`d2_fan (x,V,E)={ (x',v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;

let inverse_sigma_fan_alt=new_definition`inverse_sigma_fan_alt x V E v w = @a. sigma_fan x V E v a=w`;;
let e_fan=new_definition` e_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,v,(sigma_fan x V E w v)))`;;

let f_fan=new_definition`f_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse_sigma_fan_alt x V E w v),v) )`;;


let n_fan=new_definition`n_fan (x:real^3) V E =(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,(sigma_fan x V E v w),(sigma_fan x V E v (sigma_fan x V E v w))))`;;
(* i_fan corrects the 4th coordinate to be
   the dart *)

let i_fan=new_definition`i_fan (x:real^3) V E=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,w,(sigma_fan x V E v w)))`;;
let pr1=new_definition`pr1=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). x)`;;
let pr2=new_definition`pr2=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). v)`;;
let pr3=new_definition`pr3=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w)`;;
let pr4=new_definition`pr4=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w1)`;;
(* if f = sigma, the power_map_points gives
   iterates of sigma (for fixed x v) *)


let power_map_points= new_recursive_definition num_RECURSION `(power_map_points f x V E v w 0 = w)/\(power_map_points f x V E v w  (SUC n)= f x V E v (power_map_points f x V E v w n))`;;
(* This is the composition operator (o),
   specialized to functions on 4-tuples *)

let o_funs=new_definition`!(f:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (g:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3). o_funs f g =(\(x:real^3,y:real^3,z:real^3,t:real^3).  f (pr1 (g(x,y,z,t)),pr2(g(x,y,z,t)),pr3(g(x,y,z,t)),pr4(g(x,y,z,t))))`;;
(* powers of permutations *)

let power_maps= new_recursive_definition num_RECURSION `(power_maps  (f:real^3->(real^3->bool)->((real^3->bool)->bool)->real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) 0 = i_fan (x:real^3) V E) /\ (power_maps f x V E (SUC n)= o_funs (f x V E)  (power_maps f x V E n))`;;

(* powers of node map *)



 
let power_n_fan= new_definition`power_n_fan x V E n=( \(x,v,w,w1). (x,v,(power_map_points sigma_fan x V E v w n),(power_map_points sigma_fan x V E v w (SUC n))))`;; 


(* the node of a dart, in a special form
   for fans *)


let a_node_fan=new_definition`a_node_fan x V E (x,v,w,w1)={a | ?n. a=(power_maps  n_fan x V E n) (x,v,w,sigma_fan x V E v w)}`;;

(* The set X(V,E) *)

let xfan= new_definition`xfan (x,V,E)={v | ?e. (E e)/\(v IN aff_ge {x} e)}`;;
(* See comment by AS in fan_defs.hl.  The correct definition is there. *)
let yfan_deprecated= new_definition`yfan_deprecated (x,V,E)={v:real^3 | ?e. ( E e )/\(~(v IN aff_ge {x} e))}`;;

(*
W^0_{dart}(x,v,w...)
*)

let w_dart_fan=new_definition`w_dart_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ((y:real^3),(v:real^3),(w:real^3),(w1:real^3))=  
if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
else  
(if set_of_edge v  V E ={w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
else (if set_of_edge v  V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
 







let image_power_map_points=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
FAN(x,V,E)  /\ (u IN set_of_edge v V E)
==> power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E`,
INDUCT_TAC THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[power_map_points]
THENL[
ASM_MESON_TAC[];
REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC 
THEN REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(u:real^3)`] th)) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN DISJ_CASES_TAC(SET_RULE `set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i}\/ ~(set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i})`)
THENL[ASM_MESON_TAC[sigma_fan];
ASM_MESON_TAC[SIGMA_FAN]]]);;

let IN2_ORBITS_FAN=prove(`!(i:num) (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)
==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;
let IN1_ORBITS_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
FAN(x,V,E)  /\ (u IN set_of_edge v V E)
==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;

let remark_power_map_points=prove(`!(i:num) (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)
==> 
power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E
/\ {v,power_map_points sigma_fan x V E v u i} IN E
/\
 ~(collinear {x,v,power_map_points sigma_fan x V E v u i})
/\ ~(x = power_map_points (sigma_fan) x V E v u i) /\
             ~(v = power_map_points (sigma_fan) x V E v u i) /\
             DISJOINT {x, v} {power_map_points (sigma_fan) x V E v u i} /\
             ~((power_map_points (sigma_fan) x V E v u i) IN aff {x, v}) /\
             DISJOINT {x} {v, (power_map_points (sigma_fan) x V E v u i)} `,
MESON_TAC[IN2_ORBITS_FAN;remark1_fan;image_power_map_points;properties_of_set_of_edge_fan]);;






(*-------------------------------------------------------------------------------------------*)
(*    the properties in normal vector                                                        *)
(*-------------------------------------------------------------------------------------------*)
 
let imp_norm_not_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> ~(norm ( v - x) = &0)`,
REPEAT GEN_TAC THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(v:real^3)-(x:real^3)= vec 0` ASSUME_TAC THENL
                   [POP_ASSUM MP_TAC THEN MESON_TAC[NORM_EQ_0];
                    SUBGOAL_THEN `(v:real^3) = (x:real^3)` ASSUME_TAC THENL
                     [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;
                     ASM_TAC THEN SET_TAC[]]]);;

let imp_norm_gl_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> inv(norm ( v - x)) > &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(norm ( (v:real^3) - (x:real^3)) = &0)` ASSUME_TAC THENL
  [ASM_MESON_TAC[imp_norm_not_zero_fan];
   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
     [POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
      MP_TAC (ISPEC `norm((v:real^3)-(x:real^3))` REAL_LT_INV_EQ) THEN POP_ASSUM MP_TAC 
THEN REAL_ARITH_TAC]]);;

let imp_inv_norm_not_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> ~(inv(norm ( v - x)) = &0)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN SUBGOAL_THEN `inv(norm ((v:real^3) - (x:real^3))) > &0` ASSUME_TAC
THENL
  [ASM_MESON_TAC[imp_norm_gl_zero_fan]; 
   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]);;

let imp_norm_ge_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> inv(norm ( v - x)) >= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(norm ( (v:real^3) - (x:real^3)) = &0)` ASSUME_TAC THENL
  [ASM_MESON_TAC[imp_norm_not_zero_fan];
   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
     [POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
      MP_TAC (ISPEC `norm((v:real^3)-(x:real^3))` REAL_LT_INV_EQ) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]]);;
let norm_of_normal_vector_is_unit_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> norm(inv(norm ( v - x))% (v-x))= &1`,
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[NORM_MUL] THEN SUBGOAL_THEN ` inv(norm ( (v:real^3) - (x:real^3))) >= &0` ASSUME_TAC THENL[ ASM_MESON_TAC[imp_norm_ge_zero_fan]; 
                SUBGOAL_THEN ` ~(norm ( (v:real^3) - (x:real^3))= &0)` ASSUME_TAC THENL
                   [ASM_MESON_TAC[imp_norm_not_zero_fan];
                    SUBGOAL_THEN ` abs(inv(norm ( (v:real^3) - (x:real^3))))= inv(norm ( (v:real^3) - (x:real^3)))` ASSUME_TAC THENL
                       [ASM_MESON_TAC[REAL_ABS_REFL;REAL_ARITH `(a:real)>= &0 <=> &0 <= a`; ];
                        MP_TAC(ISPEC `norm ( (v:real^3) - (x:real^3))` REAL_MUL_LINV)THEN ASM_REWRITE_TAC[]]]]);;


(*---------------------------------------------------------------------------------------*)
(* the normal coordinate is the definiton of frame in flyspeck(above JBDNJJB)              *)
(*---------------------------------------------------------------------------------------*)
 

let e3_fan=new_definition`e3_fan  (x:real^3) (v:real^3) (u:real^3) = inv(norm((v:real^3)-(x:real^3))) % ((v:real^3)-(x:real^3))`;;



  let e2_fan=new_definition`e2_fan (x:real^3) (v:real^3) (u:real^3) = inv(norm((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3)))) % ((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))) `;;  
let e1_fan=new_definition`e1_fan (x:real^3) (v:real^3) (u:real^3)=(e2_fan (x:real^3) (v:real^3) (u:real^3)) cross (e3_fan (x:real^3) (v:real^3) (u:real^3))`;;

  
  let e3_mul_dist_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) ==> dist (v,x) % e3_fan x v u = v - x`,
REPEAT GEN_TAC THEN REWRITE_TAC[e3_fan; dist; VECTOR_ARITH `(a:real) % (b:real)% (v:real^3)=(a*b)%v`] THEN 
MESON_TAC[imp_norm_not_zero_fan; REAL_MUL_RINV; VECTOR_ARITH `&1 %(v:real^3)=v`]);;
let norm_dot_fan=prove(`!x:real^3. norm x = &1 ==> x dot x = &1`,
 ASM_MESON_TAC[NORM_POW_2; REAL_ARITH `&1 pow 2= &1`]);;

  let e3_is_normal_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) ==> e3_fan x v u dot e3_fan x v u = &1`,
REPEAT GEN_TAC THEN REWRITE_TAC[e3_fan]THEN DISCH_TAC 
THEN SUBGOAL_THEN `norm(inv(norm((v:real^3)-(x:real^3))) %(v-x)) pow 2= &1 pow 2` ASSUME_TAC THENL
 [ASM_MESON_TAC[norm_of_normal_vector_is_unit_fan] ;
ASM_MESON_TAC[NORM_POW_2; REAL_ARITH `&1 pow 2= &1`]]);;
  let e2_is_normal_fan= prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> e2_fan x v u dot e2_fan x v u = &1`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))= vec 0)` ASSUME_TAC 
THENL[
POP_ASSUM MP_TAC THEN MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[e3_fan;CROSS_LMUL] 
THEN DISCH_TAC THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`] imp_inv_norm_not_zero_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 
MP_TAC(ISPECL [`inv(norm((v:real^3)-(x:real^3)))`; `((v:real^3) -(x:real^3)) cross ((u:real^3)-(x:real^3))`; `(vec 0):real^3`] VECTOR_MUL_LCANCEL_IMP) 
THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO;CROSS_EQ_0 ];

MP_TAC(ISPECL [`(e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))`; `((vec 0):real^3)`] norm_of_normal_vector_is_unit_fan) THEN 
ASM_REWRITE_TAC[] THEN REWRITE_TAC[e2_fan; VECTOR_ARITH`(v:real^3)- vec 0 = v`] THEN MESON_TAC[norm_dot_fan]]);; 

  let e2_orthogonal_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. 
~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (e2_fan x v u) dot (e3_fan x v u)= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;e3_fan;CROSS_LMUL;DOT_RMUL;] THEN VEC3_TAC);;


  let e1_is_normal_fan=prove(`!x:real^3 v:real^3 u:real^3. 
~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> e1_fan x v u dot e1_fan x v u = &1`,
REPEAT GEN_TAC THEN STRIP_TAC THEN 
REWRITE_TAC[e1_fan;DOT_CROSS] THEN 
MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e2_orthogonal_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 
MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e2_is_normal_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN  
MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e3_is_normal_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
  let e1_orthogonal_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
==> (e1_fan x v u) dot (e3_fan x v u)= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;DOT_CROSS_SELF] );;

  let e1_orthogonal_e2_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
==> (e1_fan x v u) dot (e2_fan x v u)= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;DOT_CROSS_SELF] );;

  let e1_cross_e2_dot_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==>
&0 < (e1_fan x v u cross e2_fan x v u) dot e3_fan x v u`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;CROSS_TRIPLE] 
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e1_is_normal_fan) 
THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[e1_fan] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;


  let orthonormal_e1_e2_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==>
(orthonormal (e1_fan x v u) (e2_fan x v u) (e3_fan x v u))`,
REPEAT GEN_TAC THEN REWRITE_TAC[orthonormal] THEN DISCH_TAC THEN 
ASM_MESON_TAC[e1_is_normal_fan;e2_is_normal_fan;e3_is_normal_fan;e1_orthogonal_e2_fan;
e1_orthogonal_e3_fan;e2_orthogonal_e3_fan;e1_cross_e2_dot_e3_fan]);;


  let dot_e2_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
==> (u-x) dot e2_fan x v u = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;DOT_RMUL;DOT_CROSS_SELF] THEN REAL_ARITH_TAC);;
let vdot_e2_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
==> (v-x) dot e2_fan x v u = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;e3_fan;CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF] THEN REAL_ARITH_TAC);;
let vcross_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
==>
(v - x) cross (e3_fan x v u) = vec 0`,

REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e3_fan;CROSS_RMUL;CROSS_REFL] THEN VECTOR_ARITH_TAC);;
let udot_e1_fan=prove(`!x:real^3 v:real^3 u:real^3. 
~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
==> &0 < (u - x) dot e1_fan x v u `,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan; e2_fan;CROSS_LMUL;DOT_RMUL;DOT_SYM;DOT_LMUL;CROSS_TRIPLE]
THEN SUBGOAL_THEN `~((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))= vec 0)` ASSUME_TAC
THENL[
POP_ASSUM MP_TAC THEN MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[e3_fan;CROSS_LMUL] 
THEN DISCH_TAC THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`] imp_inv_norm_not_zero_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 
MP_TAC(ISPECL [`inv(norm((v:real^3)-(x:real^3)))`; `((v:real^3) -(x:real^3)) cross ((u:real^3)-(x:real^3))`; `(vec 0):real^3`] VECTOR_MUL_LCANCEL_IMP) 
THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO;CROSS_EQ_0 ];
MP_TAC(ISPECL [`(e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))`; `((vec 0):real^3)`]imp_norm_gl_zero_fan) THEN 
ASM_REWRITE_TAC[REAL_ARITH`(a:real)> &0 <=> &0 < (a:real)`;VECTOR_ARITH `(a:real^3)- vec 0=a`] THEN DISCH_TAC
  THEN MP_TAC(ISPEC `e3_fan (x:real^3) (v:real^3) (u:real^3) cross (u-x)`DOT_POS_LT) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[REAL_LT_MUL]]);;  

let udot_e1_fan1=prove(`!x:real^3 v:real^3 u:real^3. 
~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
==> &0 <= (u - x) dot e1_fan x v u `,
REPEAT GEN_TAC THEN STRIP_TAC THEN 
MP_TAC(ISPECL[`x:real^3` ;`v:real^3` ;`u:real^3`]udot_e1_fan) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);; 

let vdot_e1_fan=prove(`!x:real^3 v:real^3 u:real^3. 
~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
==>  (v - x) dot e1_fan x v u = &0`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e3_mul_dist_fan) THEN RES_TAC THEN SYM_ASSUM_TAC THEN
REWRITE_TAC[DOT_SYM;DOT_LMUL] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e1_orthogonal_e3_fan) THEN RESA_TAC THEN
REAL_ARITH_TAC);;

 



let properties_coordinate=prove(`!x:real^3 v:real^3 u:real^3. 
~(collinear {x, v, u}) 
==> (orthonormal (e1_fan x v u) (e2_fan x v u) (e3_fan x v u))
/\ dist (v,x) % e3_fan x v u = v - x
/\ ((v - x) cross (e3_fan x v u) = vec 0)
/\  (v-x) dot e2_fan x v u = &0
/\ ((u-x) dot e2_fan x v u = &0)
/\  &0 <= (u - x) dot e1_fan x v u
/\ &0 < (u - x) dot e1_fan x v u
/\ (v - x) dot e1_fan x v u = &0`,
(	let lem=prove(`!a b c. {a,b,c}={b,a,c}`,SET_TAC[]) in
REPEAT GEN_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3)
  THEN RED_TAC THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[lem;] THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[COLLINEAR_3]
THEN
ASM_MESON_TAC[orthonormal_e1_e2_e3_fan;e3_mul_dist_fan; dot_e2_fan;vdot_e2_fan;vcross_e3_fan;udot_e1_fan;udot_e1_fan1;vdot_e1_fan]));;

let module_of_vector =prove(`!x:real^3 v:real^3 u:real^3 w:real^3 r:real psi:real h:real.
 ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) 
/\ (&0 < r) /\ (w=(r * cos psi) % e1_fan x v u + (r * sin psi) % e2_fan x v u + h % (v-x))
==>
sqrt(((w cross (e3_fan x v u)) dot e1_fan x v u) pow 2 + ((w cross (e3_fan x v u)) dot e2_fan x v u) pow 2) = r`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;] THEN
MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[]
  THEN DISCH_THEN (LABEL_TAC "a") 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 ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN ASM_REWRITE_TAC[] 
THEN MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ]vcross_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]CROSS_SKEW) 
  THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
  THEN REWRITE_TAC[DOT_LADD;DOT_LMUL;DOT_LZERO;DOT_LNEG]
  THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[orthonormal] THEN  DISCH_TAC THEN ASM_REWRITE_TAC[DOT_SYM]
  THEN REWRITE_TAC[REAL_ARITH `-- &0 = &0`; REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH `(a:real) * &1 = a`;
REAL_ARITH `(a:real) + &0 = a`;REAL_ARITH `&0 + (a:real) = a`;REAL_POW_MUL; REAL_ARITH `-- &1 pow 2 = &1`;
REAL_ARITH `(d:real) * (b:real) + d * (c:real) = d * ( b + c)`;SIN_CIRCLE; sqrt] THEN MATCH_MP_TAC SELECT_UNIQUE
THEN REWRITE_TAC[BETA_THM] THEN GEN_TAC THEN EQ_TAC

	   THENL[
              STRIP_TAC THEN SUBGOAL_THEN `((y:real) - (r:real))* (y + r) = &0` ASSUME_TAC
	       THENL[
		 REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_ARITH `((a:real)- (b:real)) * (c:real)= a *c - b * c`; 
REAL_ARITH`(y:real) * (r:real)= r * y`; REAL_ARITH `((a:real) +(b:real)) - ((b:real) + (c:real))= a - c`; 
REAL_ARITH `(a:real)- (c:real)= &0 <=> a = c`] 
		   THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
		 MP_TAC (ISPECL [`(y:real)- (r:real)`; `(y:real)+(r:real)` ]REAL_ENTIRE) THEN ASM_REWRITE_TAC[] 
		   THEN STRIP_TAC
		   THENL
		     [POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
		     REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]];

	     DISCH_TAC THEN ASM_REWRITE_TAC[] 
	       THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;


(****************************************************************************)
(*        some properties of azim in the orthonormal frame                  *)
(****************************************************************************)

let collinear_imp_azim_is_rezo_fan=prove(
`!x:real^3 v:real^3 u:real^3 y:real h1:real h2:real.
~(v = x) /\ ~(u = x) /\ ~collinear {x, v, u} 
/\ &0 <= y /\
 y < &2 * pi /\
 ( !e1:real^3 e2:real^3 e3:real^3.
          orthonormal e1 e2 e3 /\ dist (v,x) % e3 = v - x
          ==> (?psi:real r1:real r2:real.
                   u - x =
                   (r1 * cos psi) % e1 + (r1 * sin psi) % e2 + h1 % (v - x) /\
                   u - x =
                   (r2 * cos (psi + y)) % e1 +
                   (r2 * sin (psi + y)) % e2 +
                   h2 % (v - x) /\
                   &0 < r1 /\
                   &0 < r2))
 ==> y = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 
  THEN REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~collinear {vec 0, (v:real^3)-(x:real^3), (u:real^3)-x}` ASSUME_TAC
  THENL (*1*)[
    POP_ASSUM MP_TAC 
      THEN MATCH_MP_TAC MONO_NOT 
      THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`; `u:real^3`] COLLINEAR_3) 
      THEN SUBGOAL_THEN `{(v:real^3),(x:real^3),(u:real^3)}={x,v,u}` ASSUME_TAC
      THENL[SET_TAC[]; ASM_REWRITE_TAC[] THEN SET_TAC[]]; (*1*)
   REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 
     THEN DISCH_THEN (LABEL_TAC "1") THEN DISCH_THEN (LABEL_TAC "2") THEN REWRITE_TAC[LEFT_IMP_FORALL_THM] 
     THEN EXISTS_TAC `e1_fan (x:real^3) (v:real^3) (u:real^3)`
     THEN EXISTS_TAC `e2_fan (x:real^3) (v:real^3) (u:real^3)`
     THEN EXISTS_TAC `e3_fan (x:real^3) (v:real^3) (u:real^3)`
     THEN MP_TAC(ISPECL [`(x:real^3)` ;`(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[] 
     THEN DISCH_TAC
     THEN MP_TAC(ISPECL [`(x:real^3)` ;`(v:real^3)`;`u:real^3`] e3_mul_dist_fan)THEN ASM_REWRITE_TAC[] 
     THEN DISCH_THEN(LABEL_TAC "AB") THEN ASM_REWRITE_TAC[] THEN STRIP_TAC 
     THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)- (x:real^3)`; `r1:real`; `psi:real`; `h1:real`] module_of_vector) 
     THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
     THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)- (x:real^3)`; `r2:real`; `(psi:real)+(y:real)`; `h2:real`] module_of_vector)  
     THEN ASM_REWRITE_TAC[]
     THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 
     THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
     THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC 
     THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
     THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC
     THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC th)
     THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `sin (psi:real)= &0` ASSUME_TAC
      THENL (*2*)[
	MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan) 
	  THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DOT_LADD;DOT_LMUL] 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan) 
	  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN ASM_REWRITE_TAC[] 
	  THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`; 
               REAL_ARITH`(a:real) * &1= a`]
	  THEN DISCH_TAC
	  THEN MATCH_MP_TAC(ISPECL [`sin (psi:real)`;`&0`; `r1:real`] REAL_EQ_LCANCEL_IMP)  THEN ASM_REWRITE_TAC[] 
	  THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; (*2*)


	POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 
	  THEN POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC 
	  THEN DISCH_THEN (LABEL_TAC "a")   THEN DISCH_THEN (LABEL_TAC "b")
	  THEN REPEAT (DISCH_TAC) THEN REMOVE_THEN "a" MP_TAC THEN REMOVE_THEN "b" MP_TAC
	  THEN REWRITE_TAC[COS_ADD;SIN_ADD] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan) 
	  THEN ASM_REWRITE_TAC[] THEN  REWRITE_TAC[DOT_LADD;DOT_LMUL] 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan) 
	  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN ASM_REWRITE_TAC[] 
	  THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`&0 * (a:real) = &0`; 
              REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`; REAL_ARITH`(a:real) * &1= a`;REAL_ENTIRE] 
	  THEN ASM_REWRITE_TAC[]
	  THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
	  THEN STRIP_TAC
	     THENL(*3*)[
	       REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*3*)
	       MP_TAC(ISPEC `psi:real` SIN_CIRCLE) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;(*3*)
	       MP_TAC(ISPEC `y:real` SIN_EQ_0) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM MP_TAC 
		 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_TAC THEN REMOVE_THEN "1" MP_TAC 
		 THEN REMOVE_THEN "2" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(PI_WORKS) THEN REPEAT STRIP_TAC 
		 THEN MP_TAC(ISPECL [ `n:real`;`&2`;`pi:real`]REAL_LT_RCANCEL_IMP) 
		 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "4")
		 THEN MP_TAC(ISPECL [ `&0`;`n:real`;`pi:real`]REAL_LE_RCANCEL_IMP) 
		 THEN REWRITE_TAC[REAL_ARITH`&0 * (a:real) = &0`] 
		 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC "5")  
		 THEN MP_TAC(ISPECL [`n:real`; `pi:real`]REAL_ENTIRE) THEN DISCH_TAC THEN ASM_REWRITE_TAC[]  
		 THEN REMOVE_THEN "3" MP_TAC THEN REWRITE_TAC[integer] 
		 THEN MP_TAC(ISPEC `n:real` REAL_ABS_REFL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
		 THEN STRIP_TAC THEN REMOVE_THEN "4" MP_TAC THEN REMOVE_THEN "5" MP_TAC 
		 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
		 THEN MP_TAC(ISPECL [`0`; `n':num`]REAL_OF_NUM_LE) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
		 THEN MP_TAC(ISPECL [`n':num`; `2`]REAL_OF_NUM_LT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
		 THEN SUBGOAL_THEN `(n':num)= 0 \/ n' = 1` ASSUME_TAC
		    THENL (*4*)[
		      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;(*4*)
		      POP_ASSUM MP_TAC THEN STRIP_TAC
			THENL(*5*)[
			  ASM_MESON_TAC[REAL_OF_NUM_EQ];(*5*)
			  POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC 
			    THEN REMOVE_THEN "A" MP_TAC 
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])

			    THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC 
			    THEN REMOVE_THEN "A" MP_TAC 
			    THEN POP_ASSUM MP_TAC 
			    THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC 
			    THEN REMOVE_THEN "A" MP_TAC THEN ASM_REWRITE_TAC[] 
			    THEN REWRITE_TAC[REAL_ARITH `&1 * (a:real)=a`]
			    THEN POP_ASSUM MP_TAC 
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
			    THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC 
			    THEN REMOVE_THEN "A" MP_TAC THEN ASM_REWRITE_TAC[]
			    THEN REWRITE_TAC[SIN_PI;COS_PI; REAL_ARITH `(a:real)- &0 = a`; REAL_ARITH `(a:real) * &0= &0`;
				REAL_ARITH `(a:real) * -- &1= -- a`;
				VECTOR_ARITH `&0 % (v:real^3)= vec 0`; VECTOR_ARITH `(v:real^3)+ vec 0 + (w:real^3)= v+w`]
			    THEN REMOVE_THEN "AB" MP_TAC THEN DISCH_TAC 
			    THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM(th)]) THEN DISCH_TAC 
			    THEN SUBGOAL_THEN `(((r2:real) * --cos (psi:real)) % e1_fan (x:real^3) (v:real^3) (u:real^3) + (h2:real) % dist (v,x) % e3_fan x v u) dot e1_fan x v u =(((r2:real) * cos psi) % e1_fan x v u + (h1:real) % dist (v,x) % e3_fan x v u) dot e1_fan x v u` ASSUME_TAC
			    THENL (*6*)[
			      ASM_REWRITE_TAC[]; (*6*)
			      POP_ASSUM MP_TAC THEN REWRITE_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;]
				THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_is_normal_fan) 
				THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
				THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e3_fan) 
				THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
				THEN ASM_REWRITE_TAC[] 
				THEN REWRITE_TAC[REAL_ARITH `(a:real) * &0 = &0`; REAL_ARITH `(a:real)+ &0=a`; 
						 REAL_ARITH `(a:real) * &1 =a`; 
						 REAL_ARITH `(a:real) *(-- b)= a * b <=> &2 * a * b = &0`]
				THEN DISCH_TAC 
				THEN MP_TAC(ISPECL [`&2 * (r2:real)`; `cos (psi:real)`]REAL_ENTIRE) 
				THEN REWRITE_TAC[REAL_ARITH `((a:real)*(b:real))*(c:real)=a * b * c`] 
				THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
				 THENL(*7*)[
				   REPEAT(POP_ASSUM MP_TAC ) THEN REAL_ARITH_TAC;(*7*)
				   MP_TAC( ISPEC `psi:real` SIN_CIRCLE) 
				     THEN ASM_REWRITE_TAC[] 
				     THEN REWRITE_TAC[REAL_ARITH `&0 pow 2= &0`; REAL_ARITH `&0 + &0 = &0`] 
				     THEN SET_TAC[](*7*)](*6*)](*5*)]]]]]);;



let azim_is_zero_fan=prove(`!x:real^3 v:real^3 u:real^3. 
~(v=x) /\ ~(u=x) /\ (~(collinear {x, v, u}))
==>
azim (x:real^3) (v:real^3) (u:real^3) (u:real^3) = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
REWRITE_TAC[azim_def] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SELECT_UNIQUE 
THEN REWRITE_TAC[BETA_THM] THEN GEN_TAC THEN EQ_TAC
THENL[
  REPEAT STRIP_TAC 
    THEN MP_TAC (ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `y:real`; `h1:real`; `h2:real`]collinear_imp_azim_is_rezo_fan) 
    THEN ASM_REWRITE_TAC[]; 
  DISCH_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC 
    THENL[
      REAL_ARITH_TAC; 
      STRIP_TAC
	THENL[
	  ASSUME_TAC(PI_WORKS) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
	  MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `u:real^3`] AZIM_EXISTS)
	    THEN ASM_REWRITE_TAC[]  
	    THEN STRIP_TAC 
	    THEN EXISTS_TAC `h1:real` 
	    THEN EXISTS_TAC `h2:real`
	    THEN MP_TAC (ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `theta:real`; `h1:real`; `h2:real`]collinear_imp_azim_is_rezo_fan) 
	    THEN ASM_REWRITE_TAC[]
	    THEN POP_ASSUM MP_TAC  
	    THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN (LABEL_TAC "b")
	    THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[]]]]);;

let SINCOS_PRINCIPAL_VALUE_FAN = prove(
`!x:real. ?y:real. (&0<= y /\ y < &2* pi) /\ (sin(y) = sin(x) /\ cos(y) = cos(x))`,
  GEN_TAC THEN MP_TAC(SPECL [`x:real`] SINCOS_PRINCIPAL_VALUE) THEN STRIP_TAC THEN
DISJ_CASES_TAC(REAL_ARITH`((y:real) < &0)\/ (&0 <= y)`) THENL
[ EXISTS_TAC `(y:real)+ &2 * pi` THEN ASSUME_TAC(PI_POS) 
THEN ASM_REWRITE_TAC[SIN_PERIODIC;COS_PERIODIC] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 EXISTS_TAC `(y:real)` THEN ASSUME_TAC(PI_POS) 
THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
let sin_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
  ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1 
/\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x)
==> sin psi = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN  MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan) 
	  THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DOT_LADD;DOT_LMUL] 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan) 
	  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
	  THEN ASM_REWRITE_TAC[]
          THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`; 
               REAL_ARITH`(a:real) * &1= a`]
	  THEN DISCH_TAC
          THEN MATCH_MP_TAC(ISPECL [`sin (psi:real)`;`&0`; `r1:real`] REAL_EQ_LCANCEL_IMP)  THEN ASM_REWRITE_TAC[] 
	  THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);;
let cos_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
  ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1 
/\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x)
==> cos psi = &1`,
REPEAT GEN_TAC THEN STRIP_TAC 
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)-(x:real^3)`; `r1:real`; `psi:real`; `h1:real`]module_of_vector) THEN ASM_REWRITE_TAC[] THEN 
 POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
THEN POP_ASSUM MP_TAC
  THEN MP_TAC(ISPECL[`(u:real^3)-(x:real^3)`; `e3_fan (x:real^3) (v:real^3)(u:real^3)`;`e1_fan (x:real^3) (v:real^3)(u:real^3)`]CROSS_TRIPLE) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
THEN MP_TAC(ISPECL[`(u:real^3)-(x:real^3)`; `e3_fan (x:real^3) (v:real^3)(u:real^3)`;`e2_fan (x:real^3) (v:real^3)(u:real^3)`]CROSS_TRIPLE) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
 THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_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 POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN STRIP_TAC THEN 
POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN
POP_ASSUM (fun th-> REWRITE_TAC[CROSS_SKEW;th])
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan)THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC THEN MP_TAC(ISPECL[ `e2_fan (x:real^3) (v:real^3)(u:real^3)`;`(u:real^3)-(x:real^3)`]DOT_SYM) THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2 +(a:real)=a`] THEN
MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] udot_e1_fan1) THEN ASM_REWRITE_TAC[DOT_LNEG;] THEN DISCH_TAC 
  THEN  MP_TAC(ISPECL[ `e1_fan (x:real^3) (v:real^3)(u:real^3)`;`(u:real^3)-(x:real^3)`]DOT_SYM) THEN DISCH_TAC THEN
POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN REWRITE_TAC[POW_2_SQRT_ABS;REAL_ABS_NEG] THEN
 MP_TAC(ISPECL[ `((u:real^3)-(x:real^3)) dot e1_fan (x:real^3) (v:real^3)(u:real^3)`]
  REAL_ABS_REFL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] 
  THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_TAC
THEN
 MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `r1:real`; `psi:real`; `h1:real`] sin_of_u_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH`
 (r1 * cos psi) % e1_fan x v u + (r1 * &0) % e2_fan x v u + h1 % (v - x)=
 (r1 * cos psi) % e1_fan x v u + h1 % (v - x)`] THEN DISCH_TAC THEN
  SUBGOAL_THEN`((u:real^3) - (x:real^3)) dot e1_fan x (v:real^3) u = (((r1:real) * cos (psi:real)) % e1_fan x v u + (h1:real) % (v - x)) dot e1_fan x v u` ASSUME_TAC

THENL[ASM_MESON_TAC[];

POP_ASSUM MP_TAC THEN REWRITE_TAC[DOT_LADD;DOT_LMUL] THEN POP_ASSUM MP_TAC THEN  MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e3_mul_dist_fan) THEN ASM_REWRITE_TAC[]
  THEN DISCH_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
e1_orthogonal_e3_fan) THEN ASM_REWRITE_TAC[]
  THEN DISCH_TAC THEN ASM_REWRITE_TAC[DOT_LMUL;DOT_SYM]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
e1_is_normal_fan) THEN ASM_REWRITE_TAC[]
  THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)* &1+ (b:real)*(c:real)* &0= a`] THEN REPEAT DISCH_TAC 
  THEN MP_TAC(ISPECL[`&1`;`cos (psi:real)`; `r1:real`]REAL_EQ_LCANCEL_IMP) THEN REWRITE_TAC[REAL_ARITH`(a:real)* &1=a`; REAL_ARITH`&1 = (a:real) <=> a= &1`] THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;

 

let sincos_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
  ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1 
/\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x)
==>  sin psi = &0 /\ cos psi = &1`,
MESON_TAC[cos_of_u_fan;sin_of_u_fan]);;



let sincos1_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
  ~collinear {x,v,u} /\ &0 < r1 
/\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x)
==>  sin psi = &0 /\ cos psi = &1`,

REPEAT STRIP_TAC
THEN FIND_ASSUM MP_TAC`~collinear {x,v,u:real^3}`
THEN ONCE_REWRITE_TAC[SET_RULE`{X,V,U}={U,X,V}`]
THEN DISCH_TAC
THEN FIND_ASSUM MP_TAC`~collinear {x,v,u:real^3}`
THEN ONCE_REWRITE_TAC[SET_RULE`{X,V,U}={V,X,U}`]
THEN ONCE_REWRITE_TAC[COLLINEAR_3]
THEN DISCH_TAC
THEN MRESA_TAC th3[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]
THEN MRESA_TAC sincos_of_u_fan[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`;`r1:real`; `psi:real`; `h1:real`])
;;




(****************************************************************************)
(*        the conditions to add azim                  *)
(****************************************************************************)





let sum1_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 cyclic_set {u, w1, w2} x v /\ (azim x v u w1 + azim x v w1 w2) < &2 * pi
==> 
azim x v u w2 = azim x v u w1+ azim x v w1 w2
`,
( let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in  


REPEAT GEN_TAC THEN STRIP_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set1) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set2) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`v:real^3`; `x:real^3`; `u:real^3`]COLLINEAR_3) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN  SUBGOAL_THEN `~collinear {(x:real^3),(v:real^3),(u:real^3)}/\ ~collinear {(u:real^3),(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[ASM_MESON_TAC[th];

MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim) 
  THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`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)`]) 
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN MP_TAC(SPEC `psi:real` SINCOS_PRINCIPAL_VALUE_FAN ) THEN STRIP_TAC THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`u:real^3`]AZIM_EXISTS) THEN STRIP_TAC 
THEN
POP_ASSUM (fun th-> 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)`]th)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1':real`]sincos_of_u_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 

THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `h1':real`; `h1:real`; `r1':real`; `r1:real`;
`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)`; `psi':real`; `y:real`  ] AZIM_UNIQUE)
  THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`; `h1':real`; `h2:real`; `r1':real`; `r2:real`;
`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)`; `psi':real`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) + azim x v w1 (w2:real^3)`  ] AZIM_UNIQUE) 
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THENL[ ASM_MESON_TAC[REAL_LE_ADD];


ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
     ]]));;






let sum3_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
((azim x v u w1 + azim x v w1 w2) < &2 * pi)
/\
(~collinear {(x:real^3),(v:real^3),(w1:real^3)})
/\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
/\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})
==> 
azim x v u w2 = azim x v u w1+ azim x v w1 w2
`, (let th=prove(`!x v u. {x,v,u}={v,x,u}`,SET_TAC[]) in
 (let th1=prove(`!x v u. {x,v,u}={u,x,v}`,SET_TAC[]) in

REPEAT GEN_TAC THEN STRIP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") 

THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b")

THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC

THEN USE_THEN "b" MP_TAC THEN
GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
THEN  
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim) 
  THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`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)`]) 
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN MP_TAC(SPEC `psi:real` SINCOS_PRINCIPAL_VALUE_FAN ) THEN STRIP_TAC THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`u:real^3`]AZIM_EXISTS) THEN STRIP_TAC 
THEN
POP_ASSUM (fun th-> 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)`]th)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1':real`]sincos_of_u_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 

THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `h1':real`; `h1:real`; `r1':real`; `r1:real`;
`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)`; `psi':real`; `y:real`  ] AZIM_UNIQUE)
  THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`; `h1':real`; `h2:real`; `r1':real`; `r2:real`;
`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)`; `psi':real`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) + azim x v w1 (w2:real^3)`  ] AZIM_UNIQUE) 
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THENL[
 ASM_MESON_TAC[REAL_LE_ADD];

ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]])));;


let sum2_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 cyclic_set {u, w1, w2} x v /\ azim x v u w1 <= azim x v u w2
==> 
azim x v u w2 = azim x v u w1 + azim x v w1 w2
`,

(let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in

REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN
REPEAT GEN_TAC THEN STRIP_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set1) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set2) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`v:real^3`; `x:real^3`; `u:real^3`]COLLINEAR_3) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN  SUBGOAL_THEN `~collinear {(x:real^3),(v:real^3),(u:real^3)}/\ ~collinear {(u:real^3),(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[ASM_MESON_TAC[th];
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`] azim) 
  THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`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)`]) 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`] azim) THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`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)`]) 
THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 
  THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_THEN (LABEL_TAC"b")
THEN REPEAT STRIP_TAC
   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
  THEN DISCH_THEN (LABEL_TAC"c") THEN REPEAT STRIP_TAC 
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1:real`; `psi:real`; `h1':real`]sincos_of_u_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1:real`]sincos_of_u_fan)
  THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN  DISCH_TAC THEN DISCH_TAC
  THEN REMOVE_THEN "b" MP_TAC THEN REMOVE_THEN "c" MP_TAC
  THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
  THEN REPEAT STRIP_TAC 
  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`; `h2:real`; `h2':real`; `r2':real`; `r2:real`;
`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)`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3) - azim x v u (w1:real^3)`  ] AZIM_UNIQUE) 
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC 
THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)+(b:real)-a=b`; REAL_ARITH`(&0 <= (a:real)-(b:real))<=> b<= a`] THEN MP_TAC(ISPEC `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)` REAL_NEG_LE0) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
THEN MP_TAC(ISPECL[`azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3)`;`&2 * pi`;`--azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`;`&0`]REAL_LTE_ADD2 ) 
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]));;



let sum4_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 azim x v u w1 <= azim x v u w2
/\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)})
/\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
/\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})

==> 
azim x v u w2 = azim x v u w1 + azim x v w1 w2
`,(let th=prove(`!x v u. {x,v,u}={v,x,u}`,SET_TAC[]) in
(let th1=prove(`!x v u. {x,v,u}={u,x,v}`,SET_TAC[]) in

REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN

REPEAT GEN_TAC THEN STRIP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a1") 

THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b1")

THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC

THEN USE_THEN "b1" MP_TAC THEN
GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`] azim) 
  THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`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)`]) 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`] azim) THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`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)`]) 
THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 
  THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_THEN (LABEL_TAC"b")
THEN REPEAT STRIP_TAC
   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
  THEN DISCH_THEN (LABEL_TAC"c") THEN REPEAT STRIP_TAC 
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1:real`; `psi:real`; `h1':real`]sincos_of_u_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1:real`]sincos_of_u_fan)
  THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN  DISCH_TAC THEN DISCH_TAC
  THEN REMOVE_THEN "b" MP_TAC THEN REMOVE_THEN "c" MP_TAC
  THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
  THEN REPEAT STRIP_TAC
  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`; `h2:real`; `h2':real`; `r2':real`; `r2:real`;
`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)`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3) - azim x v u (w1:real^3)`  ] AZIM_UNIQUE) 
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)+(b:real)-a=b`; REAL_ARITH`(&0 <= (a:real)-(b:real))<=> b<= a`] THEN MP_TAC(ISPEC `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)` REAL_NEG_LE0) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
THEN MP_TAC(ISPECL[`azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3)`;`&2 * pi`;`--azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`;`&0`]REAL_LTE_ADD2 ) 
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC
)));;



let sum5_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
  azim x v  w1 w2 <= azim x v u w2
/\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)})
/\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
/\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})

==> 
azim x v u w2 = azim x v u w1 + azim x v w1 w2
`,
REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC"1") THEN REPEAT STRIP_TAC
  THEN DISJ_CASES_TAC(REAL_ARITH`(azim x v u w2)= &0 \/ ~(azim x v u w2 = &0)`)
THENL(*1*)[
SUBGOAL_THEN`azim x v w1 w2 = &0` ASSUME_TAC
THENL(*2*)[
REPEAT(POP_ASSUM MP_TAC) THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]azim) THEN REAL_ARITH_TAC;
(*2*)
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_EQ_0_SYM) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w2:real^3`]AZIM_EQ_0_SYM) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
SUBGOAL_THEN`azim x v w2 w1 = azim x v w2 u` ASSUME_TAC
THENL(*3*)[ASM_MESON_TAC[];(*3*)
REWRITE_TAC[REAL_ARITH`&0 = a + &0 <=> a= &0`] THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w2:real^3`;`u:real^3`;`w1:real^3`]AZIM_EQ_ALT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w1:real^3`]AZIM_EQ_0) THEN ASM_REWRITE_TAC[]]];
 DISJ_CASES_TAC(REAL_ARITH`(azim x v w1 w2)= &0 \/ ~(azim x v w1 w2 = &0)`)
THENL(*4*)[
ASM_REWRITE_TAC[REAL_ARITH`b = a + &0 <=> b= a`] THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[]THEN ASM_MESON_TAC[AZIM_EQ_ALT]  ;(*4*)
REMOVE_THEN"1" MP_TAC THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_COMPL
) THEN ASM_REWRITE_TAC[]  
  THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w2:real^3`]AZIM_COMPL
) THEN ASM_REWRITE_TAC[REAL_ARITH`a=b-c <=> c= b-a`] THEN DISCH_TAC THEN DISCH_TAC
  THEN ASM_REWRITE_TAC[REAL_ARITH`a-b=c+a-d<=> d=b+c`;REAL_ARITH`a-b<=a-d<=> d<=b`] THEN ASM_MESON_TAC[sum4_azim_fan]]
]);;





(****************************************************************************)
(*        sigma_fan is permutes                                            *)
(****************************************************************************)


let  SUR_SIGMA_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)
==> ?w.  {v,w} IN E /\sigma_fan x V E v w= u
`,
REPEAT GEN_TAC THEN STRIP_TAC 
THEN DISJ_CASES_TAC(SET_RULE `(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})`)
THENL(*1*)[
EXISTS_TAC`u:real^3` THEN ASM_REWRITE_TAC[sigma_fan];(*1*)

MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]properties_of_set_of_edge_fan) 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)`;` (u:real^3)`]exists_inverse_sigma_fan_alt) THEN ASM_REWRITE_TAC[azim1;] THEN STRIP_TAC THEN
MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]properties_of_set_of_edge_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[] 
  THEN MATCH_MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`] UNIQUE_SIGMA_FAN)
  THEN ASM_REWRITE_TAC[] 
  THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "be") THEN DISCH_TAC
THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w} \/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w})`)
THENL(*2*)[
FIND_ASSUM(MP_TAC)`u:real^3 IN set_of_edge v V E` THEN POP_ASSUM(fun th->REWRITE_TAC[th;IN_SING]) THEN ASM_TAC THEN SET_TAC[] ;(*2*)

ASM_REWRITE_TAC[] THEN GEN_TAC THEN STRIP_TAC THEN
DISJ_CASES_TAC(SET_RULE`~(azim (x:real^3) v w u <= azim x v w w1)\/ (azim (x:real^3) v w u <= azim x v w w1)`)
THENL(*3*)[
ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`azim (x:real^3) v w w1 <= azim x v w u` ASSUME_TAC
THENL(*4*)[
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*4*)
 SUBGOAL_THEN `{(w:real^3),(w1:real^3),(u:real^3)} SUBSET set_of_edge v V E` ASSUME_TAC
THENL(*5*)[
ASM_TAC THEN SET_TAC[];(*5*)
FIND_ASSUM(MP_TAC)`FAN((x:real^3),V,E)` THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "b") THEN STRIP_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) 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)`]CYCLIC_SET_EDGE_FAN) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(w:real^3), (w1:real^3),(u:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
		THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`;`u:real^3`]sum2_azim_fan) THEN ASM_REWRITE_TAC[]
  THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`]azim) THEN STRIP_TAC THEN STRIP_TAC
  THEN SUBGOAL_THEN`azim (x:real^3) v w1 u <= azim x v w u` ASSUME_TAC
THENL(*6*)[ REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*)
POP_ASSUM MP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[]) THEN ASM_REWRITE_TAC[] THEN
MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(w1:real^3)`]properties_of_set_of_edge)
THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC 
 THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),w1}`th) THEN ASSUME_TAC(th))
  THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
  THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
THEN
  DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (u:real^3) (w1:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (u:real^3) (w1:real^3) = &0)`)
THENL(*7*)[
MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`w1:real^3`]UNIQUE_AZIM_0_POINT_FAN) 
THEN ASM_TAC THEN SET_TAC[];(*7*)

  DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (u:real^3) (w:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (u:real^3) (w:real^3) = &0)`)
THENL(*8*)[
MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`w:real^3`]UNIQUE_AZIM_0_POINT_FAN) 
THEN ASM_TAC THEN SET_TAC[];(*8*)
 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w1:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[]
   THEN  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[]
   THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
   THEN FIND_ASSUM(MP_TAC o (SPEC`w1:real^3`))`!w1:real^3.  w1 IN set_of_edge v V E /\ ~(w1 = u)
           ==> &2 * pi - azim x v u w <= &2 * pi - azim x v u w1` 
 THEN REMOVE_THEN "be" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`~(w1:real^3=u)\/ (w1=u)`)
THENL(*9*)[
ASM_REWRITE_TAC[REAL_ARITH`&2 * pi -(a:real)<= &2 *pi - b <=> b <= a`] THEN DISJ_CASES_TAC(SET_RULE `(azim(x:real^3) v u w =azim x v u w1)\/ ~(azim(x:real^3) v u w =azim x v u w1)`) 
THENL(*10*)[
MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`;`(w1:real^3)`]UNIQUE_AZIM_POINT_FAN) THEN ASM_REWRITE_TAC[];(*10*)
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC](*10*);(*9*)
SUBGOAL_THEN `azim (x:real^3) v w u= azim x v w w1` ASSUME_TAC
THENL(*10*)[POP_ASSUM(fun th->REWRITE_TAC[th]);(*10*)
REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC](*10*)(*9*)](*8*)](*7*)](*6*)](*5*)](*4*)](*3*);
ASM_TAC THEN SET_TAC[]]]]);;





let MONO_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
FAN(x,V,E) /\ ({v,u} IN E)
/\ ({v,w} IN E)/\
 (sigma_fan x V E v u= sigma_fan x V E v w)
==> u=w
`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") 
THEN USE_THEN "1" MP_TAC THEN REWRITE_TAC[FAN;fan6] 
THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN 
DISCH_THEN (LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(LABEL_TAC "b") 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)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})\/ ~((set_of_edge v V E={u}))`)
THENL(*1*)[
POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM] 
THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[] 
THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM]
THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`w:real^3`th)) 
THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM]
THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(w:real^3)}`th)) 
  THEN ASM_TAC THEN SET_TAC[];(*1*)

DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(w:real^3)})\/ ~((set_of_edge v V E={w}))`)
THENL(*2*)[

POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM] 
THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[] 
THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM]
THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`u:real^3`th)) 
THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM]
THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)) 
  THEN ASM_TAC THEN SET_TAC[];(*2*)


MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`]properties_of_set_of_edge)
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (w:real^3)`]properties_of_set_of_edge)
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIGMA_FAN)
THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(w:real^3)`th))
THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]SIGMA_FAN)
THEN ASM_REWRITE_TAC[] THEN STRIP_TAC 
  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(u:real^3)`th))
  THEN ASM_REWRITE_TAC[] 
THEN MP_TAC (ISPECL[`(v: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) (w:real^3))`]properties_of_set_of_edge)
THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC 
 THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))}`th) THEN ASSUME_TAC(th))
  THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[] 
  THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ u=w`)

THENL(*3*)[
ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `{(w:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(u:real^3)}SUBSET set_of_edge v V E` ASSUME_TAC
THENL(*4*)[ ASM_TAC THEN SET_TAC[];(*4*)

MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(w:real^3), (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(u:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
		THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]sum2_azim_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "c") THEN
  DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))= &0) \/ ~(azim (x:real^3)  (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = &0)`)

THENL(*5*)[
MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]UNIQUE_AZIM_0_POINT_FAN) 
THEN ASM_TAC THEN SET_TAC[];(*5*)

DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (w:real^3) (u:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (w:real^3) (u:real^3) = &0)`)

THENL(*6*)[

MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(u:real^3)`]UNIQUE_AZIM_0_POINT_FAN) 
THEN ASM_TAC THEN SET_TAC[];(*6*)

  DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3)  (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (u:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (u:real^3) = &0)`)

THENL(*7*)[
MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]UNIQUE_AZIM_0_POINT_FAN) 
THEN ASM_TAC THEN SET_TAC[];(*7*)

MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]AZIM_COMPL) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`]AZIM_COMPL) THEN 
ASM_REWRITE_TAC[REAL_ARITH`&2 * pi - ((a:real)+(b:real))= --(a:real)+ (&2 * pi - b)`] THEN DISCH_TAC 
THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_ARITH`b <= (a:real)+(b:real)<=> &0 <= a`]
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`] azim)THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC
(*7*)](*6*)](*5*)](*4*)];(*3*)

ASM_REWRITE_TAC[](*3*)]]]);;



let permutes_sigma_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)
==>
(extension_sigma_fan x V E v) permutes (set_of_edge v V E)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`FAN((x:real^3), V, E)` THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC
THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`]remark_finite_fan1)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`;`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)`]PERMUTES_FINITE_INJECTIVE)
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THENL[
GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan];
STRIP_TAC
THENL[
GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(x':real^3)}\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(x':real^3)})`)
THENL[ASM_REWRITE_TAC[sigma_fan;IN_SING];
ASM_MESON_TAC[SIGMA_FAN]];
REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (x':real^3)`]properties_of_set_of_edge)
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (y:real^3)`]properties_of_set_of_edge)
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
ASM_MESON_TAC[MONO_SIGMA_FAN]]]);;





(****************************************************************************)
(*        inverse of sigma_fan                                             *)
(****************************************************************************)








  





let exists_function_inverse_sigma_fan_alt=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
FAN(x,V,E) ==> 
(?g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
/\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
/\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w))
`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] sigma_fan_in_set_of_edge) THEN 
 ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`; `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]BIJECTIVE_ON_LEFT_RIGHT_INVERSE)
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] properties_of_set_of_edge_fan) THEN 
 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] 

THEN
MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] MONO_SIGMA_FAN) 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)`] SUR_SIGMA_FAN) THEN 
 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
(*
This is the same as inverse_sigma_fan_alt,
but easier to use.
*)



let inverse1_sigma_fan=new_definition`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)= @g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
/\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
/\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;


let INVERSE1_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
FAN(x,V,E) ==> 
( (!w:real^3. {v,w} IN E==> {v, inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) w} IN E)
/\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) w) =w)
/\ (!w:real^3. {v,w} IN E==> inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (sigma_fan x V E v w) =w))`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[inverse1_sigma_fan] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3) `]exists_function_inverse_sigma_fan_alt)
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC  THEN EXISTS_TAC`g:real^3->real^3` THEN ASM_REWRITE_TAC[]);;
(* This is the same as f_fan, 
   but easier to use *)

let f1_fan=new_definition`f1_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse1_sigma_fan x V E w v),v) )`;;

(* Proof Lemma 6.1 [AAUHTVE] *)

let node_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) n:num. power_maps n_fan x V E n=power_n_fan x V E n`,
GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[power_maps; n_fan; power_n_fan; power_map_points] THEN INDUCT_TAC THEN REWRITE_TAC[power_maps; power_map_points;i_fan;] THEN REWRITE_TAC[power_map_points; power_maps] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[n_fan;o_funs; pr1; pr2; pr3; pr4]);;




let EQ_PAIR_4=prove(`!a:real^3 b:real^3 c:real^3 d:real^3 a1:real^3 b1:real^3 c1:real^3 d:real^3.
(a,b,c,d)=(a1,b1,c1,d1) <=> a=a1 /\ b=b1 /\ c=c1 /\ d=d1`,
REPEAT GEN_TAC THEN EQ_TAC
THENL[
DISCH_TAC THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr1(a,b,c,d)=pr1(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr1]
  THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr2(a,b,c,d)=pr2(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr2] THEN 
MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr3(a,b,c,d)=pr3(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr3] THEN 
MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr4(a,b,c,d)=pr4(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr4] THEN ASM_REWRITE_TAC[] 
  THEN SET_TAC[];
SET_TAC[]]);;


let MONO_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)`,

REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[n_fan;EQ_PAIR_4]
  THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th -> REWRITE_TAC[]) 
  THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_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 ASM_REWRITE_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 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[MONO_SIGMA_FAN;]);;

let SUR_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))`,

REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN 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`] SUR_SIGMA_FAN) 
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN EXISTS_TAC`(x:real^3,v:real^3,w':real^3,w:real^3)`
  THEN ASM_REWRITE_TAC[n_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`v:real^3`
  THEN EXISTS_TAC`w':real^3` THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);; 



let simp_inverse_sigma_fan_alt=prove(`!x V E v w.
inverse_sigma_fan_alt x V E v w= inverse (sigma_fan x V E v) w`,
REWRITE_TAC[inverse] THEN MESON_TAC[inverse_sigma_fan_alt]);;


let SUR_F1_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC
  THEN EXISTS_TAC`(x:real^3,sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w, v:real^3,sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  v w) v)`
  THEN ASM_REWRITE_TAC[f_fan;EQ_PAIR_4;]
 THEN STRIP_TAC
THENL[
EXISTS_TAC`x:real^3` THEN EXISTS_TAC`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w`
  THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  v w) v`
THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ={w:real^3}) \/ ~(set_of_edge v V E ={w})`)
THENL[
REWRITE_TAC[sigma_fan;SET_RULE`{a,b}={b,a}`] THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) 
THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[])
THEN POP_ASSUM (fun th-> REWRITE_TAC[th]);

MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3`]remark1_fan)
  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`]SIGMA_FAN)
  THEN ASM_REWRITE_TAC[remark1_fan] THEN STRIP_TAC
  THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`sigma_fan x V E v w:real^3`;`v:real^3`]remark1_fan)
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]];

REWRITE_TAC[f1_fan] THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`]INVERSE1_SIGMA_FAN)
  THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th))
  THEN ASM_REWRITE_TAC[]]);;




let MONO_F1_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[f1_fan;EQ_PAIR_4]
  THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;

let MONO_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan;EQ_PAIR_4]
  THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;

let SUR_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))`,

REWRITE_TAC[d1_fan; IN_ELIM_THM] THEN REPEAT STRIP_TAC
 THEN EXISTS_TAC`(x:real^3,w:real^3,v:real^3, sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v)` 
THEN ASM_REWRITE_TAC[e_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3`
  THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v`
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]);;





let permuters_of_enf_fan=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)
/\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))
/\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)
/\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))
/\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)
/\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))
`,MESON_TAC[MONO_N_FAN;SUR_N_FAN;MONO_F1_FAN;SUR_F1_FAN;MONO_E_FAN;SUR_E_FAN]);;








let condition_hypermap_fan=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool). 
FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==> e_fan x V E((n_fan x V E) (f1_fan x V E a))=a)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[f1_fan;n_fan; e_fan; EQ_PAIR_4]
  THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`]INVERSE1_SIGMA_FAN)
  THEN ASM_REWRITE_TAC[]
  THEN STRIP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[])
  THEN POP_ASSUM (fun th-> MP_TAC(ISPEC`v:real^3`th))
  THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]
  THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;


let plain_hypermap_fan=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool). 
FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==>
(e_fan x V E)  (e_fan x V E a) =a)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]);;

let e_fan_no_fix_point=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]
 THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
  THEN ASM_MESON_TAC[]);;
let f_fan_no_fix_point=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[f1_fan; EQ_PAIR_4] 
THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
  THEN ASM_MESON_TAC[]);;


(* from hypermap.hl *)

(******************************)
parse_as_infix("POWER",(24,"right"));;

let POWER = new_recursive_definition num_RECURSION 
 `(!(f:A->A). f POWER 0  = I) /\  
  (!(f:A->A) (n:num). f POWER (SUC n) = (f POWER n) o f)`;;
let POWER_0 = prove(`!f:A->A. f POWER 0 = I`,
 REWRITE_TAC[POWER]);;
let POWER_1 = prove(`!f:A->A. f POWER 1 = f`,
 REWRITE_TAC[POWER; ONE; I_O_ID]);;
let POWER_2 = prove(`!f:A->A. f POWER 2 = f o f`,
 REWRITE_TAC[POWER; TWO; POWER_1]);;
let orbit_map = new_definition `orbit_map (f:A->A)  (x:A) = {(f POWER n) x | n >= 0}`;;(**************************************************)

let POWER_RIGHT=prove(`!k:num f:A->A. f POWER SUC(k) = f o (f POWER k)`,
INDUCT_TAC
THENL[REWRITE_TAC[POWER;o_DEF; I_DEF];
REWRITE_TAC[POWER;o_ASSOC] THEN GEN_TAC THEN POP_ASSUM(fun th -> MP_TAC(SPEC`f:A->A`th)) THEN DISCH_TAC
 THEN 
POP_ASSUM(fun th-> REWRITE_TAC[SYM(th);POWER])]) ;;


let power_n_fan=prove(`!l:num 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)==> 
(n_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) POWER l) (x,v,w,sigma_fan x V E v w)= (x,v, power_map_points sigma_fan x V E v w l, power_map_points sigma_fan x V E v w (SUC l) )`,
INDUCT_TAC
THENL[REWRITE_TAC[POWER; power_map_points;I_DEF];
POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT STRIP_TAC THEN
  REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;`(w:real^3)`]th)) 
THEN ASM_REWRITE_TAC[POWER_RIGHT; o_DEF;]
THEN DISCH_TAC THEN ASM_REWRITE_TAC[n_fan;power_map_points] ]);;


let distinct_nodes=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) .
FAN(x,V,E)==> (!k:num l:num a. a IN d1_fan(x,V,E) ==>
(((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC  THEN
ASM_REWRITE_TAC[o_DEF;e_fan]  THEN
MP_TAC(ISPECL[`l:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`k:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` w:real^3`;` v:real^3`]power_n_fan)
  THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC
  THEN POP_ASSUM(fun th-> REWRITE_TAC[])   THEN POP_ASSUM(fun th-> REWRITE_TAC[])
  THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(th))
  THEN ASM_REWRITE_TAC[power_map_points] THEN  POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]));;



let edge_lie_different_nodes=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool). 
FAN(x,V,E)==> (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a)) `,

REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC  THEN
ASM_REWRITE_TAC[e_fan]  THEN
MP_TAC(ISPECL[`n:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4]
  THEN STRIP_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
  THEN ASM_MESON_TAC[]);;



(**********************)


let d20_fan=new_definition`d20_fan (x,V,E)={ (x',v,v,v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
let d_fan=new_definition`d_fan (x,V,E)= d1_fan (x,V,E) UNION d20_fan (x,V,E)`;;
let hypermap_of_fanx = new_definition
  `hypermap_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) = 
    (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in 
          hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f_fan))`;;

let hypermap1_of_fanx = new_definition
  `hypermap1_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) = 
    (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in 
          hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f1_fan))`;;



let finite_d1_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) ==> FINITE (d1_fan (x,V,E))`,
REPEAT GEN_TAC
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "EM" MP_TAC
THEN REWRITE_TAC[FAN;fan1]
THEN STRIP_TAC
THEN MRESA_TAC set_edges_is_finite_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MRESA_TAC FINITE_PRODUCT[`V:real^3->bool`;`V:real^3->bool`]
THEN MRESA_TAC FINITE_IMAGE[`(\(a,b:real^3). (x,a,b,sigma_fan x V E a b))`;`{x,y | x IN (V:real^3->bool) /\ y IN V}`]
THEN MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`(IMAGE (\(a,b). x,a,b,sigma_fan x V E a b) {x,y | x IN V /\ y IN (V:real^3->bool)})`
THEN ASM_REWRITE_TAC[IMAGE;IN_ELIM_THM;d1_fan;SUBSET]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`(v:real^3,w:real^3)`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`w:real^3`
THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`]
THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;


let finite_d20_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) ==> FINITE (d20_fan (x,V,E))`,

REPEAT GEN_TAC
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "EM" MP_TAC
THEN REWRITE_TAC[FAN;fan1]
THEN STRIP_TAC
THEN MRESA_TAC FINITE_IMAGE[`(\b:real^3. (x:real^3,b,b,b))`;`V:real^3->bool`]
THEN MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`(IMAGE (\b:real^3. (x:real^3,b,b,b))  (V:real^3->bool))`
THEN ASM_REWRITE_TAC[d20_fan;SUBSET;IMAGE;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`v:real^3`
THEN ASM_REWRITE_TAC[IN]);;


let finite_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) 
==> FINITE (d_fan (x,V,E))`,
REPEAT STRIP_TAC
THEN REWRITE_TAC[d_fan;FINITE_UNION]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[finite_d1_fan;finite_d20_fan]);;
let subset_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
d1_fan (x,V,E) SUBSET d_fan (x,V,E) /\ d20_fan (x,V,E) SUBSET d_fan(x,V,E)`,
REWRITE_TAC[d_fan] THEN SET_TAC[]);;

let FACE_FAN_NOT_EMPTY=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s.
FAN(x,V,E)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
==> ~(ds={})`,
REPEAT STRIP_TAC 
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`]
THEN MRESA_TAC FACE_FINITE[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]
THEN STRIP_TAC
THEN MRESA1_TAC CARD_EQ_0`face (hypermap1_of_fanx (x:real^3,V,E)) x'`
THEN MRESA_TAC FACE_NOT_EMPTY[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC);;






let into_domain_e_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
==> (!y. y IN d_fan (x,V,E)==> ((p e_fan ) y) IN (d_fan (x,V,E)))`,
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[res;]
THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
THENL[
ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MATCH_MP_TAC(SET_RULE`x,w,v,sigma_fan x V E w v IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
==>x,w,v,sigma_fan x V E w v IN  d_fan (x:real^3,V,E)`)
THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
THEN EXISTS_TAC`x:real^3`
THEN EXISTS_TAC`w:real^3`
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)`
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]]);;



let into_domain1_e_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (e_fan x V E y IN d1_fan (x,V,E)))`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`x:real^3`
THEN EXISTS_TAC`w:real^3`
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)`
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]);;




let e_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
==> (p e_fan) permutes (d_fan (x,V,E))`,
REPEAT STRIP_TAC
THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (e_fan x V E) (d1_fan (x:real^3,V,E))`]
THEN STRIP_TAC
THENL[
REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[];

MRESA_TAC into_domain_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
THENL[EXISTS_TAC`y:real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[res];
MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
THEN REWRITE_TAC[res]
THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN ASM_TAC THEN SET_TAC[]]]);;
let into_domain_f1_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
==> (!y. y IN d_fan (x,V,E)==> ((p f1_fan ) y) IN (d_fan (x,V,E)))`,
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[res;]
THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
THENL[
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MATCH_MP_TAC(SET_RULE`x,w,inverse1_sigma_fan x V E w v,v IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
==>x,w,inverse1_sigma_fan x V E w v,v IN  d_fan (x:real^3,V,E)`)
THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
THEN EXISTS_TAC`x:real^3`
THEN EXISTS_TAC`w:real^3`
THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3`
THEN EXISTS_TAC`(v:real^3)`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]]);;



let into_domain1_f1_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E)==> (!y. y IN d1_fan (x,V,E)==> (f1_fan x V E y IN d1_fan (x,V,E)))`,
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
THEN STRIP_TAC
THEN EXISTS_TAC`x:real^3`
THEN EXISTS_TAC`w:real^3`
THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3`
THEN EXISTS_TAC`(v:real^3)`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]);;




let f1_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
==> (p f1_fan) permutes (d_fan (x,V,E))`,

REPEAT STRIP_TAC
THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (f1_fan x V E) (d1_fan (x:real^3,V,E))`]
THEN STRIP_TAC
THENL[
REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[];
MRESA_TAC into_domain_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
THENL[
EXISTS_TAC`y:real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[res];
MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
THEN REWRITE_TAC[res]
THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN ASM_TAC THEN SET_TAC[]]]);;




let into_domain_n_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
==> (!y. y IN d_fan (x,V,E)==> ((p n_fan ) y) IN (d_fan (x,V,E)))`,
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[res;]
THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
THENL[
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MATCH_MP_TAC(SET_RULE`x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
==>x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN  d_fan (x:real^3,V,E)`)
THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
THEN EXISTS_TAC`x:real^3`
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`sigma_fan x V E v w:real^3`
THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC 
THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]]);;


let into_domain1_n_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (n_fan x V E y IN d1_fan (x,V,E)))`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`x:real^3`
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`sigma_fan x V E v w:real^3`
THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC 
THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]);;


let n_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
==> (p n_fan) permutes (d_fan (x,V,E))`,

REPEAT STRIP_TAC
THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (n_fan x V E) (d1_fan (x:real^3,V,E))`]
THEN STRIP_TAC
THENL[
REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[];
MRESA_TAC into_domain_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
THENL[
EXISTS_TAC`y:real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[res];
MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
THEN REWRITE_TAC[res]
THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN ASM_TAC THEN SET_TAC[]]]);;

let id_enf_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3.
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E))
==> (p e_fan) y=y /\ (p n_fan) y=y/\ (p f1_fan) y=y`,
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]);;
let id_power_enf_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3 n:num p.
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E))
==> ((p e_fan) POWER n) y=y /\ ((p n_fan) POWER n)y=y/\ ((p f1_fan) POWER n) y=y`,
(let lem=prove(`!f:A->A x:A. f x = x ==> !m. (f POWER m) x = x`,
MRESA_TAC power_map_fix_point[`1:num`]
THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[POWER_1;ARITH_RULE`m*1=m:num`]) in
REPEAT STRIP_TAC
THEN MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`y:real^3#real^3#real^3#real^3`]
THEN MRESA_TAC lem[`(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
THEN MRESA_TAC lem[`(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
THEN MRESA_TAC lem[`(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]));;



let into_domain_efn_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) 
==> (!y. y IN d1_fan (x,V,E)==> (p e_fan ) y = e_fan x V E y)
/\ (!y. y IN d1_fan (x,V,E)==> (p n_fan ) y = n_fan x V E y)
/\(!y. y IN d1_fan (x,V,E)==> (p f1_fan ) y = f1_fan x V E y)
`,
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[res;]);;



let power_map_fix_set = prove(`!n f:A->A g:A->A s:A->bool. (!x:A. x IN s ==>  f x= g x) /\ (!x:A. x IN s ==> g x IN s) ==> (!x. x IN s==>(f POWER n) x = (g POWER n) x)`,
 INDUCT_TAC THENL[REWRITE_TAC[MULT; POWER; I_THM];
    REWRITE_TAC[POWER; o_DEF] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN DISCH_THEN(LABEL_TAC"NHO")  THEN DISCH_TAC
THEN REMOVE_THEN "YEU" (fun th -> MRESA_TAC th[`f:A->A`;`g:A->A`;`s:A->bool`])
THEN POP_ASSUM (fun th-> MRESA1_TAC th `g (x:A):A`)
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN "EM"  (fun th -> MRESA1_TAC th `x:A`)
THEN REMOVE_THEN "NHO"  (fun th -> MRESA1_TAC th `x:A`)]);;





let into_domain_power_efn_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num p.
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) 
==> (!y. y IN d1_fan (x,V,E)==> ((p e_fan ) POWER n)y = ((e_fan x V E) POWER n) y)
/\ (!y. y IN d1_fan (x,V,E)==> ((p n_fan ) POWER n) y = ((n_fan x V E) POWER n) y)
/\(!y. y IN d1_fan (x,V,E)==> ((p f1_fan ) POWER n) y = ((f1_fan x V E) POWER n) y)`,
REPEAT GEN_TAC THEN REPEAT DISCH_TAC
THEN MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN MRESA_TAC power_map_fix_set[`n:num`;
`(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
`(e_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]
THEN MRESA_TAC power_map_fix_set[`n:num`;
`(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
`(n_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]
THEN MRESA_TAC power_map_fix_set[`n:num`;
`(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
`(f1_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]);;



let power_fun_in_domain=prove(`!n f:A->A s:A->bool.(!y. y IN s==> f y IN s)==> (!y. y IN s==> (f POWER n) y IN s)`,
 INDUCT_TAC THENL[REWRITE_TAC[POWER_0; I_THM];
POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU")
THEN REPEAT STRIP_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`f:A->A`;`s:A->bool`])
THEN REWRITE_TAC[COM_POWER;o_DEF]
THEN POP_ASSUM  (fun th-> MRESA1_TAC th`y:A`)]);;


let into_domain1_power_efn_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num.
FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (((e_fan x V E) POWER n) y IN d1_fan (x,V,E)))
/\ (!y. y IN d1_fan (x,V,E)==> (((n_fan x V E) POWER n) y IN d1_fan (x,V,E)))
/\(!y. y IN d1_fan (x,V,E)==> (((f1_fan x V E) POWER n) y IN d1_fan (x,V,E)))`,
REPEAT GEN_TAC THEN DISCH_TAC
THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
THEN MRESA_TAC power_fun_in_domain[`n:num`;`e_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]
THEN MRESA_TAC power_fun_in_domain[`n:num`;`f1_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]
THEN MRESA_TAC power_fun_in_domain[`n:num`;`n_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]);;





let lemma_hypermap1_of_fanx=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) )  ==>
(p e_fan) o (p n_fan) o (p f1_fan)= I`,
REPEAT STRIP_TAC
THEN MATCH_MP_TAC EQ_EXT
THEN ASM_REWRITE_TAC[I_THM;o_DEF]
THEN GEN_TAC
THEN DISJ_CASES_TAC(SET_RULE`~(x' IN d1_fan (x,V,E) )\/ (x' IN d1_fan (x:real^3,V,E))`)
THENL[
MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x':real^3#real^3#real^3#real^3`];
MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` )
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"YEU")
THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )
THEN RESA_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `(n_fan x V E (f1_fan x V E x')):real^3#real^3#real^3#real^3` )
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` )
THEN RESA_TAC
THEN MRESA_TAC condition_hypermap_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )]);;








let hypermap_of_fan_rep=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) p.
FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) )  ==>
dart ( hypermap1_of_fanx (x,V,E)) =d_fan (x,V,E)  /\ edge_map (hypermap1_of_fanx (x,V,E)) = p e_fan  /\ node_map (hypermap1_of_fanx (x,V,E)) = p n_fan /\ face_map (hypermap1_of_fanx (x,V,E)) = p f1_fan `,
REPEAT GEN_TAC THEN DISCH_TAC
THEN REWRITE_TAC[hypermap1_of_fanx]
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
THEN MRESA_TAC e_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
THEN MRESA_TAC n_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
THEN MRESA_TAC f1_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
THEN MRESA_TAC lemma_hypermap1_of_fanx[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
THEN MRESA_TAC lemma_hypermap_rep[`d_fan (x:real^3,V,E):real^3#real^3#real^3#real^3->bool`;
`(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
`(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
`(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`]);;
let properties_of_f1_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y y1.
FAN(x,V,E) /\ y = f1_fan x V E y1 /\ y1 IN d1_fan (x,V,E)
==> pr3 y1 =pr2 y /\ {pr2 y1, pr3 y1} IN E /\ {pr2 y, pr3 y} IN E /\
pr2 y1= sigma_fan x V E (pr2 y) (pr3 y)`,
REPEAT GEN_TAC 
THEN STRIP_TAC 
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[d1_fan; IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[pr2;pr3;f1_fan]
THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`w:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]);;


let face_subset_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
FAN(x,V,E)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
==> ds SUBSET d_fan (x,V,E)`,
REPEAT GEN_TAC THEN STRIP_TAC
THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`]
THEN MRESA_TAC hypermap_of_fan_rep[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x V E) (d1_fan (x,V,E)))`]
THEN MRESA_TAC lemma_face_subset[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]);;



let properties_of_elements_in_face_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
FAN(x,V,E)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
/\ y IN ds
==> {pr2 y, pr3 y} IN E\/ pr2 y= pr3 y`,
REPEAT GEN_TAC THEN STRIP_TAC
THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`]
THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[d_fan;d1_fan;d20_fan;UNION;IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[pr2;pr3]);;
let fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
/\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
==> d20_fan(x,V,E)={}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
THEN REWRITE_TAC[SET_RULE`A={}<=> ~(?y. y IN A)`]
THEN REWRITE_TAC[d20_fan;IN_ELIM_THM]
THEN STRIP_TAC
THEN REMOVE_THEN "YEU"(fun th-> MRESAL1_TAC th`v:real^3`[IN;CARD_CLAUSES])
THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;



let dartset_fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
FAN(x,V,E)
/\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
==> d_fan(x,V,E)=d1_fan(x,V,E)`,
REPEAT STRIP_TAC 
THEN MRESA_TAC fully_surrounded_is_non_isolated_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
THEN ASM_REWRITE_TAC[d_fan;]
THEN SET_TAC[]);;

let properties_of_elements_in_face_fully_surroundedfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
FAN(x,V,E)
/\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
/\ y IN ds
==> {pr2 y, pr3 y} IN E`,
REPEAT GEN_TAC THEN STRIP_TAC
THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`]
THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC 
THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
THEN REWRITE_TAC[d1_fan;IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[pr2;pr3]);;


let AAUHTVE=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) p. 
FAN(x,V,E)/\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==> 
FINITE (d_fan (x,V,E)) 
/\ (p e_fan) permutes (d_fan (x,V,E))
/\ (p n_fan) permutes (d_fan (x,V,E))
/\ (p f1_fan) permutes (d_fan (x,V,E))
/\(p e_fan) o (p n_fan) o (p f1_fan)= I
/\ (!a. a IN d1_fan(x,V,E)==> (e_fan x V E)  (e_fan x V E a) =a)
/\ (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))
/\ (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))
/\ (!k:num l:num a. a IN d1_fan(x,V,E) ==>
(((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)

/\ (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a))`,

MESON_TAC[lemma_hypermap1_of_fanx;e_fan_permutes;n_fan_permutes;finite_d_fan;f1_fan_permutes;plain_hypermap_fan;e_fan_no_fix_point;f_fan_no_fix_point;distinct_nodes;edge_lie_different_nodes]);;
(********************************)


end;;