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




module  Cfyxfty = struct









open Sphere;;
open Fan_defs;;
open Hypermap;;
open Vol1;;
open Fan;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Sphere;;
open Hypermap;;
open Fan;;
open Topology;;
open Polyhedron;;
open Prove_by_refinement;;
open Nkezbfc_local;;



let EDGES0_FAN=new_definition`EDGES0_FAN (p:real^3->bool) f1={e | e IN (edges p) /\ ~(aff_gt {vec 0} e INTER closure(fchanged f1)={})}`;;



let CONVEX_CLOSURE_DARTSET_LEADS_INTO_FAN=
prove(`
!p:real^3->bool f1:real^3#real^3#real^3#real^3->bool U:real^3->bool.
 bounded p /\ polyhedron p /\ vec 0 IN interior p 
/\ f1 IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p)) 
/\
dartset_leads_into_fan (vec 0) (vertices p) (edges p) f1 =U
==> convex(closure U)`,


REPEAT STRIP_TAC
THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
THEN MRESA1_TAC CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH")
THEN MRESA1_TAC POLYTOPE_FAN80`p:real^3->bool`
THEN MRESAL_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;][conforming_fan;conforming_half_space_fan]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`f1:real^3#real^3#real^3#real^3->bool`)
THEN MATCH_MP_TAC CONVEX_CLOSURE
THEN MATCH_MP_TAC CONVEX_INTERS
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MESON_TAC[CONVEX_AFF_GT]);;

let WBLARHH_BIJ = 
prove_by_refinement(
  `!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==>
 (BIJ 
   (dartset_leads_into_fan (vec 0) (vertices p) (edges p)) 
   (face_set (hypermap1_of_fanx(vec 0,vertices p,edges p))) 
   (topological_component_yfan (vec 0,vertices p, edges p)))`,

  (* {{{ proof *)
  [
REWRITE_TAC [BIJ;INJ;SURJ;IN;IN_ELIM_THM];
GEN_TAC ;
STRIP_TAC ;
MRESA_TAC (REWRITE_RULE[IN] POLYHEDRON_FAN) [`p:real^3->bool`;`vec 0:real^3`];
MRESA1_TAC (REWRITE_RULE[IN] CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON)`p:real^3->bool`;
 MRESA1_TAC (REWRITE_RULE[IN] POLYTOPE_FAN80) `p:real^3->bool`;
MRESA_TAC (REWRITE_RULE[IN] dartset_leads_into_is_topological_component_yfan) [`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`];
 MRESAL_TAC (REWRITE_RULE[IN] Conforming.PIIJBJK)[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;][REWRITE_RULE[IN] Conforming.conforming_fan;REWRITE_RULE[IN] Conforming.conforming_bijection_fan];
ASM_MESON_TAC []
  ]);;
  (* }}} *)






let CONVEX_CLOSURE_FCHANGED=
prove(`!p:real^3->bool f U.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f facet_of p /\ 							 
 fchanged f= U
==> convex(closure U)`,

REPEAT STRIP_TAC
THEN MRESA_TAC Polyhedron.FCHANGED_IN_COMPONENT[`f:real^3->bool`;`p:real^3->bool`]
THEN MRESAL1_TAC WBLARHH_BIJ`p:real^3->bool`[BIJ;SURJ]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`U:real^3->bool`)
THEN MRESAL1_TAC WBLARHH`p:real^3->bool`[]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`y:real^3#real^3#real^3#real^3->bool`)
THEN MRESA_TAC CONVEX_CLOSURE_DARTSET_LEADS_INTO_FAN[`p:real^3->bool`; `y:real^3#real^3#real^3#real^3->bool`;` U:real^3->bool`] );;

let GINGUAP=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
FAN(x,V,E)
/\ conforming_fan (x,V,E)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
==>   convex(dartset_leads_into_fan x V E ds)`,


REWRITE_TAC[conforming_fan;conforming_half_space_fan]
THEN REPEAT 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"EM")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "EM"(fun th-> MRESA1_TAC th`ds:real^3#real^3#real^3#real^3->bool`)
THEN MATCH_MP_TAC CONVEX_INTERS
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[CONVEX_AFF_GT]);;





let AFF_GT_SUBSET_DARTSET_LEADS_INTO= 
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y z.
FAN(x,V,E)
/\ conforming_fan (x,V,E)
 /\ (!v. v IN V==>CARD (set_of_edge v V E) > 1)
/\ fan80(x,V,E)
/\ ds IN face_set (hypermap1_of_fanx (x,V,E))
/\ y IN dartset_leads_into_fan x V E ds
/\ z IN dartset_leads_into_fan x V E ds
==> aff_gt {x} {y,z}  SUBSET dartset_leads_into_fan x V E ds`,

REPEAT STRIP_TAC
THEN MRESA_TAC Planarity.dartset_leads_into_is_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds:(real^3#real^3#real^3#real^3->bool)`]
THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`dartset_leads_into_fan x V E ds`;` z:real^3`]
THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`dartset_leads_into_fan x V E ds`;` y:real^3`]
THEN MRESAL_TAC GINGUAP[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds:(real^3#real^3#real^3#real^3->bool)`][CONVEX_CONTAINS_SEGMENT]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`y:real^3`;`z:real^3`][segment;SUBSET;IN_ELIM_THM])
THEN SUBGOAL_THEN`(!t. &0 < t /\ t < &1 ==> (&1 - t) % y + t % z IN yfan (x:real^3,V:real^3->bool,E))` ASSUME_TAC
THENL[
POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH")
THEN REPEAT STRIP_TAC 
THEN REMOVE_THEN "LINH" (fun th-> MRESA1_TAC th`(&1 - t) % y + t % z:real^3`)
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`(?u. (&0 <= u /\ u <= &1) /\
           (&1 - t) % y + t % z = (&1 - u) % y + u % z:real^3)` ASSUME_TAC
THENL[
EXISTS_TAC`t:real`
THEN REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC Planarity.dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds:(real^3#real^3#real^3#real^3->bool)`]
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]];
MRESAL_TAC Planarity.aff_gt_subset_component_y_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`dartset_leads_into_fan x V E ds`;`y:real^3`;`z:real^3`][SET_RULE`DISJOINT {x} {y, z}<=> ~(x=y) /\ ~(x=z)`;SUBSET]]);;

let FACET_SUBSET_CLOSURE_FCHANGED=
prove(`!p:real^3->bool f.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f facet_of p 
==> f SUBSET closure(fchanged f)`,


REPEAT STRIP_TAC
THEN MRESA_TAC Polyhedron.RELATIVE_SUBSET_FCHANGE[`p:real^3->bool`;`vec 0:real^3`;`f:real^3->bool`]
THEN MRESA_TAC FACET_OF_IMP_FACE_OF[`f:real^3->bool`;`p:real^3->bool`]
THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[POLYHEDRON_EQ_FINITE_FACES]
THEN STRIP_TAC
THEN MRESA1_TAC CONVEX_CLOSURE_RELATIVE_INTERIOR`f:real^3->bool`
THEN MRESA_TAC SUBSET_CLOSURE[`relative_interior f:real^3->bool`;`fchanged f:real^3->bool`]
THEN MRESA1_TAC CLOSURE_SUBSET`f:real^3->bool`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]);;




let MAP_EDGES_FACET_INTO_E1_FAN=
prove_by_refinement(`!p:real^3->bool f e.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f facet_of p 
/\ e IN edges f
==> e IN EDGES0_FAN p f `,


[ REWRITE_TAC[EDGES0_FAN;IN_ELIM_THM;edges]
THEN REPEAT STRIP_TAC;
ASM_TAC
THEN REWRITE_TAC[edge_of;facet_of]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[]
THEN ASM_MESON_TAC[FACE_OF_TRANS];
POP_ASSUM MP_TAC
THEN MRESA_TAC FACET_SUBSET_CLOSURE_FCHANGED[`p:real^3->bool`;`f:real^3->bool`]
THEN MRESA_TAC EDGE_OF_IMP_SUBSET[`segment [v,w:real^3]`;`f:real^3->bool`]
THEN MRESA_TAC SEGMENT_OPEN_SUBSET_CLOSED[`v:real^3`;`w:real^3`]
THEN MRESA_TAC SEGMENT_EDGE_OF[`f:real^3->bool`;`v:real^3`;`w:real^3`]
THEN ABBREV_TAC`t= &1/ &2 % v+ &1/ &2 % w:real^3`
THEN SUBGOAL_THEN`?u1. &0 < u1 /\ u1 < &1 /\ t = (&1 - u1) % v + u1 % w:real^3`
ASSUME_TAC;
EXISTS_TAC`&1/ &2`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - &1/ &2= &1/ &2`]
THEN REAL_ARITH_TAC;
MRESA_TAC IN_SEGMENT[`v:real^3`;`w:real^3`;`t:real^3`]
THEN SUBGOAL_THEN`t IN closure(fchanged f:real^3->bool)`ASSUME_TAC;
ASM_TAC
THEN SET_TAC[];
REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;INTER;IN_ELIM_THM]
THEN EXISTS_TAC`t:real^3`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC facet_of[`f:real^3->bool`;`p:real^3->bool`]
THEN MRESA_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`v:real^3`]
THEN MRESA_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`w:real^3`]
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`v:real^3`]
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`w:real^3`]
THEN MP_TAC(SET_RULE`~(v IN interior p) /\ ~(w IN interior p) /\ (vec 0 IN interior p)==> DISJOINT{vec 0} {v,w:real^3}`)
THEN RESA_TAC
THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1/ &2`
THEN EXISTS_TAC`&1/ &2`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % vec 0+ A+B=A+B`]
THEN REAL_ARITH_TAC]);;
let LIM_NULL_CMUL_BOUNDED_FAN = 
prove
 (`!f g:A->real^N B net.
        eventually (\a. abs(f a) < B) net /\
        (g --> vec 0) net
        ==> ((\n. f n % g n) --> vec 0) net`,

  REPEAT GEN_TAC THEN REWRITE_TAC[tendsto] THEN STRIP_TAC THEN
  X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e / (abs B + &1)`) THEN
  ASM_SIMP_TAC[REAL_LT_DIV; REAL_ARITH `&0 < abs x + &1`] THEN
  UNDISCH_TAC `eventually (\a. abs(f a) < B) (net:(A net))` THEN
  REWRITE_TAC[IMP_IMP; GSYM EVENTUALLY_AND] THEN
  MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MP) THEN
  REWRITE_TAC[dist; VECTOR_SUB_RZERO; o_THM; NORM_LIFT; NORM_MUL] THEN
  MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `x:A` THEN REWRITE_TAC[] THEN
  STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
  EXISTS_TAC `B * e / (abs B + &1)` THEN
  ASM_SIMP_TAC[REAL_LE_MUL2; REAL_ABS_POS; NORM_POS_LE; REAL_LT_IMP_LE] THEN
  REWRITE_TAC[REAL_ARITH `c * (a / b) = (c * a) / b`] THEN
  SIMP_TAC[REAL_LT_LDIV_EQ; REAL_ARITH `&0 < abs x + &1`] THEN
  MATCH_MP_TAC(REAL_ARITH
   `e * B <= e * abs B /\ &0 < e ==> B * e < e * (abs B + &1)`) THEN
  ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN REAL_ARITH_TAC);;




let MAP_EDGES_FACET_INTO_E1_FAN_INJ=
prove_by_refinement(`!p:real^3->bool f e.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f facet_of p 
/\ e IN EDGES0_FAN p f 
==> e IN edges f`,

[REWRITE_TAC[EDGES0_FAN;IN_ELIM_THM;SET_RULE`~(A={})<=> ?a. a IN A`;INTER]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC`e IN edges (p:real^3->bool)`
THEN REWRITE_TAC[edges;IN_ELIM_THM;edge_of]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[CLOSURE_SEQUENTIAL;fchanged;IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SKOLEM_THM;]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC CONVERGENT_IMP_CAUCHY[`x:num->real^3`;`a:real^3`][cauchy]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC FACET_OF_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN ASSUME_TAC(SYM th))
THEN SUBGOAL_THEN`!n. a' dot (v1:num->real^3) n=b:real ` ASSUME_TAC;
MRESA1_TAC RELATIVE_INTERIOR`f:real^3->bool`
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;IN_ELIM_THM] THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[SYM th;IN_ELIM_THM;INTER] THEN REPEAT STRIP_TAC)
THEN ASM_TAC
THEN SET_TAC[];
FIND_ASSUM(fun th -> MP_TAC th THEN REWRITE_TAC[facet_of] THEN STRIP_TAC)`f facet_of (p:real^3->bool)`
THEN POP_ASSUM MP_TAC
THEN DISJ_CASES_TAC(SET_RULE`f=p \/ ~(f=p:real^3->bool)`);
ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;
MRESA_TAC FACE_OF_DISJOINT_INTERIOR[`f:real^3->bool`;`p:real^3->bool`]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN DISJ_CASES_TAC(REAL_ARITH`(b= &0) \/ ~(b= &0)`);
SUBGOAL_THEN`vec 0 IN (f:real^3->bool)`ASSUME_TAC;
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 POP_ASSUM(fun th-> REWRITE_TAC[SYM th;INTER;IN_ELIM_THM;DOT_RZERO])
THEN STRIP_TAC
THEN RESA_TAC
THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
THEN REPEAT RESA_TAC
THEN ASM_TAC
THEN SET_TAC[];
 ASM_TAC
THEN SET_TAC[];
SUBGOAL_THEN`(lift o (t:num->real) --> lift(inv b *(a' dot a:real^3))) sequentially`ASSUME_TAC;
MRESAL_TAC CONTINUOUS_ON_LIFT_DOT[`(:real^3)`;`a':real^3`;][GSYM CONVERGENT_EQ_CAUCHY]
THEN MRESA_TAC CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN[`lift o (\y. (a':real^3) dot y)`;`(:real^3)`]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`a:real^3`[SET_RULE`(a:real^3) IN (:real^3)`])
THEN MRESA_TAC (GEN_ALL CONTINUOUS_WITHIN_SEQUENTIALLY)[`(:real^3)`;`lift o (\y. (a':real^3) dot y)`;`(a:real^3)`]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num->real^3`[SET_RULE`(a:real^3) IN (:real^3)`;o_DEF;DOT_RMUL])
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[LIM_SEQUENTIALLY;dist;GSYM LIFT_SUB;NORM_LIFT]
THEN DISCH_THEN(LABEL_TAC"HA")
THEN REPEAT STRIP_TAC
THEN MRESA1_TAC REAL_ABS_CASES`b:real`
THEN MRESA1_TAC REAL_LT_INV`abs (b:real)`
THEN MRESA_TAC REAL_LT_MUL[`(abs b)`;`e':real`]
THEN REMOVE_THEN "HA" (fun th-> MRESA1_TAC th`abs b * e'`)
THEN EXISTS_TAC`N:num`
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th `n:num`)
THEN MP_TAC(REAL_ARITH`&0< abs b==> ~(abs b= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`abs b`
THEN MRESA1_TAC REAL_MUL_LINV`b:real`
THEN MRESAL_TAC REAL_LT_LMUL[`inv(abs b)`;`abs (((t:num->real) n) * b - a' dot (a:real^3))`;`(abs b) * e'`][REAL_ARITH`A*B*C=(A*B)*C/\ &1 *A=A`;]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[GSYM REAL_ABS_INV;GSYM REAL_ABS_MUL;REAL_ARITH`A*(b*c- D)= (A*c)* b- A*D/\ &1 * A=A`];
SUBGOAL_THEN`!n:num. (v1 n) IN (f:real^3->bool)`ASSUME_TAC;
MRESA1_TAC RELATIVE_INTERIOR`f:real^3->bool`
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;IN_ELIM_THM] THEN REPEAT STRIP_TAC)
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`n:num`)
THEN ASM_REWRITE_TAC[];
MRESA_TAC FACET_OF_IMP_SUBSET[`f:real^3->bool`;`p:real^3->bool`]
THEN SUBGOAL_THEN `!n. norm ((v1:num->real^3) n) <= diameter (p:real^3->bool)` ASSUME_TAC;
STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`n:num`)
THEN STRIP_TAC
THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
THEN MP_TAC(SET_RULE`vec 0 IN interior p /\ interior p  SUBSET p==> vec 0 IN p:real^3->bool`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(v1:num->real^3) n IN f /\ f SUBSET p:real^3->bool==> v1 n IN p`)
THEN RESA_TAC
THEN MRESA1_TAC DIAMETER_BOUNDED`p:real^3->bool`
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(v1:num->real^3) n`;`(vec 0):real^3`][VECTOR_ARITH`A- vec 0=A`]);
DISJ_CASES_TAC(SET_RULE`a' dot (a:real^3)= &0 \/ ~(a' dot (a:real^3)= &0)`);
 SUBGOAL_THEN(`(x --> (vec 0:real^3)) sequentially`) ASSUME_TAC;
ASM_REWRITE_TAC[LIM_SEQUENTIALLY;dist;NORM_LIFT;VECTOR_ARITH`A- vec 0=A`;NORM_MUL]
THEN REPEAT STRIP_TAC
THEN FIND_ASSUM(MP_TAC)`(lift o t --> lift (inv b * (a' dot (a:real^3)))) sequentially`
THEN REWRITE_TAC[LIM_SEQUENTIALLY;dist;GSYM LIFT_SUB;o_DEF;NORM_LIFT]
THEN ASM_REWRITE_TAC[REAL_ARITH`A- B * &0=A`]
THEN SUBGOAL_THEN`&0< diameter (p:real^3->bool)` ASSUME_TAC;
REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`a1:num`)
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`a1:num`)
THEN MP_TAC(SET_RULE`(v1:num->real^3) a1 IN f /\ f INTER interior p = {} /\ vec 0 IN interior p==> ~(v1 a1 = vec 0)`)
THEN RESA_TAC
THEN MRESA1_TAC NORM_POS_LT`(v1:num->real^3) a1`
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
MRESA1_TAC REAL_LT_INV`diameter (p:real^3->bool)`
THEN MRESA_TAC REAL_LT_MUL[`inv (diameter (p:real^3->bool))`;`e':real`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`inv (diameter (p:real^3->bool)) * e'`)
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"HA")
THEN EXISTS_TAC`N:num`
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN"HA"(fun th-> MRESA1_TAC th`n:num`)
THEN MP_TAC(REAL_ARITH`&0 < diameter (p:real^3->bool)==> ~(diameter p= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`(diameter (p:real^3->bool))`
THEN MRESAL_TAC REAL_LT_LMUL[`(diameter (p:real^3->bool))`;`abs ((t:num->real) n)`;`inv (diameter (p:real^3->bool)) * e'`][REAL_ARITH`A*B*C=(B*A)*C/\ &1 *A=A`]
THEN MRESAL_TAC REAL_LE_LMUL[`abs ((t:num->real) n)`;`norm ((v1:num->real^3) n)`;`(diameter (p:real^3->bool))`][REAL_ARITH`A*B*C=(B*A)*C/\ &1 *A=A`;REAL_ABS_POS]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
MRESAL_TAC LIM_UNIQUE[`sequentially`;`x:num-> real^3`;`a:real^3`;`vec 0:real^3`][TRIVIAL_LIMIT_SEQUENTIALLY]
THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`v:real^3`]
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`w:real^3`]
THEN MP_TAC(SET_RULE`~(v IN interior p) /\ ~(w IN interior p) /\ (vec 0 IN interior p)==> DISJOINT{vec 0} {v,w:real^3}`)
THEN RESA_TAC
THEN DISJ_CASES_TAC(SET_RULE`(vec 0 IN aff_gt {vec 0} {v, w:real^3}) \/ ~(vec 0 IN aff_gt {vec 0} {v, w})`);
POP_ASSUM MP_TAC
 THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;VECTOR_ARITH`vec 0= t % vec 0 +A+B<=>  A+B=vec 0`]
THEN REPEAT STRIP_TAC;
SUBGOAL_THEN`vec 0 IN segment[v,w:real^3]`ASSUME_TAC;
REMOVE_ASSUM_TAC
THEN ASM_REWRITE_TAC[IN_SEGMENT]
THEN EXISTS_TAC`inv (&1- t1) * t3`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`A+B+C= &1<=> B+C= &1- A`]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0< t2 /\ &0< t3 ==> ~(t2+ t3= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`&1 - t1`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`t2 % v + t3 % w = vec 0:real^3 ==> (inv (t2+t3))%(t2 % v+ t3 % w) = (inv (t2+t3))%(vec 0)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % vec 0= vec 0/\ A %(B+C)=A % B+A %C/\ A % D %C=(A*D)%C`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`t2+ t3= &1- t1 ==> (inv (&1 - t1))*(t2 +t3) = (inv (&1-t1))*( &1- t1)`)
THEN POP_ASSUM (fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th] 
THEN REWRITE_TAC[]
THEN DISCH_THEN(LABEL_TAC"HA")
THEN STRIP_TAC
THEN STRIP_TAC
THEN REMOVE_THEN "HA" MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`A*(B+C)= &1 <=> A*B= &1 - A*C`]
THEN RESA_TAC
THEN ASSUME_TAC th)
THEN MP_TAC(REAL_ARITH`&0< t2 /\ &0< t3 ==> &0 < t2+ t3`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_LT_INV`&1 - t1`
THEN MRESA_TAC REAL_LT_MUL[`inv(&1 -t1)`;`t3:real`]
THEN MRESA_TAC REAL_LT_MUL[`inv(&1 -t1)`;`t2:real`]
THEN MP_TAC(REAL_ARITH`&0 < inv (&1 - t1) * t3==> &0 <= inv (&1 - t1) * t3`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
DISJ_CASES_TAC(SET_RULE`(segment [v,w] = p) \/ ~(segment [v,w:real^3] = p)`);
POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC Polyhedron.AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;
MRESA_TAC FACE_OF_DISJOINT_INTERIOR[`segment[v,w:real^3]`;`p:real^3->bool`]
THEN ASM_TAC
THEN SET_TAC[];
POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN FIND_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)`e={v,w:real^3}`
THEN ASM_TAC
THEN SET_TAC[];
MRESA1_TAC REAL_INV_EQ_0`b:real`
THEN MRESA_TAC Trigonometry2.NOT_MUL_EQ0_EQ[`inv b`;`a' dot (a:real^3)`]
THEN MRESA_TAC LIM_INV[`sequentially`;`t:num->real`;`inv b * (a' dot a:real^3)`]
THEN MRESA_TAC CONVERGENT_IMP_BOUNDED[`lift o inv o (t:num->real)`; `lift (inv(inv b * (a' dot (a:real^3))))`]
THEN MRESAL_TAC tendsto[`lift o inv o (t:num->real)`; `lift (inv(inv b * (a' dot (a:real^3))))`;`sequentially`][o_DEF;dist;GSYM LIFT_SUB;NORM_LIFT]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`&1`[REAL_ARITH`&0< &1`])
THEN MRESAL_TAC LIM_NULL_CMUL_BOUNDED_FAN[`(\n. inv ((t:num->real) n) - inv (inv b * (a' dot a:real^3)))`;`(\n. (x:num->real^3) n -a)`;`&1`;`sequentially`][GSYM LIM_NULL;VECTOR_ARITH`A%(B-C)=A%B-A%C /\ A% D%B=(A*D)%B`]
THEN MRESA_TAC (GEN_ALL LIM_CMUL)[`sequentially`;`x:num->real^3`;`a:real^3`;`inv (inv b * (a' dot (a:real^3)))`]
THEN MRESA_TAC LIM_NULL[`sequentially`;`(\x. inv (inv b * (a' dot a:real^3)) % t x % (v1:num->real^3) x)`;`inv (inv b * (a' dot a)) % a:real^3`]
THEN MRESAL_TAC LIM_ADD[`sequentially`;`(\x. inv (inv b * (a' dot a:real^3)) % t x % (v1:num->real^3) x -inv (inv b * (a' dot a)) % a:real^3)`;`(\n:num. ((inv (t n) - inv (inv b * (a' dot a))) * t n) % v1 n -
            (inv (t n) - inv (inv b * (a' dot a))) % a:real^3)`;`vec 0:real^3`;`vec 0:real^3`][VECTOR_ARITH`inv (inv b * (a' dot a)) % t x % v1 x -
            inv (inv b * (a' dot a)) % a +
            ((inv (t x) - inv (inv b * (a' dot a))) * t x) % v1 x -
            (inv (t x) - inv (inv b * (a' dot a))) % a
=(inv (t x)  * t x) % v1 x -
            (inv (t x) ) % a/\ vec 0+ vec 0= vec 0`] 
THEN SUBGOAL_THEN`((\n:num. inv (t n) % a:real^3) --> inv (inv b * (a' dot a)) % a:real^3) sequentially` ASSUME_TAC;
REWRITE_TAC[LIM_SEQUENTIALLY;dist;GSYM VECTOR_SUB_RDISTRIB;NORM_MUL]
THEN DISJ_CASES_TAC(SET_RULE`norm (a:real^3)= &0 \/ ~(norm a= &0)`);
ASM_REWRITE_TAC[REAL_ARITH`A * &0= &0`]
THEN REAL_ARITH_TAC;
REPEAT STRIP_TAC
THEN FIND_ASSUM MP_TAC`(lift o inv o t --> lift (inv (inv b * (a' dot a:real^3)))) sequentially`
THEN REWRITE_TAC[LIM_SEQUENTIALLY;NORM_LIFT;dist;o_DEF;GSYM LIFT_SUB]
THEN MP_TAC(REAL_ARITH`&0<= norm a /\ ~(norm a= &0)==> &0< norm (a:real^3) `)
THEN ASM_REWRITE_TAC[NORM_POS_LE]
THEN STRIP_TAC
THEN MRESA1_TAC REAL_LT_INV`norm (a:real^3)`
THEN MRESA1_TAC REAL_MUL_LINV`norm (a:real^3)`
THEN MRESA_TAC REAL_LT_MUL[`e':real`;`inv(norm (a:real^3))`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th` e' * inv(norm (a:real^3)) :real`)
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN EXISTS_TAC`N:num`
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th`n:num`)
THEN MRESAL_TAC REAL_LT_RMUL[`abs (inv (t (n:num)) - inv (inv b * (a' dot (a:real^3))))`;`e' * inv (norm (a:real^3))`;`norm (a:real^3)`][REAL_ARITH`(a*b)*c=a*(b*c)/\ a * &1=a`];
MRESA_TAC LIM_NULL[`sequentially`;`(\n:num. inv (t n) % (a:real^3))`;`inv (inv b * (a' dot a)) % (a:real^3)`]
THEN MRESAL_TAC LIM_ADD[`sequentially`;`(\x:num. (inv (t x) * t x) % v1 x - inv (t x) % a:real^3)`;`(\x:num. inv (t x) % a - inv (inv b * (a' dot a)) % a:real^3)`;`vec 0:real^3`;`vec 0:real^3`][VECTOR_ARITH` A-B+B-C=A-C:real^3 /\ vec 0+ vec 0= vec 0`] 
THEN MRESA_TAC LIM_NULL[`sequentially`;`(\x:num. (inv (t x) * t x) % (v1:num->real^3) x)`;`inv (inv b * (a' dot a)) % (a:real^3)`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`!n:num. inv( t n) * t n= &1 ` ASSUME_TAC;
REPEAT STRIP_TAC
THEN MATCH_MP_TAC REAL_MUL_LINV
THEN MATCH_MP_TAC(REAL_ARITH`A > &0==> ~(A= &0)`)
THEN ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[VECTOR_ARITH`&1 % A=A`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`(!n:num. v1 n IN f:real^3->bool) /\ ((\n. v1 n) --> inv (inv b * (a' dot (a:real^3))) % (a:real^3)) sequentially ==> (?v1:num->real^3. (!n:num. v1 n IN f:real^3->bool) /\ (v1 --> inv (inv b * (a' dot (a:real^3))) % (a:real^3)) sequentially)`)
THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC
THEN MRESA_TAC CLOSURE_SEQUENTIAL[`f:real^3->bool`;`inv (inv b * (a' dot (a:real^3))) % (a:real^3)`]
THEN POP_ASSUM MP_TAC
THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f:real^3->bool`;`p:real^3->bool`]
THEN MRESA1_TAC POLYTOPE_IMP_CLOSED`f:real^3->bool`
THEN MRESA1_TAC CLOSURE_CLOSED`f:real^3->bool`
THEN REPEAT STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN MP_TAC(SET_RULE`vec 0 IN interior p /\ interior p SUBSET (p:real^3->bool)
/\ p SUBSET {x | a' dot x <= b} ==> a' dot vec 0<= b`)
THEN ASM_REWRITE_TAC[INTERIOR_SUBSET;DOT_RZERO]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0<= b /\ ~(b= &0) ==> &0< b`)
THEN RESA_TAC
THEN DISJ_CASES_TAC(REAL_ARITH`&0< -- (a' dot (a:real^3)) \/ &0<= a' dot (a:real^3)`);
MRESAL_TAC CONTINUOUS_ON_LIFT_DOT[`(:real^3)`;`a':real^3`;][GSYM CONVERGENT_EQ_CAUCHY]
THEN MRESA_TAC CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN[`lift o (\y. (a':real^3) dot y)`;`(:real^3)`]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`a:real^3`[SET_RULE`(a:real^3) IN (:real^3)`])
THEN MRESA_TAC (GEN_ALL CONTINUOUS_WITHIN_SEQUENTIALLY)[`(:real^3)`;`lift o (\y. (a':real^3) dot y)`;`(a:real^3)`]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num->real^3`[SET_RULE`(a:real^3) IN (:real^3)`;o_DEF;DOT_RMUL])
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[LIM_SEQUENTIALLY;dist;GSYM LIFT_SUB;NORM_LIFT]
THEN MP_TAC(REAL_ARITH`&0< --(a' dot (a:real^3))==> &0< --(a' dot (a:real^3))/ &2`)
THEN RESA_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`--(a' dot (a:real^3))/ &2`)
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`N:num`[ARITH_RULE`N<=N:num`])
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`(t:num->real) N > &0 ==> &0< t N`)
THEN RESA_TAC
THEN MRESA_TAC REAL_LT_MUL[`(t:num->real) N`;`b:real`]
THEN MP_TAC(REAL_ARITH`&0< (t:num->real) N * b /\ &0< --(a' dot (a:real^3))  ==> &0< t N * b- a' dot a`)
THEN RESA_TAC
THEN MRESAL1_TAC (GEN_ALL Trigonometry2.LT_IMP_ABS_REFL)`(t:num->real) N * b- a' dot (a:real^3)`[REAL_ARITH`A - B < -- B/ &2<=> A< B/ &2`]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`(t:num->real) N * b < (a' dot (a:real^3))/ &2 /\ &0< --(a' dot (a:real^3))  ==> ~(&0< t N * b)`)
THEN RESA_TAC;
MP_TAC(REAL_ARITH`&0 <= (a' dot (a:real^3)) /\ ~(a' dot (a:real^3)= &0)  ==> &0< a' dot a`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_LT_INV`b:real`
THEN MRESA_TAC REAL_LT_MUL[`inv b:real`;`(a' dot (a:real^3)):real`]
THEN MRESA1_TAC REAL_LT_INV`inv b *(a' dot (a:real^3)):real`
THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`v:real^3`]
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`w:real^3`]
THEN MP_TAC(SET_RULE`~(v IN interior p) /\ ~(w IN interior p) /\ (vec 0 IN interior p)==> DISJOINT{vec 0} {v,w:real^3}`)
THEN RESA_TAC
THEN SUBGOAL_THEN`a IN aff_gt {vec 0} {v,w:real^3}` ASSUME_TAC;
ASM_MESON_TAC[];
MRESA_TAC Planarity.scale_aff_gt_fan[`vec 0:real^3`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`a:real^3`;`inv (inv b * (a' dot (a:real^3)))`][VECTOR_ARITH`a- vec 0= a /\ a+ vec 0=a`])
THEN DISJ_CASES_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN relative_interior f \/ ~(inv (inv b * (a' dot a)) % a IN relative_interior (f:real^3->bool) )`);
SUBGOAL_THEN `inv (inv b * (a' dot a)) % a IN fchanged (f:real^3->bool)`ASSUME_TAC;
REWRITE_TAC[fchanged;IN_ELIM_THM]
THEN EXISTS_TAC`inv (inv b * (a' dot a)) % a:real^3`
THEN EXISTS_TAC `&1`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1> &0`;]
THEN VECTOR_ARITH_TAC;
MRESA1_TAC Polyhedron.FCHANGED_EQ_YFAN`p:real^3->bool`
THEN SUBGOAL_THEN` fchanged f SUBSET yfan (vec 0,vertices p,edges (p:real^3->bool))`ASSUME_TAC;
POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;UNIONS;IN_ELIM_THM;SUBSET])
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`fchanged f:real^3->bool`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`f:real^3->bool`
THEN ASM_REWRITE_TAC[];
SUBGOAL_THEN `{v, w:real^3} IN edges p` ASSUME_TAC;
ASM_REWRITE_TAC[IN_ELIM_THM;edges]
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[edge_of];
MRESA_TAC Planarity.AFF_GE_SUBSET_XFAN[`vec 0:real^3`;`vertices p:real^3->bool`;`edges (p:real^3->bool)`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0:real^3}`;`{v,w:real^3}`]
THEN MP_TAC(SET_RULE`aff_ge {vec 0} {v, w} SUBSET xfan (vec 0,vertices p,edges p)/\ aff_gt {vec 0} {v, w} SUBSET aff_ge {vec 0} {v, w}
/\ inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
==> inv (inv b * (a' dot a)) % a IN xfan (vec 0,vertices p,edges (p:real^3->bool))`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN fchanged f
/\ fchanged f SUBSET yfan (vec 0,vertices p,edges p)
==> inv (inv b * (a' dot a)) % a IN  yfan (vec 0,vertices p,edges (p:real^3->bool))`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[yfan;IN_ELIM_THM; DIFF];
POP_ASSUM MP_TAC
THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`]
THEN MRESA1_TAC RELATIVE_INTERIOR_OF_POLYHEDRON`f:real^3->bool`
THEN ASM_REWRITE_TAC[DIFF;IN_ELIM_THM;DE_MORGAN_THM;UNIONS;]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`?v w. {v,w} IN edges (p:real^3->bool) /\ u = segment[v,w]`ASSUME_TAC;
 FIND_ASSUM MP_TAC`u facet_of (f:real^3->bool)`
THEN FIND_ASSUM MP_TAC`f facet_of (p:real^3->bool)`
THEN REWRITE_TAC[facet_of]
THEN ASM_REWRITE_TAC[edges;IN_ELIM_THM;edge_of]
THEN MRESA_TAC Polyhedron.AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_RULE`&3 - &1- &1= &1:int`]
THEN RESA_TAC
THEN MRESA_TAC FACE_OF_TRANS[`u:real^3->bool`;`f:real^3->bool`;`p:real^3->bool`]
THEN MRESA_TAC Polyhedron.EXPAND_EDGE_POLYTOPE[`u:real^3->bool`;`p:real^3->bool`]
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`a'':real^3`
THEN EXISTS_TAC`b':real^3`
THEN REWRITE_TAC[]
THEN EXISTS_TAC`a'':real^3`
THEN EXISTS_TAC`b':real^3`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
POP_ASSUM MP_TAC
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC FACET_OF_IMP_FACE_OF[`u:real^3->bool`;`f:real^3->bool`]
THEN MRESA_TAC FACE_OF_TRANS[`u:real^3->bool`;`f:real^3->bool`;`p:real^3->bool`]
THEN SUBGOAL_THEN`segment [v',w'] SUBSET aff_ge {vec 0} {v',w':real^3}` ASSUME_TAC;
MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v':real^3`;`w':real^3`]
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`v':real^3`]
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`w':real^3`]
THEN MP_TAC(SET_RULE`~(v' IN interior p) /\ ~(w' IN interior p) /\ (vec 0 IN interior p)==> DISJOINT{vec 0} {v',w':real^3}`)
THEN RESA_TAC
THEN MRESAL_TAC Polyhedron.in_aff_ge_fan[`vec 0:real^3`;`v':real^3`;`w':real^3`]
[segment;SUBSET;IN_ELIM_THM]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th `u':real`);
 MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0:real^3}`;`{v,w:real^3}`]
THEN MP_TAC(SET_RULE` aff_gt {vec 0} {v, w} SUBSET aff_ge {vec 0} {v, w}
/\ inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
==> inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v, w:real^3}`)
THEN RESA_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`  inv (inv b * (a' dot a)) % a IN segment[v',w']
/\ segment[v',w'] SUBSET aff_ge {vec 0} {v', w'}
/\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v, w:real^3}
==> inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v', w':real^3} INTER aff_ge {vec 0} {v,w}`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`][FAN;fan7;UNION;IN_ELIM_THM]
THEN POP_ASSUM(fun th-> MRESA_TAC th [`{v',w':real^3}`;`e:(real^3->bool)`])
THEN MRESA1_TAC Polyhedron.POLYTOPE_FAN80`p:real^3->bool`
THEN MRESA1_TAC Polyhedron.CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
THEN DISJ_CASES_TAC(SET_RULE`{v', w'} INTER {v, w:real^3} = {} \/ ~({v', w'} INTER {v, w} = {})`);
MP_TAC(REAL_ARITH`&0 < inv (inv b * (a' dot (a:real^3)))==> ~(inv (inv b * (a' dot a))= &0)`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING;VECTOR_MUL_EQ_0]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DOT_RZERO]);
POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={}) <=> ?v1. v1 IN A`]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[ INTER;IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`v1' IN {v',w':real^3} ==> v1'= v' \/ v1'= w'`)
THEN RESA_TAC;
STRIP_TAC
THEN MP_TAC(SET_RULE`v' IN {v,w:real^3} ==> v'= v \/ v'= w`)
THEN RESA_TAC;
DISJ_CASES_TAC(SET_RULE`~(w'=w) \/ w'=w:real^3`);
MP_TAC(SET_RULE`~(w'=w:real^3) ==>{x | x IN {v, w'} /\ x IN {v, w}}= {v}`)
THEN RESA_TAC
THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
THEN MRESA_TAC Conforming.properties12_fan7[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
THEN MRESA_TAC properties_of_graph[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`w':real^3`;`v':real^3`]
THEN MP_TAC(SET_RULE` e IN edges p /\ v IN vertices p
/\ UNIONS {aff_gt {vec 0:real^3} e' | e' IN edges (p:real^3->bool)} INTER UNIONS {aff_ge {vec 0} {v} | v IN vertices p}= {} ==> aff_gt {vec 0:real^3} e INTER aff_ge {vec 0:real^3} {v}= {}`)
THEN RESA_TAC 
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
/\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v}
==> ~(aff_gt {vec 0:real^3} {v,w} INTER aff_ge {vec 0:real^3} {v}= {})`)
THEN RESA_TAC;
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN ASM_REWRITE_TAC[];
DISJ_CASES_TAC(SET_RULE`~(w'=v) \/ w'=v:real^3`);
MP_TAC(SET_RULE`~(w'=v:real^3) ==>{x | x IN {w, w'} /\ x IN {v, w}}= {w}`)
THEN RESA_TAC
THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
THEN MRESA_TAC Conforming.properties12_fan7[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
THEN MRESA_TAC properties_of_graph[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`w':real^3`;`v':real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN MP_TAC(SET_RULE` e IN edges p /\ w IN vertices p
/\ UNIONS {aff_gt {vec 0:real^3} e' | e' IN edges (p:real^3->bool)} INTER UNIONS {aff_ge {vec 0} {v} | v IN vertices p}= {} ==> aff_gt {vec 0:real^3} e INTER aff_ge {vec 0:real^3} {w}= {}`)
THEN RESA_TAC 
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
/\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {w}
==> ~(aff_gt {vec 0:real^3} {v,w} INTER aff_ge {vec 0:real^3} {w}= {})`)
THEN RESA_TAC;
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
THEN ASM_REWRITE_TAC[];
STRIP_TAC
THEN MP_TAC(SET_RULE`w' IN {v,w:real^3} ==> w'= v \/ w'= w`)
THEN RESA_TAC;
DISJ_CASES_TAC(SET_RULE`~(v'=w) \/ v'=w:real^3`);
MP_TAC(SET_RULE`~(v'=w:real^3) ==>{x | x IN {v', v} /\ x IN {v, w}}= {v}`)
THEN RESA_TAC
THEN MRESA_TAC Conforming.properties12_fan7[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
THEN MRESA_TAC properties_of_graph[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`v':real^3`;`w':real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "THY" MP_TAC
THEN RESA_TAC
THEN MP_TAC(SET_RULE` e IN edges p /\ v IN vertices p
/\ UNIONS {aff_gt {vec 0:real^3} e' | e' IN edges (p:real^3->bool)} INTER UNIONS {aff_ge {vec 0} {v} | v IN vertices p}= {} ==> aff_gt {vec 0:real^3} e INTER aff_ge {vec 0:real^3} {v}= {}`)
THEN RESA_TAC 
THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
/\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v}
==> ~(aff_gt {vec 0:real^3} {v,w} INTER aff_ge {vec 0:real^3} {v}= {})`)
THEN RESA_TAC;
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
THEN ASM_REWRITE_TAC[];
DISJ_CASES_TAC(SET_RULE`~(v'=v) \/ v'=v:real^3`);
MP_TAC(SET_RULE`~(v'=v:real^3) ==>{x | x IN {v', w} /\ x IN {v, w}}= {w}`)
THEN RESA_TAC
THEN MRESA_TAC Conforming.properties12_fan7[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
THEN MRESA_TAC properties_of_graph[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`v':real^3`;`w':real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "THY" MP_TAC
THEN RESA_TAC
THEN MP_TAC(SET_RULE` e IN edges p /\ w IN vertices p
/\ UNIONS {aff_gt {vec 0:real^3} e' | e' IN edges (p:real^3->bool)} INTER UNIONS {aff_ge {vec 0} {v} | v IN vertices p}= {} ==> aff_gt {vec 0:real^3} e INTER aff_ge {vec 0:real^3} {w}= {}`)
THEN RESA_TAC 
THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
/\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {w}
==> ~(aff_gt {vec 0:real^3} {v,w} INTER aff_ge {vec 0:real^3} {w}= {})`)
THEN RESA_TAC;
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN ASM_REWRITE_TAC[]]);;





let CONVEX_OPEN_AFF_GT_FACE=
prove(`FAN(x,V,E) 
/\ (!v. v IN V ==> CARD (set_of_edge v V E) > 1)
/\ fan80(x,V,E)
/\ f IN face_set (hypermap1_of_fanx (x,V,E))
==> (!s. s IN {aff_gt {x, pr2 y, pr3 y} {pr3 (f1_fan x V E y)} | y IN (f:real^3#real^3#real^3#real^3->bool)} ==> convex s /\ open s)`,


REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THENL[
ASM_REWRITE_TAC[CONVEX_AFF_GT];
MRESA_TAC fully_surrounded_imp_aff_gt_3_1_of_dart_eq_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`f:real^3#real^3#real^3#real^3->bool`;`y:real^3#real^3#real^3#real^3`]
THEN MATCH_MP_TAC OPEN_AFF_GT_3_1
THEN MRESA_TAC properties_of_elements_in_face_fully_surroundedfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`f:real^3#real^3#real^3#real^3->bool`; `y:real^3#real^3#real^3#real^3`]
THEN FIND_ASSUM MP_TAC `fan80(x:real^3,V,E)`
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th -> MRESA_TAC th [`(pr2 y):real^3`;`(pr3 y):real^3`] )
THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`(pr2 y):real^3`;`(pr3 y):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`;`(pr2 y):real^3`;`(pr3 y):real^3`]
THEN DISCH_TAC
THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`(pr2 y):real^3`;`(sigma_fan x V E (pr2 y) (pr3 y)):real^3`]
THEN MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(sigma_fan x V E (pr2 y) (pr3 y)):real^3`;`(pr2 y):real^3`;`(pr3 y):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,C,D}={A,C,D,B}`]
THEN ASM_REWRITE_TAC[]]);;

let AFF_GE_3_1 = 
prove
 (`!x v u w.
        DISJOINT {x,v,u} {w}
        ==> aff_ge {x,v,u} {w} =
             {y | ?t1 t2 t3 t4.
                     &0 <= t4 /\
                     t1 + t2 +t3 +t4 = &1 /\
                     y = t1 % x + t2 % v + t3 % u +t4 % w }`,

  AFF_TAC);;

let inter_aff_ge_3_1_is_aff_ge_1_3=
prove(`!x v u w:real^3.
~coplanar {x,v,u,w}
==>
aff_ge {x,v,u} {w} INTER aff_ge {x,u,w} {v} INTER aff_ge {x,w,v} {u}=aff_ge {x} {v,u,w}`,

GEOM_ORIGIN_TAC `x:real^3`
THEN REPEAT STRIP_TAC
THEN MRESA_TAC notcoplanar_disjoints[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC notcoplanar_disjoint[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
THEN MRESA_TAC AFF_GE_1_3[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC NOT_COPLANAR_0_4_IMP_INDEPENDENT[`v:real^3`;`u:real^3`;`w:real^3`]
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;INTER]
THEN REDUCE_VECTOR_TAC
THEN GEN_TAC
THEN EQ_TAC
THENL[
STRIP_TAC
THEN POP_ASSUM MP_TAC 
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t2 % v + t3 % u + t4 % w = t2'' % w + t3'' % v + t4'' % u <=> (t2-t3'') % v + (t3-t4'') % u + (t4-t2'') % w= vec 0`]
THEN STRIP_TAC
THEN MRESAL_TAC INDEPENDENT_3[`v:real^3`;`u:real^3`;`w:real^3`;`t2-t3'':real`; `t3-t4'':real`; `t4 -t2'':real`][REAL_ARITH`A-B= &0<=> A=B`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC 
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t2 % v + t3 % u + t4 % w = t2' % u + t3' % w + t4' % v <=> (t2-t4') % v + (t3-t2') % u + (t4-t3') % w= vec 0`]
THEN STRIP_TAC
THEN MRESAL_TAC INDEPENDENT_3[`v:real^3`;`u:real^3`;`w:real^3`;`t2-t4':real`; `t3-t2':real`; `t4 -t3':real`][REAL_ARITH`A-B= &0<=> A=B`]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`t1'':real`
THEN EXISTS_TAC`t3'':real`
THEN EXISTS_TAC`t4'':real`
THEN EXISTS_TAC`t2'':real`
THEN ASM_REWRITE_TAC[REAL_ARITH`t1+t2+t3+t4=t1+t4+t2+t3:real`]
THEN ASM_TAC
THEN REAL_ARITH_TAC;

STRIP_TAC
THEN STRIP_TAC
THENL[EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`t3:real`
THEN EXISTS_TAC`t4:real`
THEN ASM_REWRITE_TAC[];

STRIP_TAC
THENL[
EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t3:real`
THEN EXISTS_TAC`t4:real`
THEN EXISTS_TAC`t2:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`t1  + t3 + t4+ t2:real=t1 + t2 + t3 + t4`]
THEN VECTOR_ARITH_TAC;
EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t4:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`t3:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`t1  + t4+ t2+ t3:real=t1 + t2 + t3 + t4`]
THEN VECTOR_ARITH_TAC]]]);;

let CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1=
prove_by_refinement(`!x v u w:real^3. ~coplanar {x, v, u, w} ==> 
closure (aff_gt {x,v, u}  {w}) = aff_ge {x, v, u} {w}`,

[GEOM_ORIGIN_TAC `x:real^3`
THEN REPEAT STRIP_TAC
THEN MRESA_TAC notcoplanar_disjoints[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESAL_TAC Planarity.coplanar_cross_dot[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN MP_TAC(REAL_ARITH`~((v cross u) dot w = &0) ==> &0 < (v cross u) dot w \/ &0 < --((v cross u) dot (w:real^3))`)
THEN RESA_TAC;
MRESAL_TAC Planarity.aff_gt_3_1_rep_cross_dot[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN DISJ_CASES_TAC (SET_RULE` v cross u = vec 0 \/ ~(v cross (u:real^3) = vec 0)`);
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; DOT_LZERO]);
REWRITE_TAC[REAL_ARITH`&0 < A <=> (-- A) < &0`;REAL_ARITH`&0 <= A <=> (-- A) <= &0`;GSYM DOT_LNEG]
THEN MATCH_MP_TAC CLOSURE_HALFSPACE_LT
THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- A=  vec 0<=> A= vec 0:real^3`];
POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[CROSS_SKEW]
THEN REWRITE_TAC[DOT_LNEG; REAL_ARITH`-- (-- A)=A`]
THEN STRIP_TAC
THEN MRESAL_TAC Planarity.aff_gt_3_1_rep_cross_dot[`(vec 0):real^3`;`u:real^3`;`v:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{X, u, v, w}= {X, v, u, w}`]
THEN RESA_TAC
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot[`(vec 0):real^3`;`u:real^3`;`v:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{X, u, v, w}= {X, v, u, w}`]
THEN RESA_TAC
THEN DISJ_CASES_TAC (SET_RULE` u cross v = vec 0 \/ ~(u cross (v:real^3) = vec 0)`);
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; DOT_LZERO])
THEN REAL_ARITH_TAC;
ONCE_REWRITE_TAC[SET_RULE`{X, u, v}= {X, v, u}`]
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[REAL_ARITH`&0 < A <=> (-- A) < &0`;REAL_ARITH`&0 <= A <=> (-- A) <= &0`;GSYM DOT_LNEG]
THEN MATCH_MP_TAC CLOSURE_HALFSPACE_LT
THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- A=  vec 0<=> A= vec 0:real^3`]]);;
let CLOSURE_AFF_GT_1_3_EQ_AFF_GE_1_3= 
prove(`!x v u w:real^3. ~coplanar {x, v, u, w} ==> 
closure (aff_gt {x} {v, u, w}) = aff_ge {x} {v, u, w}`,

REPEAT STRIP_TAC
THEN MRESA_TAC inter_aff_ge_3_1_is_aff_ge_1_3[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC OPEN_AFF_GT_3_1[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC OPEN_AFF_GT_3_1[`x:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{x, u, w, v}={x, v,u, w}`]
THEN RESA_TAC
THEN MRESA_TAC OPEN_AFF_GT_3_1[`x:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{x, w, v, u}={x, v,u, w}`]
THEN RESA_TAC
THEN MRESA_TAC CONVEX_AFF_GT[`{x,v,u:real^3}`;`{w:real^3}`]
THEN MRESA_TAC CONVEX_AFF_GT[`{x,u:real^3,w}`;`{v:real^3}`]
THEN MRESA_TAC CONVEX_AFF_GT[`{x,w,v:real^3}`;`{u:real^3}`]
THEN MRESA_TAC Planarity.notcoplanar_4point_aff_gt_1_3_not_empty[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC Planarity.inter_aff_gt_3_1_is_aff_gt_1_3[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`~(aff_gt {x, v, u} {w} INTER aff_gt {x, u, w} {v} INTER aff_gt {x, w, v} {u} =
   {})
==> ~(aff_gt {x, v, u} {w} INTER aff_gt {x, u, w} {v:real^3} =
   {})`)
THEN RESA_TAC
THEN MRESA_TAC CLOSURE_INTER_CONVEX_OPEN[`aff_gt {x, v, u} {w:real^3}`;`aff_gt {x, u, w} {v:real^3}`]
THEN MRESA_TAC OPEN_INTER[`aff_gt {x, v, u} {w:real^3}`;`aff_gt {x, u, w} {v:real^3}`]
THEN MRESA_TAC CONVEX_INTER[`aff_gt {x, v, u} {w:real^3}`;`aff_gt {x, u, w} {v:real^3}`]
THEN MRESAL_TAC CLOSURE_INTER_CONVEX_OPEN[`aff_gt {x, v, u} {w:real^3} INTER aff_gt {x, u, w} {v:real^3}`;`aff_gt {x, w, v} {u:real^3}`][SET_RULE`(A INTER B) INTER C= A INTER B INTER C`]
THEN MRESA_TAC CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1[`x:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{x, u, w, v}={x, v,u, w}`]
THEN RESA_TAC
THEN MRESA_TAC CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1[`x:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{x, w, v,u}={x, v,u, w}`]
THEN RESA_TAC);;

let AFF_GT_SUBSET_CLOSURE_DARTSET_LEADS_INTO_FAN=
prove(`FAN(x,V,E) 
/\ (!v. v IN V ==> CARD (set_of_edge v V E) > 1)
/\ fan80(x,V,E)
/\ f IN face_set (hypermap1_of_fanx (x,V,E))
/\ e IN f
==>  aff_gt {x} {(pr2 e), pr3 e } SUBSET closure(dartset_leads_into_fan x V E f)`,


REPEAT STRIP_TAC
THEN MRESAL_TAC properties_of_elements_in_face_fully_surroundedfan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`f:real^3#real^3#real^3#real^3->bool`;`e:real^3#real^3#real^3#real^3`][edges;IN_ELIM_THM]
THEN ABBREV_TAC`v=pr2 (e:real^3#real^3#real^3#real^3)`
THEN ABBREV_TAC`w=pr3 (e:real^3#real^3#real^3#real^3)`
THEN ABBREV_TAC`u=sigma_fan x V E v (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 Fan.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 MRESA_TAC remark1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u:real^3`;`v:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN MRESA_TAC aff_gt_1_3_subset_dart_leads_into_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC SUBSET_CLOSURE[`aff_gt {x} {u, v, w:real^3}`;`dart_leads_into x V E v (w:real^3)`]
THEN MRESA_TAC Planarity.DARTSET_LEADS_INTO_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`f:real^3#real^3#real^3#real^3->bool`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(e:real^3#real^3#real^3#real^3)`)
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC`fan80(x:real^3,V,E)`
THEN REWRITE_TAC[fan80]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
THEN MRESA_TAC Planarity.properties_fully_surrounded[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC CLOSURE_AFF_GT_1_3_EQ_AFF_GE_1_3[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC Planarity.aff_ge_1_3_eq_unions_aff_ge_1_2_and_aff_gt_1_3[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{x:real^3}`;`{v,w:real^3}`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]);;



let IN_EDGES0_FAN=
prove(`!p:real^3->bool f f1.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p)) 
/\ f1 facet_of p /\ 							 dartset_leads_into_fan (vec 0) (vertices p) (edges p) f = fchanged f1
/\ e IN f
==> {pr2 e, pr3 e} IN EDGES0_FAN p f1`,

REPEAT STRIP_TAC
THEN REWRITE_TAC[EDGES0_FAN;IN_ELIM_THM;edges]
THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
THEN MRESA1_TAC Polyhedron.POLYTOPE_FAN80`p:real^3->bool`
THEN MRESA1_TAC Polyhedron.CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
THEN MRESA_TAC properties_of_elements_in_face_fully_surroundedfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`f:real^3#real^3#real^3#real^3->bool`;`e:real^3#real^3#real^3#real^3`]
THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[edges;IN_ELIM_THM]
THEN STRIP_TAC THEN MP_TAC th THEN ASM_REWRITE_TAC[] THEN STRIP_TAC)
THEN STRIP_TAC
THENL[
EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`w:real^3`
THEN ASM_REWRITE_TAC[];
MRESA_TAC (GEN_ALL AFF_GT_SUBSET_CLOSURE_DARTSET_LEADS_INTO_FAN)[`e:real^3#real^3#real^3#real^3`;`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`f:real^3#real^3#real^3#real^3->bool`]
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`w:real^3`;`v:real^3`]
THEN MRESA_TAC Planarity.exists_in_aff_gt_disjoint[`vec 0:real^3`;`v:real^3`;`w:real^3`]
THEN REWRITE_TAC[SET_RULE`~(A= {})<=> ?a. a IN A`]
THEN EXISTS_TAC`y:real^3`
THEN ASM_TAC
THEN SET_TAC[]]);;

let SUBSET_EDGES0_FAN=
prove(`!p:real^3->bool f f1.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p)) 
/\ f1 facet_of p /\ 							 dartset_leads_into_fan (vec 0) (vertices p) (edges p) f = fchanged f1
==> {{pr2 e, pr3 e}|  e IN f} SUBSET  EDGES0_FAN p f1`,

 REWRITE_TAC[SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_MESON_TAC[IN_EDGES0_FAN]);;



let EDGES0_SUBSET_FAN=
prove_by_refinement(`!p:real^3->bool f f1.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p)) 
/\ f1 facet_of p /\ 							 
 fchanged f1 =dartset_leads_into_fan (vec 0) (vertices p) (edges p) f
==>   EDGES0_FAN p f1 SUBSET {{pr2 e, pr3 e}|  e IN f} `,

[REPEAT STRIP_TAC
THEN  REWRITE_TAC[SUBSET;EDGES0_FAN;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th-> MP_TAC th THEN REWRITE_TAC[edges;IN_ELIM_THM] THEN STRIP_TAC THEN MP_TAC th THEN RESA_TAC)
THEN ASM_REWRITE_TAC[SET_RULE`~(A={}) <=> ?a. a IN A`;INTER;IN_ELIM_THM]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "THYGIANG1")
THEN ABBREV_TAC`x1= (vec 0:real^3)`
THEN ABBREV_TAC`V=(vertices (p:real^3->bool)) `
THEN ABBREV_TAC`E=(edges (p:real^3->bool))`
THEN ABBREV_TAC`u=inverse1_sigma_fan (x1:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`
THEN ABBREV_TAC`U= dartset_leads_into_fan x1 V E f`
THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
THEN MRESA1_TAC Polyhedron.POLYTOPE_FAN80`p:real^3->bool`
THEN MRESA1_TAC Polyhedron.CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`w:real^3`;`v:real^3`]
THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> POP_ASSUM (fun th-> MRESA1_TAC th `w:real^3`) THEN MRESA1_TAC th `w:real^3`)
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`u:real^3`;`v:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN MRESA_TAC dartset_leads_into_is_topological_component_yfan[`x1:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`f:real^3#real^3#real^3#real^3->bool`]
THEN MRESA_TAC exists_point_in_component_yfan[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)` ;`U:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "THYGIANG")
THEN SUBGOAL_THEN`a IN xfan (x1:real^3,(V:real^3->bool),E)`ASSUME_TAC;
REWRITE_TAC[xfan;IN_ELIM_THM]
THEN EXISTS_TAC`{v,w:real^3}`
THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{x1:real^3}`;`{v,w:real^3}`]
THEN ASM_TAC
THEN SET_TAC[IN];
MRESA_TAC Planarity.origin_is_not_aff_gt_fan[`x1:real^3`;`v:real^3`;`w:real^3`]
THEN MP_TAC(SET_RULE`~(x1 IN aff_gt {x1} {v, w}) /\ (a IN aff_gt {x1} {v, w}) ==> ~(a= x1:real^3)`)
THEN RESA_TAC
THEN MRESA_TAC Planarity.topological_component_subset_yfan[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:(real^3->bool)`]
THEN SUBGOAL_THEN`~(a IN U:real^3->bool)` ASSUME_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[yfan]
THEN ASM_TAC
THEN SET_TAC[];
DISJ_CASES_TAC(SET_RULE`~(!t. &0 < t /\ t < &1 ==> (&1 - t) % a + t % z IN (U:real^3->bool)) \/ (!t. &0 < t /\ t < &1 ==> (&1 - t) % a + t % z IN (U:real^3->bool))`);
POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN MRESA_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;]
THEN MRESA_TAC GINGUAP[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`f:(real^3#real^3#real^3#real^3->bool)`]
THEN MRESA1_TAC CLOSURE_SUBSET`U:real^3->bool`
THEN MP_TAC(SET_RULE`z IN U/\ U SUBSET closure U ==> z IN closure (U:real^3->bool)`)
THEN RESA_TAC
THEN MRESAL1_TAC CONVEX_CLOSURE`U:real^3->bool`[CONVEX_CONTAINS_SEGMENT]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`a:real^3`;`z:real^3`][segment;SUBSET;IN_ELIM_THM])
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(&1 - t) % a + t % z:real^3`)
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`(?u. (&0 <= u /\ u <= &1) /\
           (&1 - t) % a + t % z = (&1 - u) % a + u % z:real^3)` ASSUME_TAC;
EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[]
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN FIND_ASSUM MP_TAC`conforming_fan (x1:real^3,V,E)`
THEN REWRITE_TAC[conforming_fan;conforming_half_space_fan]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`f:(real^3#real^3#real^3#real^3->bool)`)
THEN MP_TAC( ISPECL [`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`f:(real^3#real^3#real^3#real^3->bool)`]
Conforming.exists_point_in_dartset_leads_into_fan) 
THEN ONCE_REWRITE_TAC[SET_RULE`(?a. a IN A) <=> ~(A={})`]
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC (GEN_ALL CONVEX_OPEN_AFF_GT_FACE)[`f:(real^3#real^3#real^3#real^3->bool)`;`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
THEN MRESA1_TAC CLOSURE_INTERS_CONVEX_OPEN`{aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)} | y IN (f:(real^3#real^3#real^3#real^3->bool))}`
THEN REMOVE_THEN "THY" MP_TAC
THEN ASM_REWRITE_TAC[INTERS;IN_ELIM_THM;NOT_FORALL_THM;NOT_IMP]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_THEN "THY1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[INTERS;IN_ELIM_THM;NOT_FORALL_THM;NOT_IMP;]
THEN SUBGOAL_THEN`closure (aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)}) IN
      IMAGE closure
      {aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)} | y IN (f:(real^3#real^3#real^3#real^3->bool))}`ASSUME_TAC;
REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`aff_gt {x1:real^3, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)}`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`y:real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[];
STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`closure (aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)})`)
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC Conforming.fully_surrounded_imp_aff_gt_3_1_of_dart_eq_fan 
[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`f:(real^3#real^3#real^3#real^3->bool)`;`y:real^3#real^3#real^3#real^3`]
THEN MRESA_TAC properties_of_elements_in_face_fully_surroundedfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`f:real^3#real^3#real^3#real^3->bool`;`y:real^3#real^3#real^3#real^3`]
THEN REMOVE_THEN"THYGIANG" MP_TAC
THEN ASM_REWRITE_TAC[INTERS;IN_ELIM_THM]
THEN SUBGOAL_THEN`(?y'. y' IN f /\
            aff_gt {x1:real^3, pr2 y, pr3 y} {sigma_fan x1 V E (pr2 y) (pr3 y)} =
            aff_gt {x1, pr2 y', pr3 y'} {pr3 (f1_fan x1 V E y')})
` ASSUME_TAC;
EXISTS_TAC`y:real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[];
STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th `aff_gt {x1:real^3, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)}`)
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN"THYGIANG1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[INTERS;IN_ELIM_THM;NOT_FORALL_THM;NOT_IMP;]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`closure (aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)})`)
THEN POP_ASSUM MP_TAC
THEN ABBREV_TAC`v1=pr2 (y:real^3#real^3#real^3#real^3)`
THEN ABBREV_TAC`w1=pr3 (y:real^3#real^3#real^3#real^3)`
THEN ABBREV_TAC`u1=sigma_fan x1 V E v1 (w1:real^3)`
THEN MRESA_TAC remark1_fan[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w1:real^3`;`v1:real^3`]
THEN MRESA_TAC Fan.sigma_fan_in_set_of_edge[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v1:real^3`;`w1:real^3`]
THEN MRESA_TAC remark1_fan[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u1:real^3`;`v1:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`fan80(x1:real^3,V,E)`
THEN REWRITE_TAC[fan80]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`v1:real^3`;`w1:real^3`])
THEN MRESA_TAC Planarity.properties_fully_surrounded[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u1:real^3`;`v1:real^3`;`w1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{x1, u1, v1, w1}={x1, w1, v1, u1}`]
THEN STRIP_TAC
THEN MRESA_TAC CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1[`x1:real^3`;`w1:real^3`;`v1:real^3`;`u1:real^3`]
THEN MRESA_TAC Planarity.coplanar_cross_dot[`x1:real^3`;`w1:real^3`;`v1:real^3`;`u1:real^3`]
THEN MP_TAC(REAL_ARITH`~(((w1 - x1) cross (v1 - x1)) dot (u1 - x1) = &0)
==> &0 < ((w1 - x1) cross (v1 - x1)) dot (u1 - x1) 
\/ &0 < --( ((w1 - x1) cross (v1 - x1)) dot (u1 - x1:real^3) )`)
THEN RESA_TAC;
MRESA_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot[`x1:real^3`;`w1:real^3`;`v1:real^3`;`u1:real^3`]
THEN MRESA_TAC aff_gt_3_1_rep_cross_dot[`x1:real^3`;`w1:real^3`;`v1:real^3`;`u1:real^3`]
THEN EXPAND_TAC"x1"
THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`;DOT_RADD;DOT_RMUL]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_MUL[`t:real`;`(w1 cross v1) dot (z:real^3)`]
THEN MP_TAC(REAL_ARITH`t< &1==> &0<= &1- t`)
THEN RESA_TAC
THEN MRESA_TAC REAL_LE_MUL[`&1-t:real`;`(w1 cross v1) dot (a:real^3)`]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[VECTOR_ARITH`A - vec 0=A`;GSYM DOT_LNEG]
THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW]
THEN STRIP_TAC 
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN MRESA_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot[`x1:real^3`;`v1:real^3`;`w1:real^3`;`u1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{x1, v1, w1, u1}={x1, w1, v1, u1}`]
THEN RESA_TAC
THEN MRESA_TAC aff_gt_3_1_rep_cross_dot[`x1:real^3`;`v1:real^3`;`w1:real^3`;`u1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{x1, v1, w1, u1}={x1, w1, v1, u1}`]
THEN RESA_TAC
THEN EXPAND_TAC"x1"
THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`;DOT_RADD;DOT_RMUL]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_MUL[`t:real`;`(v1 cross w1) dot (z:real^3)`]
THEN MP_TAC(REAL_ARITH`t< &1==> &0<= &1- t`)
THEN RESA_TAC
THEN MRESA_TAC REAL_LE_MUL[`&1-t:real`;`(v1 cross w1) dot (a:real^3)`]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
SUBGOAL_THEN `(!t. &0 < t /\ t < &1 ==> (&1 - t) % a + t % z IN yfan (x1,V:real^3->bool,E))` ASSUME_TAC;
ASM_TAC
THEN SET_TAC[];
MRESA_TAC not_azim_points1_in_yfan[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;`z:real^3`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC not_azim_points1_in_yfan[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;`z:real^3`;`w:real^3`;`v: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 MP_TAC(REAL_ARITH`~(azim x1 a z v = &0) /\ &0<= azim x1 a z v==> &0< azim x1 a z (v:real^3) `)
THEN ASM_REWRITE_TAC[azim]
THEN STRIP_TAC
THEN MRESA_TAC properties_of_collinear4_points_fan[`x1:real^3`;`v:real^3`;`w:real^3`;`a:real^3`]
THEN MRESA_TAC properties_of_collinear4_points_fan[`x1:real^3`;`w:real^3`;`v:real^3`;`a:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x1:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;` z:real^3`]
THEN DISJ_CASES_TAC(REAL_ARITH`azim x1 a z (v:real^3)< pi \/ pi<= azim x1 a z (v:real^3)`);
MRESA_TAC cross_dot_fully_surrounded_fan[`x1:real^3`;`a:real^3`; `v:real^3`;`z:real^3`]
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"x1"
THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0 =A`]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN STRIP_TAC
THEN ABBREV_TAC`u1=inverse1_sigma_fan (x1:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (w:real^3) (v:real^3)`
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`v:real^3`;`w:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> 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 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 MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`u1:real^3`;`w:real^3`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN MRESA_TAC exists_dart_leads_into_edge_eq_topological1_component_fan[`x1:real^3`;`(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;`z:real^3`;`v:real^3`;`w:real^3`;` (u1:real^3)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"x1"
THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0 =A`]
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN EXISTS_TAC`(x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[pr2;pr3]
THEN ABBREV_TAC`ds2= face (hypermap1_of_fanx (x1,V,E)) ((x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3)`
THEN MRESA_TAC hypermap_of_fan_rep[`x1:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x1 V E) (d1_fan (x1,V,E)))`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN SUBGOAL_THEN`ds2 IN face_set(hypermap1_of_fanx (x1:real^3,V,E))` ASSUME_TAC;
ASM_REWRITE_TAC[face_set;set_of_orbits;IN_ELIM_THM]
THEN EXISTS_TAC`(x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3`
THEN EXPAND_TAC"ds2"
THEN REWRITE_TAC[face]
THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`x1:real^3`;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]
THEN REWRITE_TAC[d1_fan;IN_ELIM_THM]
THEN EXISTS_TAC`x1:real^3`
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`w:real^3`
THEN EXISTS_TAC`sigma_fan x1 V E v w:real^3`
THEN ASM_REWRITE_TAC[];
SUBGOAL_THEN` (x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3 IN ds2` ASSUME_TAC;
EXPAND_TAC"ds2"
THEN REWRITE_TAC[face;IN_ELIM_THM;orbit_map]
THEN EXISTS_TAC`0:num`
THEN REWRITE_TAC[ARITH_RULE`0>= 0`;POWER;I_DEF];
MRESA_TAC DARTSET_LEADS_INTO_FAN[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds2:real^3#real^3#real^3#real^3->bool`]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th `(x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3`[pr2;pr3])
THEN MRESA_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[conforming_fan;conforming_bijection_fan;EXISTS_UNIQUE]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`U:real^3->bool`)
THEN POP_ASSUM(fun th-> MRESA1_TAC th`ds2:real^3#real^3#real^3#real^3->bool`
THEN MRESA1_TAC th`f:real^3#real^3#real^3#real^3->bool`)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
MRESA_TAC aff_gt2_subset_aff_ge[`x1:real^3`;`w:real^3`; `v:real^3`;`a:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC
THEN MRESA_TAC sum5_azim_fan[`x1:real^3`;`a:real^3`;`z:real^3`;`w:real^3`;`v:real^3`]
THEN MP_TAC(REAL_ARITH`azim x1 a z v = azim x1 a z w + pi/\
azim x1 a z v < &2 * pi/\ ~(azim x1 a z w = &0) /\ &0 <= azim x1 a z w 
==>  &0< azim x1 a z w /\ azim x1 a z w < pi
`)
THEN ASM_REWRITE_TAC[azim]
THEN STRIP_TAC;
MRESA_TAC cross_dot_fully_surrounded_fan[`x1:real^3`;`a:real^3`; `w:real^3`;`z:real^3`]
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"x1"
THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0 =A`]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
THEN STRIP_TAC
THEN MRESA_TAC exists_dart_leads_into_edge_eq_topological1_component_fan[`x1:real^3`;`(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;`z:real^3`;`w:real^3`;`v:real^3`;` (u:real^3)`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"x1"
THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0 =A`]
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN EXISTS_TAC`(x1,w,v,sigma_fan x1 V E w v):real^3#real^3#real^3#real^3`
THEN ASM_REWRITE_TAC[pr2;pr3]
THEN ABBREV_TAC`ds2= face (hypermap1_of_fanx (x1,V,E)) ((x1,w,v,sigma_fan x1 V E  w v):real^3#real^3#real^3#real^3)`
THEN MRESA_TAC hypermap_of_fan_rep[`x1:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x1 V E) (d1_fan (x1,V,E)))`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN SUBGOAL_THEN`ds2 IN face_set(hypermap1_of_fanx (x1:real^3,V,E))` ASSUME_TAC;
ASM_REWRITE_TAC[face_set;set_of_orbits;IN_ELIM_THM]
THEN EXISTS_TAC`(x1,w,v,sigma_fan x1 V E w v):real^3#real^3#real^3#real^3`
THEN EXPAND_TAC"ds2"
THEN REWRITE_TAC[face]
THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`x1:real^3`;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]
THEN REWRITE_TAC[d1_fan;IN_ELIM_THM]
THEN EXISTS_TAC`x1:real^3`
THEN EXISTS_TAC`w:real^3`
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`sigma_fan x1 V E w v:real^3`
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN SUBGOAL_THEN` (x1,w,v,sigma_fan x1 V E w v):real^3#real^3#real^3#real^3 IN ds2` ASSUME_TAC;
EXPAND_TAC"ds2"
THEN REWRITE_TAC[face;IN_ELIM_THM;orbit_map]
THEN EXISTS_TAC`0:num`
THEN REWRITE_TAC[ARITH_RULE`0>= 0`;POWER;I_DEF];
MRESA_TAC DARTSET_LEADS_INTO_FAN[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds2:real^3#real^3#real^3#real^3->bool`]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th `(x1,w,v,sigma_fan x1 V E w v):real^3#real^3#real^3#real^3`[pr2;pr3])
THEN MRESA_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[conforming_fan;conforming_bijection_fan;EXISTS_UNIQUE]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`U:real^3->bool`)
THEN POP_ASSUM(fun th-> MRESA1_TAC th`ds2:real^3#real^3#real^3#real^3->bool`
THEN MRESA1_TAC th`f:real^3#real^3#real^3#real^3->bool`)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
]);;
let CFYXFTY0=
prove(`!p:real^3->bool f.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f facet_of p 
==>  EDGES0_FAN p f = edges f`,

SET_TAC[MAP_EDGES_FACET_INTO_E1_FAN; MAP_EDGES_FACET_INTO_E1_FAN_INJ]);;

let CFYXFTY1=
prove(`!p:real^3->bool f f1.
 bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p 
/\ f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p)) 
/\ f1 facet_of p /\ 							 
 fchanged f1 =dartset_leads_into_fan (vec 0) (vertices p) (edges p) f
==>   EDGES0_FAN p f1 = {{pr2 e, pr3 e}|  e IN f} `,

REPEAT STRIP_TAC
THEN REWRITE_TAC[EXTENSION]
THEN GEN_TAC
THEN EQ_TAC
THENL[  MRESA_TAC EDGES0_SUBSET_FAN[`p:real^3->bool`;`f:real^3#real^3#real^3#real^3->bool`;`f1:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN SET_TAC[];
 MRESA_TAC SUBSET_EDGES0_FAN [`p:real^3->bool`;`f:real^3#real^3#real^3#real^3->bool`;`f1:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;

end;;