(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                                   *)
(* Author: Nguyen Quang Truong                                          *)
(* Date: 2013 - 5 - 31                                                        *)
(* ========================================================================== *)


(* ================================================================ *)




module Lunar_deform = struct


open Hales_tactic;;
open Localization;;
open Wrgcvdr_cizmrrh;;
open Fan;;
open Fan_defs;;
open Localization;;
open Hypermap;;
open Hypermap_iso;;
open Conforming;;
open Sphere;;


(* ================================== *)




(*
let asms_search0 sths =
  let rec immediatesublist l1 l2 =
    match (l1,l2) with
      [],_ -> true
    | _,[] -> false
    | (h1::t1,h2::t2) -> h1 = h2 & immediatesublist t1 t2 in
  let rec sublist l1 l2 =
    match (l1,l2) with
      [],_ -> true
    | _,[] -> false
    | (h1::t1,h2::t2) -> immediatesublist l1 l2 or sublist l1 t2 in
  let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th)
  and name_contains s (n,th) = sublist (explode s) (explode n) in
  let rec filterpred tm =
    match tm with
      Comb(Var("<omit this pattern>",_),t) -> not o filterpred t
    | Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
    | Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)
    | pat -> exists_subterm_satisfying (can (term_match [] pat)) in
  fun pats ->
    let triv,nontriv = partition is_var pats in
    (if triv <> [] then
      warn true
         ("Ignoring plain variables in search: "^
          end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv))
     else ());
    (if nontriv = [] & triv <> [] then []
     else itlist (filter o filterpred) pats sths);;

let asms_search tms =
  let gstk = !current_goalstack in
  match gstk with
    [] -> []
  | (meta,gl::_,just)::_
       -> let (sths,_) = gl in
          map snd (asms_search0 sths tms)
  | _  -> failwith "asm_searchs: Invalid goal state";;

let ASMS_SEARCH_TCL (tms:(term)list) (thstac:(thm)list->tactic) : tactic =
  fun (gl:goal) ->
  let (sths,tm) = gl in
  let ths1 = map snd (asms_search0 sths tms) in
  thstac ths1 gl;;

let ASM_SEARCH_TCL (tms:(term)list) (thstac:thm->tactic) : tactic =
  let foo ths = match ths with
                  [] -> failwith "ASM_SEARCH_TCL: No matching asms found"
                | _  -> thstac (hd ths) in
  ASMS_SEARCH_TCL tms foo;;

let ASM_SEARCH_TC = asms_search;;
*)

let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;

let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (SPEC_ALL ( tm ))];;

let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `; MESON[]`
a ==> b ==> c <=> a /\ b ==> c `];;

let DOWN_TAC = REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IMP_IMP] THEN PHA;;


let DOWN = FIRST_X_ASSUM MP_TAC;;

let DOWNS n = REPLICATE_TAC n DOWN THEN PHA;;

let REMOVE_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (TAUT` a ==> b ==> a`);;


(*
let types_thm th = let cl = concl th in
List.map dest_var (frees cl );;

let seans_fn () =
let (tms,tm) = top_goal () in
let vss = map frees (tm::tms) in
let vs = setify (flat vss) in
map dest_var vs;;
*)




let PAT_REWRITE_TAC tm thms =
(CONV_TAC (PAT_CONV tm (REWRITE_CONV thms )));;

let FOR_ASM th =
let th1 = REWRITE_RULE[MESON[]` a /\ b ==> c <=>
a ==> b ==> c `] th in
let th2 = SPEC_ALL th1 in UNDISCH_ALL th2;;

(* change a th having form |- A ==> t to the form A |- t
to get ready to some other commands


|- A ==> t
----------- FOR_ASM
A |- t
*)

let ASSUME_TAC2 = ASSUME_TAC o FOR_ASM;;


let PAT_ONCE_REWRITE_TAC tm thms =
(CONV_TAC (PAT_CONV tm (ONCE_REWRITE_CONV thms )));;

let ASM_PAT_RW_TAC tm thms = EVERY_ASSUM (fun th ->
(CONV_TAC (PAT_CONV tm (ONCE_REWRITE_CONV
( th ::[ thms ] )))));;

let PAT_TH_TAC tm th =
(CONV_TAC (PAT_CONV tm (REWRITE_CONV[th] )));;


let IMP_TO_EQ_RULE th = MATCH_MP (TAUT` (a ==> b ) ==>
( a <=> a /\ b )`) (SPEC_ALL th);;

let NHANH_PAT tm th = PAT_ONCE_REWRITE_TAC tm
[ IMP_TO_EQ_RULE th ];;


let MAKE_FIRST_TAC tm = UNDISCH_TAC tm THEN DISCH_TAC;;


(* ---------- BG TEST ------------- *)


(*
let rec els L = match L with
[] -> p ()
| (x::l) -> e x; els l;;

let rec bls L = match L with
[] -> p ()
| (x::l) -> b (); bls l;;
*)

(* ============================================= *)



let CONS_IMP_CONTINUOUS_ATREAL = 
prove_by_refinement(` (! t. t IN real_interval (a,b) ==> f t = (u:real^N) )
==> (! t. t IN real_interval (a,b) ==> f continuous atreal t ) `,

[REWRITE_TAC[continuous_atreal; real_interval; IN_ELIM_THM];
REPEAT STRIP_TAC;
EXISTS_TAC` min (b - t ) ( t - a ) ` ;
CONJ_TAC;
REWRITE_TAC[REAL_LT_MIN];
ASM_REAL_ARITH_TAC;
GEN_TAC;
REWRITE_TAC[REAL_LT_MIN];
STRIP_TAC;
ASSUME_TAC2 (REAL_ARITH` a < t /\ t < b /\ abs (x' - t) < b - t /\ abs (x' - t) < t - a ==> x' < b  /\ a < x' `);
SUBGOAL_THEN ` f (x':real) = (u:real^N) ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[DIST_REFL]]);;

let AFF_GT_SUBSET_AFFINE_HULL21 = ISPECL [` {u, v:real^N} `;` {w:real^N } `] AFF_GT_SUBSET_AFFINE_HULL;;



let DISJTINCT_PROPERTY = 
prove_by_refinement (
` FINITE V /\
(f : real^N -> real -> real^N) u continuous atreal (&0) /\
 f u (&0) = u /\
 a < &0 /\
 &0 < b /\
 (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u')
 ==> (?e. &0 < e /\
          (!t u'.
               --e < t /\ t < e /\ u' IN V /\ ~(u' = u) ==> ~(f u t = f u' t)))`,
 [
STRIP_TAC;
SUBGOAL_THEN`!u'. u' IN V /\ ~(u = u') ==> (!t. t IN real_interval (a,b) ==>
(f: real^N -> real -> real^N) u' continuous atreal t )` ASSUME_TAC;
GEN_TAC THEN STRIP_TAC;
MATCH_MP_TAC (GEN`u: real^N ` CONS_IMP_CONTINUOUS_ATREAL);
EXISTS_TAC` u': real^N `;
REPEAT STRIP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
MP_TAC (ISPECL [` &0 `;` u:real^N `;` f: real^N -> real -> real^N `; 
` V:real^N -> bool `] (GEN_ALL Local_lemmas1.CONTINUOUS_FUN_DISTINCT_FINITE_SET));
ANTS_TAC;
ASM_REWRITE_TAC[];
ANTS_TAC;
CONJ_TAC;
REPEAT STRIP_TAC;
SUBGOAL_THEN` &0 IN real_interval (a,b) ` MP_TAC;
ASM_REWRITE_TAC[real_interval; IN_ELIM_THM];
ASM_MESON_TAC[];
GEN_TAC;
REWRITE_TAC[IN_INSERT];
STRIP_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` &0 IN real_interval (a,b) ` MP_TAC;
ASM_REWRITE_TAC[real_interval; IN_ELIM_THM];
ASM_MESON_TAC[];

REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT];
MESON_TAC[]]);;




let EDGE_FORM_IN_LOCAL_FAN = 
prove_by_refinement(
` local_fan (V,E,FF) /\ x IN E ==> ? u v. ~( u = v ) /\ {u, v} = x `,

[REWRITE_TAC[local_fan; FAN; graph; IN];
LET_TAC; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x:real^3 -> bool `));
DOWN; REWRITE_TAC[Local_lemmas1.HAS_SIZE_2_EXISTS2]; MESON_TAC[]]);;




let EDGE_IN_LOCAL_FAN_DET_RHO_NODE = 
prove_by_refinement
(` local_fan (V,E,FF) /\ x IN E ==> (?v. v IN V /\ {v, rho_node1 FF v} = x) `,

[NHANH EDGE_FORM_IN_LOCAL_FAN;
STRIP_TAC;
UNDISCH_TAC` (x:real^3 -> bool) IN E `;
UNDISCH_TAC` local_fan (V,E,FF) `;
PHA;
EXPAND_TAC "x";
NHANH Local_lemmas.LOFA_IN_E_IMP_IN_FF;
STRIP_TAC;
DOWN;
UNDISCH_TAC` local_fan (V,E,FF) `;
PHA;
NHANH Local_lemmas.DETER_RHO_NODE;
STRIP_TAC;
EXISTS_TAC `u: real^3 `;

ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V; Local_lemmas.DETER_RHO_NODE; INSERT_COMM];
ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V; Local_lemmas.DETER_RHO_NODE; INSERT_COMM]]);;





let TOW_POINTS_IN_IMP_AFF_GT_SUBSET = 
prove_by_refinement
(` DISJOINT {x, u} {v:real^N } /\ 
a IN aff_gt {x,u} {v} /\
b IN aff_gt {x, u} {v} /\
DISJOINT {x} {a,b} 
==> aff_gt {x} {a,b} SUBSET aff_gt {x,u} {v} `,

[NHANH AFF_GT_2_1;
NHANH AFF_GT_1_2;
STRIP_TAC;
UNDISCH_TAC` a IN aff_gt {x, u} {v:real^N }`;
UNDISCH_TAC` b IN aff_gt {x, u} {v:real^N }`;
ASM_REWRITE_TAC[IN_ELIM_THM; SUBSET];
STRIP_TAC;
STRIP_TAC;
GEN_TAC;
STRIP_TAC;
DOWN;
ASM_REWRITE_TAC[];
REWRITE_TAC[VECTOR_ARITH`  t1'' % x +

 t2'' % (t1' % x + t2' % u + t3' % v) +
 t3'' % (t1 % x + t2 % u + t3 % v) = 
(t1'' + t2'' * t1' + t3'' * t1 ) % x + (t2'' * t2' + t3'' * t2) % u + 
(t2'' * t3' + t3'' * t3 ) % v `];
STRIP_TAC;
EXISTS_TAC` (t1'' + t2'' * t1' + t3'' * t1:real) `;
EXISTS_TAC` t2'' * t2' + t3'' * t2:real `;
EXISTS_TAC` t2'' * t3' + t3'' * t3 `;
CONJ_TAC;
MATCH_MP_TAC Real_ext.REAL_PROP_POS_ADD2;
ASM_MESON_TAC[REAL_LT_MUL];
ASM_REWRITE_TAC[];

UNDISCH_TAC` t1' + t2' + t3' = &1 `;
UNDISCH_TAC` t1 + t2 + t3 = &1 `;
UNDISCH_TAC` t1'' + t2'' + t3'' = &1 `;
PHA;
CONV_TAC REAL_RING]);;



let REAL_LT_MUL12 = 
prove(` &0 < b /\ a < &0 ==> a * b < &0 `,

REWRITE_TAC[REAL_ARITH` a * b < &0 <=> &0 < (-- a) * (b ) `] THEN 
STRIP_TAC THEN 
MATCH_MP_TAC REAL_LT_MUL THEN 
DOWN_TAC THEN 
REAL_ARITH_TAC);;

let COLL_IN_AFF_GT_INTER_EMPTY = 
prove_by_refinement
(` ~ collinear {a,b,x: real^N} /\ u IN aff_gt {a,b} {x} ==>
aff_gt {a, b} {x} INTER aff_lt {a} {u} = {} `,

[NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
NHANH Fan.th3a;
STRIP_TAC;
DOWN;
NHANH (SET_RULE` DISJOINT {a, b} {u} ==> DISJOINT {a} {u} `);
NHANH AFF_LT_1_1;
STRIP_TAC;
UNDISCH_TAC` DISJOINT {a, b} {x: real^N} `;
NHANH AFF_GT_2_1;
STRIP_TAC;
UNDISCH_TAC` u IN aff_gt {a, b} {x: real^N} `;
ASM_REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
REWRITE_TAC[SET_RULE` A INTER B = {} <=> (! x. x IN B ==> ~( x IN A)) `];
REWRITE_TAC[IN_ELIM_THM];
GEN_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[];

REWRITE_TAC[Local_lemmas.VECTOR_ADD_LDISTRIB1];
STRIP_TAC;
SUBGOAL_THEN` (t1' + t2' * t1 ) + (t2' * t2 ) + (t2' * t3) = &1 ` ASSUME_TAC;
ASM_REWRITE_TAC[REAL_RING` (t1' + t2' * t1) + t2' * t2 + t2' * t3 = t1' + t2' * (t1 + t2 + t3 ) `; REAL_ARITH` a * &1 = a `];
ABBREV_TAC` vv: real^N = t1'' % a + t2'' % b + t3' % x ` ;
SUBGOAL_THEN` (vv: real^N) IN affine hull {a, b, x} ` ASSUME_TAC;
ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];
ASM_MESON_TAC[];
UNDISCH_TAC` ~collinear {a, b, x:real^N} `;
DOWN THEN PHA;
NHANH Collect_geom.lemma11;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [` t1'': real `;` t2'': real `;` t3': real `]));
ANTS_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o (SPECL [` (t1': real) + t2' * t1`;`( t2': real ) * t2 `;` (t2': real) * t3 `]));
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` t1' % a + (t2' * t1) % a + (t2' * t2) % b + (t2' * t3) % x = (vv: real^N) `;
ASM_REWRITE_TAC[];
DISCH_THEN (SUBST1_TAC o SYM);
CONV_TAC VECTOR_ARITH;
STRIP_TAC;
STRIP_TAC;
DOWN;
EXPAND_TAC "t3''";
ASSUME_TAC2 (SPECL [` t2': real `;` t3: real `] (GEN_ALL REAL_LT_MUL12));
DOWN;
UNDISCH_TAC` &0 < t3' `;
REAL_ARITH_TAC]);;






let HKIRPEP_ALT = 
prove(` convex_local_fan (V,E,FF) /\ lunar (v,w) V E
     ==> (!u. u IN V DIFF {v, w} ==> interior_angle1 (vec 0) FF u = pi) /\
         &0 < interior_angle1 (vec 0) FF v /\
         interior_angle1 (vec 0) FF v <= pi /\
         interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w /\
         (?i j. i + j = CARD V /\ i < CARD V /\
              ~(i = 0) /\
              ~(i = 1) /\
              w = ITER i (rho_node1 FF) v /\
              {ITER l (rho_node1 FF) v | 0 < l /\ l < i} =
              aff_gt {vec 0, v} {rho_node1 FF v} INTER V /\
        j < CARD V /\
              ~(j = 0) /\
              ~(j = 1) /\
              v = ITER j (rho_node1 FF) w /\
              {ITER l (rho_node1 FF) w | 0 < l /\ l < j} =
              aff_gt {vec 0, v} {ivs_rho_node1 FF v} INTER V) `,

NHANH Local_lemmas.HKIRPEP THEN
STRIP_TAC THEN
UNDISCH_TAC` v = ITER j (rho_node1 FF) w ` THEN
UNDISCH_TAC` w = ITER i (rho_node1 FF) v ` THEN
DISCH_THEN (ASSUME_TAC o SYM) THEN
DISCH_THEN (ASSUME_TAC o SYM) THEN
ASM_REWRITE_TAC[] THEN
EXISTS_TAC` i: num ` THEN
EXISTS_TAC` j:num ` THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC (GEN_ALL Local_lemmas1.CARD_V_TWO_HAFL_CIRCLE) THEN
EXISTS_TAC` E: (real^3 -> bool) -> bool ` THEN
EXISTS_TAC` FF: real^3 # real^3 -> bool ` THEN
EXISTS_TAC` w:real^3 ` THEN
EXISTS_TAC` v: real^3 ` THEN
ASM_REWRITE_TAC[] THEN
UNDISCH_TAC` convex_local_fan (V,E,FF)` THEN
UNDISCH_TAC ` lunar (v,w:real^3) V E ` THEN
SIMP_TAC[convex_local_fan; lunar; INSERT_SUBSET]);;





let LUNAR_IMP_IN_TWO_HAFLS_PLANE = 
prove_by_refinement (` convex_local_fan (V,E,FF) /\ lunar (v,w) V E ==>
(! u. u IN V /\ ~( u = v ) /\ ~( u = w) ==> u IN aff_gt {vec 0, v} {rho_node1 FF v} \/ u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} ) `,

[NHANH HKIRPEP_ALT;
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO;
SUBGOAL_THEN` lunar (v,w:real^3) V E ` MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
REWRITE_TAC[lunar; circular; INSERT_SUBSET];
STRIP_TAC;
ASSUME_TAC2 (SPEC_ALL Localization.LOFA_IMP_LT_CARD_SET_V_ALT);
GEN_TAC THEN STRIP_TAC;
UNDISCH_TAC` (u:real^3) IN V `;
EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
ASM_CASES_TAC` n = 0 `;
FIRST_X_ASSUM (SUBST_ALL_TAC);
DOWN;
UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[ITER];
ASM_CASES_TAC` n < (i:num) `;
DISJ1_TAC;

UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);


SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n: num `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~( n = 0) `;
ARITH_TAC;
ASM_SIMP_TAC[IN_INTER];

ASM_CASES_TAC` n = (i:num) `;
UNDISCH_TAC` u = ITER n (rho_node1 FF) v `;
UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];

DISJ2_TAC;
SUBGOAL_THEN`u IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n - (i:num ) `;

UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
EXPAND_TAC "w";
REWRITE_TAC[ITER_ADD];
ASSUME_TAC2 (ARITH_RULE` ~( n < i) ==> n - i + i = (n:num ) `);
ASM_REWRITE_TAC[];
ASSUME_TAC2 (ARITH_RULE` ~(n < i) ==> (n - i < j <=> (n:num) < i + j ) `);
ASM_REWRITE_TAC[ARITH_RULE` 0 < n - i <=> ~( n < i ) /\ ~( n = (i:num)) `];

UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);

ASM_SIMP_TAC[IN_INTER]]);;





let IN_CONV0_IMP_AFF_EQ1 = 
prove(` a IN conv0 {x, y} ==> aff {a, x} = aff {a, y} `,

NHANH Local_lemmas.IN_CONV0_IMP_AFF_EQ THEN 
ONCE_REWRITE_TAC[INSERT_COMM] THEN 
NHANH Local_lemmas.IN_CONV0_IMP_AFF_EQ THEN 
ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 
SIMP_TAC[INSERT_COMM]);;



let AFF_LT_SUBSET_AFF11 = 
prove_by_refinement (
` DISJOINT {a} {b} ==> aff_lt {a} {b} SUBSET aff {a,b:real^N} `,

[NHANH AFF_LT_1_1;
SIMP_TAC[Collect_geom.AFF_2POINTS_INTERPRET; SUBSET; IN_ELIM_THM];
STRIP_TAC;
GEN_TAC;
STRIP_TAC;
EXISTS_TAC` t1: real `;
EXISTS_TAC` t2: real `;
ASM_REWRITE_TAC[]]);;



let IN_AFF_LT_STILL_NOT_COLLINEAR = 
prove_by_refinement
(` ~ collinear {x: real^N,y,a} /\ b IN aff_lt {x, y} {a} ==>
~ collinear {x,y,b} `,

[REPEAT STRIP_TAC;
UNDISCH_TAC` b IN aff_lt {x, y} {a: real^N} `;
PHA;
UNDISCH_TAC ` ~collinear {x, y, a: real^N} `;
NHANH Fan.th3a;
NHANH AFF_LT_2_1;
SIMP_TAC[IN_ELIM_THM];
REPEAT STRIP_TAC;
UNDISCH_TAC` ~collinear {x, y, a:real^N} `;
PHA;
UNDISCH_TAC` collinear {x,y,b:real^N} `;
REWRITE_TAC[Local_lemmas.collinear_fan22; Collect_geom.AFF_2POINTS_INTERPRET; IN_ELIM_THM];
STRIP_TAC;
DISJ1_TAC;
DOWN;
ASM_REWRITE_TAC[];
REWRITE_TAC[
VECTOR_ARITH` t1 % x + t2 % y + t3 % a = ta % x + tb % y <=>  t3 % a = (ta - t1) % x + (tb - t2) % y `];
NHANH_PAT`\x. x ==> y `  (MESON[]` a = b ==> ( &1 / t3) % a = (&1 / t3) % b `);
REWRITE_TAC[Local_lemmas.VECTOR_ADD_LDISTRIB1];
ASSUME_TAC2 (REAL_FIELD` t3 < &0 ==> &1 / t3 * t3 = &1 `);
ASM_REWRITE_TAC[VECTOR_MUL_LID];
SIMP_TAC[];
STRIP_TAC;
EXISTS_TAC` (&1 / t3 * (ta - t1)) `;
EXISTS_TAC` (&1 / t3 * (tb - t2)) `;
ASM_REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; REAL_ARITH` a - x + b - y = (a + b ) - ( x + y )`];
UNDISCH_TAC`t1 + t2 + t3 = &1 `;
ASM_SIMP_TAC[REAL_ARITH` a + b + c = &1 <=> &1 - ( a + b ) = c `];

ASM_REWRITE_TAC[]]);;




let AZIM_PI_LEMMA = 
prove_by_refinement
(` ~(aff_gt {u} s INTER aff_lt {u} {a} = {} ) /\
aff_gt {u} s SUBSET aff_gt {u, v} {y} /\
a IN aff_gt {u, v} {x} /\
~ collinear {u, v, x} /\
~ collinear {u, v, y} 
==> azim u v x y = pi `,

[MP_TAC (
ISPECL [`{u: real^3} `;` {u, v:real^3} `; `{a: real^3 }`] AFF_LT_MONO_LEFT);
ANTS_TAC;
CONV_TAC SET_RULE;
REPEAT STRIP_TAC;
SUBGOAL_THEN` aff_gt {u,v} {x} = aff_gt {u,v} {a:real^3} ` MP_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];
DISCH_THEN (ASSUME_TAC o SYM);
ASSUME_TAC2 (
SET_RULE` ~(aff_gt {u: real^3} s INTER aff_lt {u} {a} = {}) /\
aff_lt {u} {a} SUBSET aff_lt {u, v} {a} /\
aff_gt {u} s SUBSET aff_gt {u, v} {y}
==> ~ ( aff_gt {u, v} {y} INTER aff_lt {u, v} {a} = {} ) `);
DOWN;
REWRITE_TAC[SET_RULE` ~( A INTER B = {} ) <=> ? x. x IN A /\ x IN B `];
STRIP_TAC;
UNDISCH_TAC` x' IN aff_gt {u, v} {y:real^3} `;
UNDISCH_TAC` ~ collinear {u, v, y:real^3} `;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
STRIP_TAC;
SUBGOAL_THEN` ~ collinear {u, v, a: real^3} ` ASSUME_TAC;
MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
EXISTS_TAC` x: real ^3 `;
ASM_REWRITE_TAC[];

UNDISCH_TAC` ~collinear {u, v, x' : real^3} `;
UNDISCH_TAC` ~collinear {u, v, a: real^3} `;
PHA;
NHANH AZIM_EQ_PI_ALT;
STRIP_TAC;


SUBGOAL_THEN` azim u v a x' = azim u v a y ` MP_TAC;
MATCH_MP_TAC AZIM_EQ_IMP;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (ASSUME_TAC o SYM);

STRIP_TAC;
UNDISCH_TAC` x' IN aff_lt {u, v} {a:real^3} `;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` azim u v a y = azim u v x y ` MP_TAC;
ONCE_REWRITE_TAC[ Rogers.AZIM_EQ_SYM];
MATCH_MP_TAC (* Polar_fan. *) AZIM_EQ_IMP;
ASM_REWRITE_TAC[];
SIMP_TAC[]]);;



(* ================================================== *)










let SUB_LUNAR_DEFORM_LEMMA = 
prove_by_refinement(` FINITE V /\ convex_local_fan (V,E,FF) /\ lunar (v,w) V E /\
(! x. x IN E ==> x SUBSET V) /\
f (u:real^3) (&0 ) = u /\
f u continuous atreal (&0) /\
interior_angle1 (vec 0) FF v < pi /\
a < &0  /\ &0 < b /\
     u IN V /\
     ~(u = v) /\
     ~(u = w) /\
     (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
     (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})

==> (?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> 
                       lunar (v,w) (IMAGE (\v. f v t) V)
                       (IMAGE (IMAGE (\v. f v t)) E)))`,

[
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.HKIRPEP;
DOWN_TAC;
REWRITE_TAC[lunar; circular];
STRIP_TAC;
SUBGOAL_THEN` ! t. t IN real_interval (a,b) ==>  {v, w} SUBSET IMAGE (\v. (f:real^3->real->real^3) v t) V ` ASSUME_TAC;

REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_IMAGE];
REPEAT STRIP_TAC;
EXISTS_TAC` v:real^3` ;
SUBGOAL_THEN` (v:real^3) IN V ` MP_TAC;
MATCH_MP_TAC (SET_RULE` {v, w:real^3} SUBSET V ==> v IN V`);
FIRST_X_ASSUM ACCEPT_TAC;
SIMP_TAC[];
FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` &0 `));
FIRST_X_ASSUM (ASSUME_TAC o (ISPECL[ ` v:real^3`; ` t:real `]));
STRIP_TAC;
ONCE_REWRITE_TAC[EQ_SYM_EQ];
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
EXISTS_TAC` w:real^3 `;



SUBGOAL_THEN` (w:real^3) IN V ` ASSUME_TAC;
MATCH_MP_TAC (SET_RULE` {v, w} SUBSET V ==> w IN V ` );
FIRST_X_ASSUM ACCEPT_TAC;
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o GSYM);
ASM_REWRITE_TAC[];



FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` &0 `)) THEN
FIRST_X_ASSUM (ASSUME_TAC o (SPECL[ ` w:real^3 `; ` t:real `]));



ONCE_REWRITE_TAC[EQ_SYM_EQ];
FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[];

ABBREV_TAC` CONCL = ?e. &0 < e /\
     (!t. --e < t /\ t < e
          ==> ~(?v w u.
                    {v, w} IN IMAGE (IMAGE (\v. (f:real^3 -> real -> real^3) v t)) E /\
                    u IN IMAGE (\v. f v t) V /\
                    ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\
              {v, w} SUBSET IMAGE (\v. f v t) V /\
              ~(v = w) /\
              collinear {vec 0, v, w}) `;


MP_TAC (ISPEC`V: real^3 -> bool ` (GEN`V: real^N -> bool ` DISJTINCT_PROPERTY));

ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;

SUBGOAL_THEN` t IN real_interval (a,b) /\ --e < t /\ t < e
                ==> (!v w u'.
                          {v, w} IN IMAGE (IMAGE (\v. (f:real^3 -> real -> real^3) v t)) E /\
                          u' IN IMAGE (\v. f v t) V /\
 ~( f u t IN {u' ,v, w} )
==> (aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u'} =
                            {})) ` ASSUME_TAC;
REWRITE_TAC[IN_IMAGE];
REPEAT STRIP_TAC;

SUBGOAL_THEN` x SUBSET (V:real^3 -> bool ) ` ASSUME_TAC;
FIRST_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
ASM_CASES_TAC` (u:real^3) IN x `;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN {v', w'} ` ASSUME_TAC;
UNDISCH_TAC` {v': real^3, w'} = IMAGE (\v. (f:real^3 -> real -> real^3) v t) x `;
SIMP_TAC[IN_IMAGE];
STRIP_TAC;

EXISTS_TAC` u:real^3 `;
ASM_REWRITE_TAC[];
DOWN;
REPLICATE_TAC 3 DOWN;
SIMP_TAC[IN_INSERT];
MESON_TAC[]; 
SUBGOAL_THEN` t IN real_interval (a, b) ==> IMAGE (\v. (f:real^3 -> real -> real^3) v t ) x = x ` MP_TAC;
STRIP_TAC;
MATCH_MP_TAC Counting_spheres.pad2d3d_dropout_lemma;
EXISTS_TAC` \x. (x:real^3) IN V /\ ~( x = u ) ` ;
CONJ_TAC;
GEN_TAC;
REWRITE_TAC[BETA_THM];
DOWN THEN DOWN THEN DOWN;
REWRITE_TAC[SUBSET];
MESON_TAC[];
GEN_TAC;
REWRITE_TAC[BETA_THM];
STRIP_TAC;
UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> (f: real^3 -> real -> real^3) u' t = u' `;
DISCH_THEN MATCH_MP_TAC;
ASM_REWRITE_TAC[];
DISCH_THEN ASSUME_TAC2;
FIRST_X_ASSUM SUBST_ALL_TAC;

ASM_CASES_TAC` x' = (u:real^3) `;
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC` ~((f:real^3 -> real -> real^3 ) u t IN {u', v', w'}) ` ;
ASM_REWRITE_TAC[IN_INSERT];
SUBGOAL_THEN` (f: real^3 -> real -> real^3) x' t = x' ` MP_TAC;
UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> (f: real^3 -> real -> real^3 ) u' t = u' ` ;
DISCH_THEN MATCH_MP_TAC;
ASM_REWRITE_TAC[];
DISCH_THEN SUBST_ALL_TAC;
UNDISCH_TAC` ~(?v w u.
            {v, w} IN E /\
            u IN V /\
            ~(aff_gt {vec 0} {v, w: real^3} INTER aff_lt {vec 0} {u} = {})) `;

UNDISCH_TAC` x': real^3 IN V `;
UNDISCH_TAC` (x: real^3 -> bool) IN E `;
EXPAND_TAC "x'";
EXPAND_TAC "x";
MESON_TAC[];

ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO;
MP_TAC (SPECL [` i:num `;` j:num `] (GENL[` n:num `;` n': num `] Local_lemmas1.CARD_V_TWO_HAFL_CIRCLE));
ANTS_TAC;
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[SET_RULE` x IN A /\ y IN A <=> {x,y} SUBSET A `];
STRIP_TAC;
ASSUME_TAC2 (SET_RULE` {v, w:real^3} SUBSET V ==> v IN V `);
ASSUME_TAC2 Localization.LOFA_IMP_LT_CARD_SET_V_ALT;
UNDISCH_TAC` (u:real^3) IN V `;
EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
UNDISCH_TAC` v = ITER j (rho_node1 FF) w ` ;
DOWN;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
MP_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ;
ANTS_TAC;
ASM_REWRITE_TAC[lunar; circular];
DISCH_THEN (ASSUME_TAC o SYM);
FIRST_X_ASSUM SUBST_ALL_TAC;
SUBGOAL_THEN` u IN aff_gt {vec 0, v} {rho_node1 FF v} \/ u IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC;

ASM_CASES_TAC` (n:num) < i ` ;
DISJ1_TAC;
ASM_CASES_TAC` n = 0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
REPLICATE_TAC 4 DOWN THEN PHA;
ASM_REWRITE_TAC[ITER];
SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` ASSUME_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n: num `;
ASM_REWRITE_TAC[];
DOWN THEN DOWN;
ARITH_TAC;
DOWN;
ASM_SIMP_TAC[IN_INTER];
ASM_CASES_TAC` (n:num) = i ` ;
FIRST_X_ASSUM SUBST_ALL_TAC;
REPLICATE_TAC 2 DOWN THEN PHA;
ASM_REWRITE_TAC[];
DISJ2_TAC;
ASSUME_TAC2 (ARITH_RULE` ~( n:num < i) ==> i + ( n - i ) = n`);
SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j}` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` (n: num) - i `;
EXPAND_TAC "w";
ASM_REWRITE_TAC[ITER_ADD; ADD_SYM];
REPLICATE_TAC 3 DOWN THEN PHA;
SIMP_TAC[ (ARITH_RULE` ~((n:num) < i) ==> ( n - i < j <=> n < i + j ) `)];
ASM_REWRITE_TAC[];
ARITH_TAC;
ASM_SIMP_TAC[IN_INTER];

ASSUME_TAC2 (SET_RULE` {v, w:real^3} SUBSET V ==> w IN V `);
MP_TAC (SPEC` w:real^3 ` Local_lemmas.LOFA_IMP_LT_CARD_SET_V);
ANTS_TAC;
ASM_SIMP_TAC[SET_RULE` {a,b} SUBSET V ==> b IN V `];
STRIP_TAC;
SUBGOAL_THEN` u IN {ITER n (rho_node1 FF) v | n < CARD (V:real^3 -> bool)} ` ASSUME_TAC;
EXPAND_TAC "u";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n:num `;
ASM_REWRITE_TAC[];
DOWN;
ASM_REWRITE_TAC[];
EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;

DOWN;
DISCH_THEN (ASSUME_TAC o SYM);

DOWN_TAC;
REWRITE_TAC[TAUT` a /\ b /\ c <=> (a /\ b) /\ c `];
SPEC_TAC (`n':num `,` n': num ` );
SPEC_TAC (`n:num `,` n: num ` );

SPEC_TAC (`v:real^3 `, ` v:real^3 `);
SPEC_TAC (`i: num `,` i:num ` );
SPEC_TAC (`w:real^3 `, ` w:real^3 `);
SPEC_TAC (`j: num `,` j:num ` );




MATCH_MP_TAC (
MESON[]` (! j w i v n n'. P j w i v n n' ==> P i v j w n' n) /\ (! j w i v n n'. P j w i v n n' /\ u IN Q v ==> concl ) ==>
(! j w i v n n'. P j w i v n n'/\ (u IN Q v \/ u IN Q w ) ==> concl )`);
CONJ_TAC;
SIMP_TAC[];
SIMP_TAC[INSERT_COMM; ADD_SYM];
REPEAT GEN_TAC;
STRIP_TAC;
CONJ_TAC;
UNDISCH_TAC` interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w ` ;
DISCH_THEN (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[];
UNDISCH_TAC`(?e. &0 < e /\
           (!t. --e < t /\ t < e
                ==> ((~(?v w u.
                            ({v, w} IN IMAGE (IMAGE (\v. f v t)) E /\
                             u IN IMAGE (\v. f v t) V) /\
                            ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} =
                              {})) /\
                      {v, w} SUBSET IMAGE (\v. (f:real^3 -> real -> real^3) v t) V) /\
                     ~(v = w)) /\
                    collinear {v, w, vec 0})) <=>
      CONCL`;
ASM_REWRITE_TAC[];
PHA;
REPEAT STRIP_TAC; 





(* ====================================

prove_by_refinement (`FINITE V /\
 convex_local_fan (V,E,FF) /\
 ~(?v w u.
       {v, w} IN E /\
       u IN V /\
       ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\
 {v, w} SUBSET V /\
 ~(v = w) /\
 collinear {vec 0, v, w} /\
 (!x. x IN E ==> x SUBSET V) /\
 f u (&0) = u /\
 f u continuous atreal (&0) /\
 interior_angle1 (vec 0) FF v < pi /\
 a < &0 /\
 &0 < b /\
 ~(u = v) /\
 ~(u = w) /\
 (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
 (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u}) /\
 (!u. u IN V DIFF {v, w} ==> interior_angle1 (vec 0) FF u = pi) /\
 &0 < interior_angle1 (vec 0) FF v /\
 interior_angle1 (vec 0) FF v <= pi /\
 interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w /\
 i < CARD V /\
 ~(i = 0) /\
 ~(i = 1) /\
 {ITER l (rho_node1 FF) v | 0 < l /\ l < i} =
 aff_gt {vec 0, v} {rho_node1 FF v} INTER V /\
 j < CARD V /\
 ~(j = 0) /\
 ~(j = 1) /\
 {ITER l (rho_node1 FF) w | 0 < l /\ l < j} =
 aff_gt {vec 0, w} {rho_node1 FF w} INTER V /\
 (!t. t IN real_interval (a,b) ==> {v, w} SUBSET IMAGE (\v. f v t) V) /\
 ((?e. &0 < e /\
       (!t. --e < t /\ t < e
            ==> ~(?v w u.
                      {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\
                      u IN IMAGE (\v. f v t) V /\
                      ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\
                {v, w} SUBSET IMAGE (\v. f v t) V /\
                ~(v = w) /\
                collinear {vec 0, v, w})) <=>
  CONCL) /\
 &0 < e /\
 (!t u'. --e < t /\ t < e /\ u' IN V /\ ~(u' = u) ==> ~(f u t = f u' t)) /\
 (t IN real_interval (a,b) /\ --e < t /\ t < e
  ==> (!v w u'.
           {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\
           u' IN IMAGE (\v. f v t) V /\
           ~(f u t IN {u', v, w})
           ==> aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u'} = {})) /\
 local_fan (V,E,FF) /\
 i + j = CARD V /\
 v IN V /\
 {ITER n (rho_node1 FF) v | n < CARD V} = V /\
 n < CARD V /\
 ITER n (rho_node1 FF) v = u /\
 ITER j (rho_node1 FF) w = v /\
 ITER i (rho_node1 FF) v = w /\
 w IN V /\
 {ITER n (rho_node1 FF) w | n < CARD V} = V /\
 n' < CARD V /\
 ITER n' (rho_node1 FF) w = u   /\
 u IN aff_gt {vec 0, v} {rho_node1 FF v} 
 ==> CONCL`,

 [STRIP_TAC ;


================================= *)


SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} ` MP_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];
MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2 ;
ASM_REWRITE_TAC[];
STRIP_TAC;
ABBREV_TAC` u1 = ( (u dot v ) / ( v dot v )) % (v:real^3)`;
ABBREV_TAC` uh = u - (u1:real^3) `;
SUBGOAL_THEN` uh dot (v:real^3) = &0 ` ASSUME_TAC;
EXPAND_TAC "uh";
EXPAND_TAC "u1";
REWRITE_TAC[DOT_LSUB; DOT_LMUL];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 ` ));
DOWN;
REWRITE_TAC[GSYM DOT_EQ_0];
CONV_TAC REAL_FIELD;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u continuous atreal (&0) ` MP_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[continuous_atreal];
DISCH_THEN (MP_TAC o (SPEC` norm (uh: real ^3)`));
ANTS_TAC;
REWRITE_TAC[NORM_POS_LT];
STRIP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC` (u:real^3) - u1 = vec 0 ` ;
REWRITE_TAC[VECTOR_SUB_EQ];
EXPAND_TAC "u1";
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
ASSUME_TAC2 (ISPEC` v:real^3 ` (GEN_ALL Local_lemmas.COLLINEAR_ONCE_VEC_0));
FIRST_X_ASSUM (MP_TAC o (SPEC` u: real^3 `));
STRIP_TAC;
STRIP_TAC;
SUBGOAL_THEN` collinear {vec 0, v, u:real^3 } ` MP_TAC;
ASM_REWRITE_TAC[];
DOWN THEN MESON_TAC[];
REWRITE_TAC[];
MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
EXISTS_TAC` rho_node1 FF v `;
ASM_REWRITE_TAC[];
MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
SUBGOAL_THEN` ~ collinear {vec 0, v, u:real^3} ` MP_TAC;
MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
EXISTS_TAC` rho_node1 FF v `;
ASM_REWRITE_TAC[];
NHANH Fan.th3a;
NHANH AFF_GT_2_1;
STRIP_TAC;

SUBGOAL_THEN` (uh: real^3) IN aff_gt {vec 0, v} {u} ` MP_TAC;
ASM_REWRITE_TAC[IN_ELIM_THM];
EXPAND_TAC "uh";
EXPAND_TAC "u1";
EXISTS_TAC` (u dot v) / (v dot (v:real^3))`;
EXISTS_TAC` -- ((u dot v) / (v dot (v:real^3)))`;
EXISTS_TAC` &1 `;
CONJ_TAC;
REAL_ARITH_TAC;
CONJ_TAC;
REAL_ARITH_TAC;
CONV_TAC VECTOR_ARITH;

UNDISCH_TAC` ~collinear {vec 0, v, (u:real^3)}`;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
STRIP_TAC;
MP_TAC (ISPEC` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
ASSUME_TAC (ISPECL [` vec 0: real^3`;`u:real^3`] (GENL [` u:real^N `;` w:real^N `] AFF_GT_SUBSET_AFFINE_HULL21));

SUBGOAL_THEN` {vec 0, v , uh:real^3} SUBSET affine hull {vec 0, v, u}` MP_TAC;
MP_TAC (ISPEC` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
SIMP_TAC[INSERT_SUBSET];
STRIP_TAC;
UNDISCH_TAC` aff_gt {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) ` ;
REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
DISCH_THEN MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
REPEAT STRIP_TAC;
UNDISCH_TAC` uh IN aff_gt {vec 0, v} {u:real^3} `;
UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
STRIP_TAC;
DOWN;
UNDISCH_TAC` {vec 0, v, uh} SUBSET affine hull {vec 0, v, u:real^3} `;
PHA;
NHANH Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ;
STRIP_TAC;
SUBGOAL_THEN` affine hull {vec 0, v, w, u:real^3} = affine hull {vec 0, v, u } ` ASSUME_TAC;
MP_TAC (SPECL [` w:real^3 `;` {vec 0, v, u:real^3} `] Marchal_cells_3.AFFINE_HULL_3_INSERT);
ANTS_TAC;

MP_TAC (ISPECL [` vec 0: real^3 `;` v:real^3 `; ` w:real^3 `] COLLINEAR_3_AFFINE_HULL);
ANTS_TAC;
ONCE_REWRITE_TAC[EQ_SYM_EQ];
ASM_REWRITE_TAC[];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
STRIP_TAC;
SUBGOAL_THEN` collinear {vec 0, v, w:real^3} ` MP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM SUBST1_TAC;
SPEC_TAC (`w:real^3 `,` w:real^3 `);
REWRITE_TAC[GSYM SUBSET];
MATCH_MP_TAC Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA ;
REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET];
REWRITE_TAC[INSERT_COMM];




SUBGOAL_THEN` ! t. -- d < t /\ t < d /\ t IN real_interval (a,b) ==> f u t IN aff_gt {vec 0, v} {u:real^3} ` ASSUME_TAC;
GEN_TAC THEN STRIP_TAC;
UNDISCH_TAC` !t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u:real^3} ` ;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` t':real `));
DOWN;
ASM_REWRITE_TAC[];

REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];
STRIP_TAC;
ASM_CASES_TAC` w' = &0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC` !x'. abs (x' - &0) < d ==> dist ((f: real^3 -> real -> real^3) u x',f u (&0)) < norm (uh: real^3) ` ;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC` t': real `));
REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT];
DISCH_THEN ASSUME_TAC2;
DOWN;
SUBST_ALL_TAC (VECTOR_ARITH` u - u1 = (uh: real^3) <=> u = uh + u1 `);
ASM_REWRITE_TAC[VECTOR_ARITH` u' % vec 0 + v' % v + &0 % uh = v' % v `];
EXPAND_TAC "u1";
REWRITE_TAC[dist; Pack1.norm_ineq_lt; VECTOR_ARITH` a % v - ( u + b % v ) = ( a - b ) % v - u `];
REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_LMUL; DOT_RMUL];
ABBREV_TAC` con1 =  v' - (u dot v) / ((v:real^3) dot v) `;
ASM_REWRITE_TAC[DOT_SYM; Collect_geom.ZERO_NEUTRAL; REAL_ARITH` a - ( &0 - x ) = a + x `];
MP_TAC (ISPEC` v:real^3 ` DOT_POS_LE);
REWRITE_TAC[REAL_ARITH` a + x < x <=> a < &0 `];
MP_TAC (SPEC` con1: real` REAL_LE_SQUARE );
STRIP_TAC;
STRIP_TAC;
ASSUME_TAC2 (SPECL [` con1 * (con1:real)`;` v dot (v:real^3) `] REAL_LE_MUL);
DOWN;
REAL_ARITH_TAC;
ASM_CASES_TAC` w' < &0 `;
UNDISCH_TAC` !x'. abs (x' - &0) < d ==> dist ((f:real^3 -> real -> real^3) u x',f u (&0)) < norm (uh: real^3) `;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC` t': real `));
REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT];
DISCH_THEN ASSUME_TAC2;
DOWN;
SUBST_ALL_TAC (VECTOR_ARITH` u - u1 = uh <=> u = uh + (u1: real^3) `);
ASM_REWRITE_TAC[dist];


REWRITE_TAC[Pack1.norm_ineq_lt] ;
EXPAND_TAC "u1" ;
REWRITE_TAC[VECTOR_ARITH` (u' % vec 0 + v' % v + w' % uh) - (uh + uv % v)
= (v' - uv ) % v + (w' - &1) % uh `] ;
ABBREV_TAC` con1 = (u dot v) / (v dot (v:real^3)) ` ;
ASM_REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; DOT_SYM; Collect_geom.ZERO_NEUTRAL] ;
ASSUME_TAC (ISPEC` v:real^ 3 ` DOT_POS_LE) ;
ASSUME_TAC (SPEC` v' - con1:real ` REAL_LE_SQUARE) ;
ASSUME_TAC (ISPEC` uh:real^ 3 ` DOT_POS_LE) ;
STRIP_TAC ;
MP_TAC (ISPECL [` &1 `;` -- w' + &1 `] Collect_geom.POW2_COND) ;
ANTS_TAC ;
UNDISCH_TAC` w' < &0 ` ;
REAL_ARITH_TAC ;
STRIP_TAC ;
SUBGOAL_THEN` &1 <= -- w' + &1 ` MP_TAC ;
UNDISCH_TAC` w' < &0 ` ;
REAL_ARITH_TAC ;
ASM_REWRITE_TAC[] ;

REWRITE_TAC[REAL_ARITH` &1 pow 2 <= (--w' + &1) pow 2 <=> &0 <= (w' - &1 ) * (w' - &1 ) - &1 `] ;
STRIP_TAC ;
ASSUME_TAC2 (ISPECL[`(w' - &1) * (w' - &1) - &1 `;` (uh:real^3 ) dot uh `] REAL_LE_MUL) ;
ASSUME_TAC2 (ISPECL[`(v' - con1) * (v' - con1)`;` (v:real^3 ) dot v `] REAL_LE_MUL) ;
UNDISCH_TAC` (v' - con1) * (v' - con1) * ((v:real^3) dot v) +
      (w' - &1) * (w' - &1) * (uh dot uh) <
      uh dot (uh: real^3) ` ;
DOWN THEN DOWN ;
REAL_ARITH_TAC ;
SUBGOAL_THEN` f u (t': real) IN aff_gt {vec 0, v} {u:real^3} ` MP_TAC ;
UNDISCH_TAC` aff_gt {vec 0, v} {u} = aff_gt {vec 0, v} {uh:real^3} ` ;
DISCH_THEN SUBST1_TAC ;
UNDISCH_TAC` ~collinear {vec 0, v, uh:real^3} ` ;
NHANH Fan.th3a ;
NHANH AFF_GT_2_1 ;
SIMP_TAC[IN_ELIM_THM] ;
STRIP_TAC ;
EXISTS_TAC` u': real ` ;
EXISTS_TAC` v':real ` ;
EXISTS_TAC` w': real ` ;
ASM_REWRITE_TAC[];


UNDISCH_TAC` ~( w' = &0 ) `;
UNDISCH_TAC` ~( w' < &0 ) `;
REAL_ARITH_TAC;

ASM_REWRITE_TAC[IN_ELIM_THM];


SUBGOAL_THEN` ! t u. abs t < d /\ t IN real_interval (a,b) /\ (u:real^3) IN V ==> f u t IN aff_gt {vec 0, v} {u} ` MP_TAC;
REPEAT STRIP_TAC;
ASM_CASES_TAC` ~(u = u':real^3 )`;
UNDISCH_TAC` !u' t. u' IN V /\ ~(u: real^3 = u') /\ t IN real_interval (a,b) ==> f u' t = u' `;
DISCH_THEN (MP_TAC o (SPECL [` u':real^3 `;` t': real`]));
ANTS_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[];
MP_TAC (ISPECL [` {vec 0, v:real^3} `;` {u':real^3} `] (GEN_ALL Local_lemmas.CONV0_SUBSET_AFF_GT));
SIMP_TAC[Geomdetail.CONV0_SING; INSERT_SUBSET];
DOWN;

REWRITE_TAC[];
DISCH_THEN SUBST_ALL_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[REAL_BOUNDS_LT];
STRIP_TAC;


SUBGOAL_THEN` ! t. abs t < d /\ t IN real_interval (a,b) ==> (! s. s IN IMAGE (IMAGE (\v. f (v:real^3) t)) E ==> aff_gt {vec 0} s SUBSET aff_gt { vec 0, v} {rho_node1 FF v } \/
aff_gt {vec 0} s SUBSET aff_gt { vec 0, w} {rho_node1 FF w })` MP_TAC;




REWRITE_TAC[GSYM REAL_BOUNDS_LT];
PHA;
DOWN;
FIRST_ASSUM NHANH;
STRIP_TAC;
GEN_TAC THEN STRIP_TAC;
GEN_TAC;
REWRITE_TAC[IN_IMAGE];
STRIP_TAC;
DOWN;
UNDISCH_TAC` local_fan (V,E, FF) `;
PHA;
NHANH EDGE_IN_LOCAL_FAN_DET_RHO_NODE;
STRIP_TAC;
UNDISCH_TAC` (v': real^3) IN V `;
EXPAND_TAC "V";


REWRITE_TAC[IN_ELIM_THM];
ONCE_REWRITE_TAC[EQ_SYM_EQ];
STRIP_TAC;
ASM_CASES_TAC` n'' < (j:num ) `;
ASM_CASES_TAC` n'' = 0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN THEN DOWN;
REWRITE_TAC[ITER];
DISCH_THEN (SUBST_ALL_TAC o SYM);
STRIP_TAC;
DISJ2_TAC;
UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = (u': real^3) `;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [` w:real^3 `;` t': real `]));
ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` rho_node1 FF w `]));
ANTS_TAC;
ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
MP_TAC Local_lemmas.AFF_GT_SAME_WITH_ENDS;
ANTS_TAC;
ASM_REWRITE_TAC[lunar; circular];
SIMP_TAC[];
STRIP_TAC THEN STRIP_TAC;
ASSUME_TAC2 (SPEC`w: real^3 ` (GEN`v: real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2));
SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w} = aff_gt {vec 0, w} { f (rho_node1 FF w) (t':real)} ` MP_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];
DISCH_THEN (ASSUME_TAC o SYM);



MP_TAC (ISPECL [` {w:real^3} `;` {vec 0, w:real^3} `;` {(f (rho_node1 FF w) (t': real)): real^3 } `]
 (GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS));
ANTS_TAC;
REWRITE_TAC[IN_INSERT; INSERT_SUBSET; EMPTY_SUBSET];
REWRITE_TAC[SET_RULE` A UNION {a} = a INSERT A `];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
ASSUME_TAC2 (SET_RULE` ~((w:real^3) = vec 0) ==> {vec 0, w} DIFF {w} = {vec 0} `);
UNDISCH_TAC` s = IMAGE (\v. (f:real^3 -> real -> real^3) v t') x `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_SIMP_TAC[];

SUBGOAL_THEN` {w, f (rho_node1 FF w) (t':real)} = s ` MP_TAC;
EXPAND_TAC "s";
EXPAND_TAC "x";
REWRITE_TAC[EXTENSION; IN_IMAGE];
GEN_TAC;
EQ_TAC;
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
STRIP_TAC;
EXISTS_TAC `w:real^3 `;
ASM_REWRITE_TAC[];

EXISTS_TAC` rho_node1 FF w `;
ASM_REWRITE_TAC[];
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
STRIP_TAC;
DISJ1_TAC;
ASM_REWRITE_TAC[];
DISJ2_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[];



ASM_CASES_TAC` n'' = j - 1 `;
ASSUME_TAC2 (ARITH_RULE` ~( j = 0 ) ==> j - 1 + 1 = j`);
SUBGOAL_THEN` rho_node1 FF v' = v ` MP_TAC;
EXPAND_TAC "v'";
UNDISCH_TAC` n'' = j - 1 `;
SIMP_TAC[GSYM ITER; ADD1];
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n'':num `;
ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `];
ASM_REWRITE_TAC[];
STRIP_TAC;
DISJ2_TAC;
DOWN;
ASM_REWRITE_TAC[];
REWRITE_TAC[IN_INTER];
STRIP_TAC;







SUBGOAL_THEN` IMAGE (\v. f v t') x = { f (v':real^3) (t':real), v:real^3} ` MP_TAC;
REWRITE_TAC[EXTENSION];
GEN_TAC;
EQ_TAC;
EXPAND_TAC "x";
REWRITE_TAC[IN_IMAGE; IN_INSERT; NOT_IN_EMPTY];
STRIP_TAC;
ASM_REWRITE_TAC[];


ASM_REWRITE_TAC[];
DISJ2_TAC;

UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = (u': real^3) `;
DISCH_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];

EXPAND_TAC "x";
REWRITE_TAC[IN_IMAGE; IN_INSERT; NOT_IN_EMPTY];
STRIP_TAC;
EXISTS_TAC `v': real^3 `;
ASM_REWRITE_TAC[];
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[EQ_SYM_EQ];
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[];
STRIP_TAC;

FIRST_ASSUM (MP_TAC o (SPECL [` t': real`;` v': real^3 `]));
ANTS_TAC;
ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
STRIP_TAC;
MP_TAC (ISPECL [` {v:real^3 } `; `{ vec 0, v:real^3 } `;
` { (f: real^3 -> real -> real^3) v' t' } `] (GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS));
ANTS_TAC;
REWRITE_TAC[IN_INSERT; INSERT_SUBSET; EMPTY_SUBSET];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
ASSUME_TAC2 (
SET_RULE` ~((v:real^3) = vec 0 ) ==> {vec 0, v} DIFF {v} = {vec 0 } `);
ASM_REWRITE_TAC[SET_RULE` {a} UNION {b} = {a,b} `];

MP_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
ANTS_TAC;
ASM_REWRITE_TAC[lunar; circular];
STRIP_TAC;

ASSUME_TAC2 (
SPEC` w:real^3 ` (GEN` v:real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2));

MP_TAC (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS);
ANTS_TAC;
ASM_REWRITE_TAC[lunar; circular];

STRIP_TAC;
SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC;
ASM_REWRITE_TAC[lunar; circular];
ASSUME_TAC2 Local_lemmas.NOT_COLL_RHONODE_SND_POINT;
UNDISCH_TAC` v' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` ~ collinear {vec 0, v, v':real^3 } ` MP_TAC;
MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
EXISTS_TAC` rho_node1 FF w `;
ASM_REWRITE_TAC[];
STRIP_TAC;

STRIP_TAC;
UNDISCH_TAC` v' IN aff_gt {vec 0, v} {rho_node1 FF w} `;
UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
STRIP_TAC;
SUBGOAL_THEN` aff_gt {vec 0, v} {f v' (t':real)} = aff_gt {vec 0, v} {v': real^3}` ASSUME_TAC;
MATCH_MP_TAC (GSYM Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ);
ASM_REWRITE_TAC[];
UNDISCH_TAC` aff_gt {vec 0} {f v' t', v} SUBSET aff_gt {vec 0, v} {(f: real^3 -> real -> real^3) v' t'} `;
ASM_REWRITE_TAC[];



SUBGOAL_THEN` lunar (v, (w:real^3)) V E` ASSUME_TAC;
ASM_REWRITE_TAC[lunar; circular];

SUBGOAL_THEN` v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} /\
rho_node1 FF v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
EXPAND_TAC "v'";
REWRITE_TAC[IN_ELIM_THM];
CONJ_TAC;
EXISTS_TAC`n'': num `;
ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `];
EXISTS_TAC` n'' + 1 `;
REWRITE_TAC[GSYM ITER; ADD1; ARITH_RULE` 0 < a + 1 `];
MATCH_MP_TAC (ARITH_RULE` n'' < j  /\ ~(n'' = j - 1)
==> n'' + 1 < j `);
ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[];
UNDISCH_TAC` aff_gt {vec 0, v} {u: real^3} =
      {y | ?t1 t2 t3.
               &0 < t3 /\
               t1 + t2 + t3 = &1 /\
               y = t1 % vec 0 + t2 % v + t3 % u} `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[IN_INTER];
STRIP_TAC;
DISJ2_TAC;
EXPAND_TAC "x";
REWRITE_TAC[IMAGE_CLAUSES];

ASSUME_TAC2 (
SPEC` w:real^3 ` (GEN` v: real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2));
SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w } = aff_gt { vec 0, w} {v'} ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w } = aff_gt { vec 0, w} {rho_node1 FF v'} ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];
DOWN;
DOWN;
ASSUME_TAC2 (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS);
ASSUME_TAC2 Local_lemmas.NOT_COLL_RHONODE_SND_POINT;
UNDISCH_TAC` v' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF w} =  aff_gt {vec 0, v} {v'} ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];


SUBGOAL_THEN` f (v':real^3) (t': real) IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
SUBGOAL_THEN` f (rho_node1 FF v') (t': real) IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` rho_node1 FF v' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
DOWN;
ASM_REWRITE_TAC[];
STRIP_TAC;
UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_SIMP_TAC[];
STRIP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
REPEAT STRIP_TAC;

ASSUME_TAC2 (
let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO in
ISPECL [` rho_node1 FF w` ;` vec 0: real^3 `;` w:real^3 `;
` (f:real^3 -> real -> real^3) v' t' `] tt);
ASSUME_TAC2 (
let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO in
ISPECL [` rho_node1 FF w` ;` vec 0: real^3 `;` w:real^3 `;
` (f:real^3 -> real -> real^3) (rho_node1 FF v') t' `] tt);
DOWN THEN DOWN;
NHANH Fan.th3b1;
PHA;
NHANH (SET_RULE` ~( a = x ) /\ t /\ ~( a = y ) ==> DISJOINT {a} {x,y} `);
STRIP_TAC;
UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `;
NHANH Fan.th3a;
STRIP_TAC;
MATCH_MP_TAC TOW_POINTS_IN_IMP_AFF_GT_SUBSET;
ASM_REWRITE_TAC[];
UNDISCH_TAC` (f: real^3 -> real -> real^3) v' t' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
UNDISCH_TAC` (f: real^3 -> real -> real^3) (rho_node1 FF v') t' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
ASM_REWRITE_TAC[];
SIMP_TAC[];

ASM_CASES_TAC` n'' = (j:num) ` ;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN THEN DOWN;
ASM_REWRITE_TAC[];
EXPAND_TAC "x";
REWRITE_TAC[IMAGE_CLAUSES];
DISCH_THEN (SUBST_ALL_TAC o SYM);
STRIP_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) v t' = v ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[];


MP_TAC (
let tt = GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS in
ISPECL [` {v:real^3 } `; `{vec 0, v:real^3} ` ;` { (f: real^3 -> real -> real^3) (rho_node1 FF v) t' }` ] tt);
ANTS_TAC;
REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v: real^3 `));
ASSUME_TAC2 (SET_RULE` ~( v = vec 0) ==> {vec 0, v} DIFF {v} = {vec 0: real^3 }`);
ASM_REWRITE_TAC[SET_RULE` {a} UNION {b} = {b,a} `];
FIRST_ASSUM (MP_TAC o (ISPECL [` t': real `;` rho_node1 FF v `]));
ANTS_TAC;
ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;

ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
STRIP_TAC;
ASSUME_TAC2 (
let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in
ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` (f:real^3 -> real -> real^3) (rho_node1 FF v) t' `] tt);
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[];
SIMP_TAC[];



ASM_CASES_TAC` n'' = CARD (V: real^3 -> bool) - 1 `;
SUBGOAL_THEN` rho_node1 FF v' = w ` ASSUME_TAC;
EXPAND_TAC "v'";
DOWN THEN SIMP_TAC[];
STRIP_TAC;
REWRITE_TAC[GSYM ITER; ADD1];
ASSUME_TAC2 (ARITH_RULE` n'' < CARD (V:real^3 -> bool) ==> CARD V - 1 + 1 = CARD V `);
ASM_REWRITE_TAC[];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
ASM_REWRITE_TAC[];






ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
UNDISCH_TAC` ITER n'' (rho_node1 FF) w = v' `;
ASM_REWRITE_TAC[];
STRIP_TAC;
MP_TAC (GSYM (
SPECL [` w:real^3 `;` v:real^3 `] (GENL [` v: real^3 `;` w:real^3 `]
 Local_lemmas.AFF_IVS_RHO_NODE_EQQ)));
ANTS_TAC;
ASM_REWRITE_TAC[Local_lemmas.LUNAR_COMM; lunar; circular; INSERT_SUBSET; EMPTY_SUBSET];
UNDISCH_TAC` collinear {vec 0, v, w:real^3} `;
SIMP_TAC[INSERT_COMM];



STRIP_TAC;
EXPAND_TAC "x";
ASM_REWRITE_TAC[IMAGE_CLAUSES];
SUBGOAL_THEN` (f:real^3 -> real -> real^3 ) w t' = w ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` v': real^3 `]));
ANTS_TAC;
ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
EXPAND_TAC "v'";
ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
ASM_REWRITE_TAC[];
SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC;
ASM_REWRITE_TAC[lunar; circular];
MP_TAC Local_lemmas.IVS_RNODE_IN_AFF_V;

ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC THEN STRIP_TAC;
MP_TAC (
let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in
ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v: real^3 `;` v': real^3 `] tt);
ANTS_TAC;


UNDISCH_TAC ` ivs_rho_node1 FF w IN aff_gt {vec 0, v} {rho_node1 FF v} ` ;
ASM_REWRITE_TAC[];
DISCH_THEN (SUBST_ALL_TAC o SYM);
DOWN;
ASM_REWRITE_TAC[];
UNDISCH_TAC ` aff_gt {vec 0, v} {u: real^3} =
      {y | ?t1 t2 t3.
               &0 < t3 /\
               t1 + t2 + t3 = &1 /\
               y = t1 % vec 0 + t2 % v + t3 % u}`;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
SUBGOAL_THEN` aff_gt {vec 0, v} {uh: real^3} = aff_gt {vec 0, w} {ivs_rho_node1 FF w} ` MP_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[];

ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas.LOFA_IMP_NOT_COLL_IVS);
REPEAT STRIP_TAC;
SUBGOAL_THEN` aff_gt {vec 0, w} {ivs_rho_node1 FF w} = aff_gt {vec 0, w} {(f: real^3 -> real -> real^3) v' t' } ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
REPLICATE_TAC 3 DOWN THEN PHA;

SIMP_TAC[];
FIRST_X_ASSUM SUBST1_TAC;

DISJ1_TAC;
MP_TAC (
let tt = GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS in
ISPECL [` {w:real^3 } `;` {vec 0, w:real^3} `; `{(f: real^3 -> real -> real^3) v' t' } `] tt);
ANTS_TAC;
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
DOWN;
SIMP_TAC[SET_RULE` ~(w = vec 0) ==> {vec 0, w} DIFF {w} = {vec 0 } `; SET_RULE` {a} UNION {b} = {a,b} `];

SUBGOAL_THEN` x SUBSET {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
EXPAND_TAC "x";
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM];
ABBREV_TAC `i' = n'' - (j:num ) `;
ASSUME_TAC2 (ARITH_RULE` ~( n'' < j) ==> (n'' - j) + j = (n'': num) `);
SUBGOAL_THEN` ITER i' (rho_node1 FF) v = v' ` ASSUME_TAC;
EXPAND_TAC "v";
REWRITE_TAC[ITER_ADD];
EXPAND_TAC "i'";
FIRST_ASSUM SUBST1_TAC;
ASM_REWRITE_TAC[];
CONJ_TAC;
EXISTS_TAC` i': num `;
ASM_REWRITE_TAC[];
CONJ_TAC;
EXPAND_TAC "i'";
UNDISCH_TAC` ~(n'' < j:num) `;
UNDISCH_TAC` ~(n'' = j:num) `;
ARITH_TAC;

EXPAND_TAC "i'";
UNDISCH_TAC` ~( n'' < j: num) `;
SIMP_TAC[ARITH_RULE`~( n'' < j) ==> (n'' - j < i <=> n'' < i + (j:num))`];
ASM_REWRITE_TAC[];

EXISTS_TAC` i' + 1 `;
ASM_REWRITE_TAC[GSYM ADD1; ITER; ARITH_RULE` 0 < SUC a `];


EXPAND_TAC "i'";
UNDISCH_TAC` ~( n'' < j: num) `;
SIMP_TAC[ARITH_RULE`~( n'' < j) ==> (SUC (n'' - j) < i <=> n'' < (i + (j:num)) - 1 )`];
ASM_REWRITE_TAC[];
STRIP_TAC;
MATCH_MP_TAC (ARITH_RULE` n < x /\ ~( n = x - 1) ==> n < x - 1 `);
ASM_REWRITE_TAC[];

UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
EXPAND_TAC "x";
REWRITE_TAC[IMAGE_CLAUSES; INSERT_SUBSET; EMPTY_SUBSET; IN_INTER];
STRIP_TAC;
ASSUME_TAC2 (
let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in
ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` v': real^3 `] tt);
ASSUME_TAC2 (
let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in
ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` rho_node1 FF v'`] tt);
DOWN THEN DOWN;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);
FIRST_ASSUM (MP_TAC o (SPECL [` t':real `;` v': real^3 `]));
ANTS_TAC;
ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [` t':real `;` rho_node1 FF v' `]));
ANTS_TAC;
ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
STRIP_TAC;

DOWN THEN DOWN;
ASM_REWRITE_TAC[];
STRIP_TAC;
UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
NHANH Fan.th3a;

NHANH Fan.th3b1;


STRIP_TAC;
UNDISCH_TAC` (f: real^3 -> real -> real^3) v' t' IN aff_gt {vec 0, v} {rho_node1 FF v} `;
UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
NHANH Fan.th3b1;
STRIP_TAC;

DISJ1_TAC;
MATCH_MP_TAC TOW_POINTS_IN_IMP_AFF_GT_SUBSET;
ASM_REWRITE_TAC[SET_RULE` DISJOINT {a} {x,y} <=> ~( a = x ) /\ ~( a = y) `];

STRIP_TAC;

SUBGOAL_THEN` !t. abs t < d /\ t IN real_interval (a,b)
          ==> (!s u. s IN IMAGE (IMAGE (\v. f v t)) E /\ 
u IN IMAGE (\v. (f:real^3 -> real -> real^3) v t) V ==>
                          (aff_gt {vec 0} s INTER aff_lt {vec 0} {u} =
                            {})) ` ASSUME_TAC;

FIRST_ASSUM NHANH;
GEN_TAC THEN STRIP_TAC;
FIRST_ASSUM NHANH;
GEN_TAC THEN GEN_TAC;
ABBREV_TAC` vw = (aff_gt {vec 0} s SUBSET aff_gt {vec 0, v} {rho_node1 FF v} \/
       aff_gt {vec 0} s SUBSET aff_gt {vec 0, w} {rho_node1 FF w})`;

STRIP_TAC;
DOWN;
REWRITE_TAC[IN_IMAGE];
STRIP_TAC;


FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` x: real^3 `]));
ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;

ASSUME_TAC2 Local_lemmas1.LOCAL_RHO_NODE_PAIR_E;
DOWN;
SUBGOAL_THEN` FAN (vec 0: real^3,V,E)` MP_TAC;
UNDISCH_TAC` local_fan (V: real^3 -> bool,E,FF) `;
SIMP_TAC[local_fan];
LET_TAC;
SIMP_TAC[];
PHA;
NHANH Topology.disjoint_fan3;
STRIP_TAC;

ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas1.LOCAL_RHO_NODE_PAIR_E);
DOWN;
SUBGOAL_THEN` FAN (vec 0: real^3,V,E)` MP_TAC;
UNDISCH_TAC` local_fan (V: real^3 -> bool,E,FF) `;
SIMP_TAC[local_fan];
LET_TAC;
SIMP_TAC[];
PHA;
NHANH Topology.disjoint_fan3;
STRIP_TAC;
SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC;
ASM_REWRITE_TAC[lunar; circular];
ASSUME_TAC2 Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
DOWN THEN STRIP_TAC;
UNDISCH_TAC` vec 0 IN conv0 {v, w:real^3} `;
NHANH IN_CONV0_IMP_AFF_EQ1;
STRIP_TAC;
ASM_CASES_TAC ` x = v:real^3 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) v t' = v ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[];
SIMP_TAC[];
STRIP_TAC;

ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_ASSUM (ASSUME_TAC2 o SPEC_ALL);
DOWN;
REWRITE_TAC[SET_RULE` ~( a = b) <=> DISJOINT {b} {a} `];
NHANH AFF_LT_SUBSET_AFF11;
UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `;
UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `;
UNDISCH_TAC` aff {vec 0, v} INTER aff_gt {vec 0, v} {rho_node1 FF v} = {} `;
UNDISCH_TAC` vw: bool `;
EXPAND_TAC "vw";
DISCH_TAC;
PHA THEN STRIP_TAC;
MATCH_MP_TAC (SET_RULE`!A. a SUBSET A /\ x INTER A = {} ==> x INTER a = {} `);

EXISTS_TAC` aff {vec 0, v:real^3} `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` aff_gt {vec 0} s SUBSET aff_gt {vec 0, v} {rho_node1 FF v} \/
      aff_gt {vec 0} s SUBSET aff_gt {vec 0, w} {rho_node1 FF w} `;
STRIP_TAC;
MATCH_MP_TAC (SET_RULE`!A. a SUBSET A /\ x INTER A = {} ==> a INTER x = {} `);

EXISTS_TAC` aff_gt {vec 0, v} {rho_node1 FF v} `;
UNDISCH_TAC` aff_gt {vec 0, v} {u:real^3} =
      {y | ?t1 t2 t3.
               &0 < t3 /\
               t1 + t2 + t3 = &1 /\
               y = t1 % vec 0 + t2 % v + t3 % u} `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` aff_gt {vec 0, v} {u} = aff_gt {vec 0, v} {uh: real^3} `;
DISCH_THEN (ASSUME_TAC o SYM);


ASM_REWRITE_TAC[];
UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
DOWN;
UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `;
CONV_TAC SET_RULE;


ASM_CASES_TAC` x = (w:real^3) `;
FIRST_X_ASSUM SUBST_ALL_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) w t' = w ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[];
SIMP_TAC[];
STRIP_TAC;
UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w: real^3} `;
UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `;
UNDISCH_TAC` aff {vec 0, v} INTER aff_gt {vec 0, v} {rho_node1 FF v} = {} `;
ASSUME_TAC2 (Local_lemmas.LOFA_IMP_V_DIFF);
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC ` w:real^3 `));
DOWN;
NHANH (SET_RULE` ~( a = b) ==> DISJOINT {b} {a} `);
NHANH AFF_LT_SUBSET_AFF11;
STRIP_TAC;
DOWN;
UNDISCH_TAC` vw: bool `;
EXPAND_TAC "vw";
CONV_TAC SET_RULE;


ASSUME_TAC2 LUNAR_IMP_IN_TWO_HAFLS_PLANE;
FIRST_X_ASSUM (MP_TAC o (SPEC` x: real^3 `));
PHA;
ANTS_TAC;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (GSYM Local_lemmas.AFF_IVS_RHO_NODE_EQQ);
FIRST_ASSUM SUBST1_TAC;
DISCH_TAC;
UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `;
DISCH_THEN (ASSUME_TAC o SYM);
ASSUME_TAC2 (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS);
UNDISCH_TAC` x IN aff_gt {vec 0, v} {rho_node1 FF v} \/
      x IN aff_gt {vec 0, w} {rho_node1 FF w} `;
STRIP_TAC;
UNDISCH_TAC` vw: bool `;
EXPAND_TAC "vw";
STRIP_TAC;
UNDISCH_TAC` x IN aff_gt {vec 0, v} {rho_node1 FF v} ` ;
UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC o SYM);
FIRST_ASSUM (MP_TAC o (SPECL [` t': real`;` x: real^3 `]));
ANTS_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM SUBST1_TAC;
STRIP_TAC;
MATCH_MP_TAC (SET_RULE` ! s. a SUBSET s /\ s INTER b = {} ==> a INTER b = {} `);
EXISTS_TAC` aff_gt {vec 0, v} {rho_node1 FF v} `;
ASM_REWRITE_TAC[];
MATCH_MP_TAC COLL_IN_AFF_GT_INTER_EMPTY;
ASM_REWRITE_TAC[];

ASM_CASES_TAC` aff_gt {vec 0} s INTER aff_lt {vec 0} {u': real^3} = {} `;
FIRST_X_ASSUM ACCEPT_TAC;
MP_TAC (ISPECL [` s: real^3 -> bool `; `u': real^3 `; `vec 0: real^3 `;
 `v:real^3 `; `rho_node1 FF v `; ` ivs_rho_node1 FF v `]
(GEN_ALL AZIM_PI_LEMMA));
ANTS_TAC;
ASM_REWRITE_TAC[];
DOWN THEN DOWN;
ASM_SIMP_TAC[];
STRIP_TAC THEN STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
ASM_REWRITE_TAC[];
SUBGOAL_THEN ` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {x} ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[];
UNDISCH_TAC` interior_angle1 (vec 0) FF v < pi `;
ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS;
UNDISCH_TAC` interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w `;
ASM_SIMP_TAC[];
STRIP_TAC;
REAL_ARITH_TAC;

UNDISCH_TAC` vw: bool `;
EXPAND_TAC "vw";
STRIP_TAC;

ASM_CASES_TAC` aff_gt {vec 0} s INTER aff_lt {vec 0} {u': real^3} = {} `;
FIRST_X_ASSUM ACCEPT_TAC;

MP_TAC (
let tt = GEN_ALL AZIM_PI_LEMMA in
ISPECL [` s: real^3 -> bool `; `u': real^3 `;` vec 0: real^3 `;` w: real^3 `;
 ` rho_node1 FF w `;` ivs_rho_node1 FF w `] tt);
ANTS_TAC;
ASM_REWRITE_TAC[];


SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF v} =
           aff_gt {vec 0, w} {ivs_rho_node1 FF w} ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ;
ASM_REWRITE_TAC[Local_lemmas.LUNAR_COMM];
FIRST_X_ASSUM (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];


ASSUME_TAC2 Local_lemmas.AFF_GT_SAME_WITH_ENDS;
UNDISCH_TAC` x IN aff_gt {vec 0, w} {rho_node1 FF w} `;
FIRST_X_ASSUM SUBST1_TAC;
UNDISCH_TAC` aff_gt {vec 0, v} {ivs_rho_node1 FF v} =
      aff_gt {vec 0, w} {rho_node1 FF w} `;
DISCH_THEN (SUBST1_TAC o SYM );
ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas.LOFA_IMP_NOT_COLL_IVS);
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` aff_gt {vec 0, v} {ivs_rho_node1 FF v} = aff_gt {vec 0, v} {x} ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[];
MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
ASM_REWRITE_TAC[];

UNDISCH_TAC` interior_angle1 (vec 0) FF v < pi `;
ASM_REWRITE_TAC[];
ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w: real^ 3 `));
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
MATCH_MP_TAC (SET_RULE` ! A. a SUBSET A /\ A INTER b = {} ==> a INTER b = {} `);
EXISTS_TAC` aff_gt {vec 0, w} {rho_node1 FF w} `;
CONJ_TAC;
ASM_REWRITE_TAC[];
MATCH_MP_TAC COLL_IN_AFF_GT_INTER_EMPTY;
CONJ_TAC;
ASM_REWRITE_TAC[];
MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
ASM_REWRITE_TAC[];
UNDISCH_TAC` aff_gt {vec 0, w} {rho_node1 FF w} = aff_gt {vec 0, v} {rho_node1 FF w}`;
ASSUME_TAC2 Local_lemmas.AFF_IVS_RHO_NODE_EQQ;

FIRST_X_ASSUM SUBST1_TAC;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];

UNDISCH_TAC ` x IN aff_gt {vec 0, w} {rho_node1 FF w} `;
UNDISCH_TAC` aff_gt {vec 0, v} {ivs_rho_node1 FF v} =
      aff_gt {vec 0, w} {rho_node1 FF w} `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
DOWN;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
SIMP_TAC[];
ASM_REWRITE_TAC[];





EXPAND_TAC "CONCL";
ABBREV_TAC` e1 = min ( -- a) b `;
EXISTS_TAC` min e1 d `;

CONJ_TAC;
EXPAND_TAC "e1";
REWRITE_TAC[REAL_LT_MIN];
ASM_REWRITE_TAC[REAL_ARITH` &0 < -- a <=> a < &0 `];
GEN_TAC;

REWRITE_TAC[REAL_BOUNDS_LT];
EXPAND_TAC "e1";
REWRITE_TAC[REAL_LT_MIN];
STRIP_TAC;
CONJ_TAC;
REWRITE_TAC[MESON[] `
~(?v w u. P v w u /\ Q v w u /\ ~ R v w u ) <=>
(! v w u. P v w u /\ Q v w u ==> R v w u ) `];
REPEAT GEN_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` t': real `));
ANTS_TAC;
ASM_REWRITE_TAC[real_interval; IN_ELIM_THM];
DOWN THEN DOWN THEN DOWN;
REAL_ARITH_TAC;


SIMP_TAC[];


CONJ_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
DOWN THEN DOWN THEN DOWN;
REWRITE_TAC[real_interval; IN_ELIM_THM];
REAL_ARITH_TAC;
ASM_REWRITE_TAC[]]);;



let LOCAL_FAN_SET_E = 
prove_by_refinement(` local_fan (V,E,FF) ==> {{v, rho_node1 FF v} | v IN V } = E `,

[REWRITE_TAC[EXTENSION; IN_ELIM_THM];
STRIP_TAC;
GEN_TAC;
EQ_TAC;
STRIP_TAC;
DOWN;
SIMP_TAC[GSYM EXTENSION];
STRIP_TAC;
MATCH_MP_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E;
ASM_REWRITE_TAC[];
REWRITE_TAC[GSYM EXTENSION];
DOWN THEN PHA;
NHANH EDGE_IN_LOCAL_FAN_DET_RHO_NODE;
SIMP_TAC[EQ_SYM_EQ]]);;




let LOCAL_FAN_FACE_FF = 
prove_by_refinement(` local_fan (V,E,FF) ==> { v, rho_node1 FF v | v IN V } = FF `,

[REWRITE_TAC[EXTENSION; IN_ELIM_THM];
STRIP_TAC;
GEN_TAC;
EQ_TAC;
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS;
DOWN THEN STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN PHA THEN STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x: real^3 # real^3 `));
EXISTS_TAC` FST (x: real^3 # real^3 ) `;
CONJ_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_IN_V2;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM ACCEPT_TAC]);;





let ORD_PAIRS_INJ_IMAGE = 
prove_by_refinement(` (! s. s IN E ==> INJ f s (IMAGE f s )) ==>
 ord_pairs (IMAGE (\s. IMAGE f s) E) = IMAGE (\ (x:real^N,y). (f: real^N -> real^M) x, f y) (ord_pairs E ) `,

[REWRITE_TAC[EXTENSION];
STRIP_TAC;
GEN_TAC THEN EQ_TAC;
REWRITE_TAC[ord_pairs; IN_ELIM_THM; IN_IMAGE];
NHANH_PAT `\x. x ==> y ` (SET_RULE` {a,b} = S ==> a IN S /\ b IN S `);
REWRITE_TAC[IN_IMAGE];
STRIP_TAC;
EXISTS_TAC` (x'': real^N, x''': real^N) `;
ASM_REWRITE_TAC[];

SUBGOAL_THEN` {x'', x''': real^N} = x' ` MP_TAC;
ASM_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; INSERT_SUBSET; EMPTY_SUBSET];
DOWN THEN DOWN;
FIRST_X_ASSUM NHANH;
REWRITE_TAC[SUBSET; INJ];
STRIP_TAC;
REPEAT STRIP_TAC;
UNDISCH_TAC` !x. (x:real^N) IN x' ==> (f x):real^M IN IMAGE f x' `;
DISCH_THEN (ASSUME_TAC2 o (SPEC` x'''': real^N `));
DOWN_TAC;
CONV_TAC SET_RULE;
DOWN THEN DOWN;
MESON_TAC[];


REWRITE_TAC[IN_IMAGE; ord_pairs; IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` (f: real^N -> real^M ) a `;
EXISTS_TAC` (f: real^N -> real^M ) b `;
ASM_REWRITE_TAC[];
EXISTS_TAC` {a, b: real^N } `;
ASM_REWRITE_TAC[IMAGE_CLAUSES]]);;




let SET2_DETER =
prove(` s = {x,y} /\ a IN s /\ b IN s /\ ~( a = b) ==> s = {a, b} `,

STRIP_TAC THEN 
REPLICATE_TAC 3 DOWN THEN PHA THEN 
ASM_REWRITE_TAC[] THEN 
CONV_TAC SET_RULE);;


let INSERT_UNION_CLAUSES =
prove(` x INSERT S UNION U = S UNION x INSERT U /\ {} UNION U = U `,

REWRITE_TAC[Local_lemmas.INSERT_UNION2; UNION_EMPTY]);;


let INJ_IMP_BIJ_IMAGE = 
prove(` INJ f S S' ==> BIJ f S (IMAGE f S) `,

SIMP_TAC[BIJ; INJ; SURJ; FUN_IN_IMAGE] THEN 
STRIP_TAC THEN 
REWRITE_TAC[IN_IMAGE] THEN ASM_MESON_TAC[]);;




let BIJ_AND_MAP_COMM = 
prove_by_refinement(` local_fan (V,E,FF) /\
BIJ (f: real^3 -> real^3) V V' /\
IMAGE (\s. IMAGE f s) E = E' /\
FAN (vec 0, V', E') /\ 
(\(x,y). f x, f y ) = ff
==>  BIJ ff ( darts_of_hyp E V) (darts_of_hyp E' V') /\
     (!x. x IN  darts_of_hyp E V
          ==> ff_of_hyp (vec 0,V',E') (ff x) = ff (ff_of_hyp (vec 0,V,E) x))

`,


[REWRITE_TAC[hyp_iso; local_fan];
LET_TAC;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC;
REWRITE_TAC[local_fan];
LET_TAC;
ASM_REWRITE_TAC[];
DOWN;
ASM_SIMP_TAC[];
STRIP_TAC;
CONJ_TAC;
EXISTS_TAC` (x: real^3 # real^3) `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `;
DISCH_THEN SUBST_ALL_TAC;
ASM_SIMP_TAC[];
UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ;
ASM_SIMP_TAC[];

ASSUME_TAC2 LOCAL_FAN_SET_E;
ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF;
ASSUME_TAC2 LOCAL_FAN_FACE_FF;
SUBST_ALL_TAC (
MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `);
ASM_REWRITE_TAC[];


SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC;
EXPAND_TAC "E'";
REWRITE_TAC[EXTENSION];
GEN_TAC;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM; IN_IMAGE];
EQ_TAC;
STRIP_TAC;
EXISTS_TAC` {v, rho_node1 FF v} `;
REWRITE_TAC[IMAGE_CLAUSES];
ASM_REWRITE_TAC[];
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];

STRIP_TAC;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[IMAGE_CLAUSES];
UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `;
PAT_REWRITE_TAC `\x. x ==> y ` [BIJ];
NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1;
STRIP_TAC;

SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC;
REWRITE_TAC[self_pairs];
EXPAND_TAC "V'";
EXPAND_TAC "E'";
REWRITE_TAC[IN_IMAGE];


MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `);
GEN_TAC;
STRIP_TAC;
DOWN;
PHA;
REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM];
EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `;
EXISTS_TAC` x': real^3 `;
ASM_REWRITE_TAC[];

STRIP_TAC;
SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs];

SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC;
REWRITE_TAC[INJ];
REPEAT STRIP_TAC;
REWRITE_TAC[IN_IMAGE];
EXISTS_TAC` x': real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` (s: real^3 -> bool) IN E `;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;

ASM_CASES_TAC` x' = (y:real^3) `;
DOWN THEN SIMP_TAC[];
REPLICATE_TAC 6 DOWN THEN PHA;
NHANH (
MESON[SET2_DETER]` x' IN s /\
 y IN s /\
 f x' = f y /\
 v IN V /\
 s = {v, rho_node1 FF v} /\
 ~(x' = y) ==> s = {x', y} `);
STRIP_TAC;
SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC;
DOWN;
ASM_REWRITE_TAC[IMAGE_CLAUSES];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC `v: real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `;
REWRITE_TAC[FAN; fan6];
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `));
DOWN;
UNDISCH_TAC` s = {x', y:real^3} `;
SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY];
ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2];
NHANH ORD_PAIRS_INJ_IMAGE;
REWRITE_TAC[GSYM ord_pairs];










SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC;
REWRITE_TAC[EXTENSION; IN_IMAGE];
GEN_TAC;
EQ_TAC;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `));
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
DOWN THEN DOWN;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
REPEAT STRIP_TAC;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
REPLICATE_TAC 4 DOWN THEN PHA;
CONV_TAC SET_RULE;




EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` {v, rho_node1 FF v }`;
ASM_REWRITE_TAC[];
EXPAND_TAC "E";
DOWN THEN DOWN;
CONV_TAC SET_RULE;
SIMP_TAC[];
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC;
REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM];
GEN_TAC;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `));
PHA;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `;
DISCH_THEN (SUBST1_TAC o SYM);
SIMP_TAC[darts_of_hyp; UNION_EMPTY];


(* ============ *)

ASM_SIMP_TAC[];
STRIP_TAC;
CONJ_TAC;
MATCH_MP_TAC (GEN_ALL INJ_IMP_BIJ_IMAGE);
EXISTS_TAC` IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (FF UNION {(v:real^3,w: real^3) | w,v IN FF} )`;
REWRITE_TAC[INJ; FUN_IN_IMAGE];
EXPAND_TAC "ff";


SUBGOAL_THEN` !x. x IN FF UNION {v,w | w,v IN FF} ==> (? a b. x = (a,b) /\ a IN V /\ b IN (V: real^3 -> bool)) ` MP_TAC;
REWRITE_TAC[IN_UNION];
REPEAT STRIP_TAC;
DOWN;
EXPAND_TAC "FF";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` v: real^3 `;
EXISTS_TAC` rho_node1 FF v `;
ASM_REWRITE_TAC[];
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
DOWN;
EXPAND_TAC "FF";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` rho_node1 FF v' `;
EXISTS_TAC` v': real^ 3 `;
DOWN THEN DOWN;
ASM_SIMP_TAC[PAIR_EQ];
REPEAT STRIP_TAC;
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
DISCH_THEN NHANH;
REPEAT STRIP_TAC;
DOWN;
ASM_REWRITE_TAC[];
EXPAND_TAC "ff";
REWRITE_TAC[PAIR_EQ];
UNDISCH_TAC` INJ (f:real^3 -> real^3) V V' `;
DOWN THEN DOWN;
UNDISCH_TAC` (a:real^3) IN V `;
UNDISCH_TAC` (b: real^3) IN V `;
REWRITE_TAC[INJ];
MESON_TAC[];

UNDISCH_TAC` darts_of_hyp E V = FF UNION {v:real^3,w | w,v IN FF} `;
DISCH_THEN (ASSUME_TAC2 o SYM);
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
SUBGOAL_THEN` (ff: real^3 # real^3 -> real^3 # real^3) x' IN darts_of_hyp E' V' ` MP_TAC;
ASM_REWRITE_TAC[];
MATCH_MP_TAC FUN_IN_IMAGE;
FIRST_ASSUM ACCEPT_TAC;
DOWN;
SIMP_TAC[Wrgcvdr_cizmrrh.ff_of_hyp2];
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (SUBST1_TAC o SYM);
REWRITE_TAC[];
REWRITE_TAC[IN_UNION];
STRIP_TAC THEN STRIP_TAC;
UNDISCH_TAC` (x': real^3 # real^3 ) IN FF `;
EXPAND_TAC "FF";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "ff";
REWRITE_TAC[PAIR_EQ];
SUBGOAL_THEN` rho_node1 FF v IN V ` MP_TAC;
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
UNDISCH_TAC` local_fan (V,E,FF) `;
PHA;
NHANH Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND;
ASSUME_TAC2 Local_lemmas.IVS_RHO_IDD;
ASM_SIMP_TAC[];
ONCE_REWRITE_TAC[INSERT_COMM];
REWRITE_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET];
STRIP_TAC;

SUBGOAL_THEN` EE ((f:real^3 -> real^3) (rho_node1 FF v)) E' = { f v, f (rho_node1 FF (rho_node1 FF v )) } ` MP_TAC;
REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET];
CONJ_TAC;
GEN_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
DOWN;
REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND];
STRIP_TAC;
UNDISCH_TAC` INJ (f: real^3 -> real ^3) V V' `;
REWRITE_TAC[INJ];
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`rho_node1 FF v `;` v': real^3 `]));
ASM_REWRITE_TAC[];
CONV_TAC SET_RULE;

UNDISCH_TAC` INJ (f: real^3 -> real ^3) V V' `;
REWRITE_TAC[INJ];
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [`rho_node1 FF v `;` rho_node1 FF v'`]));
ANTS_TAC;
ASM_REWRITE_TAC[];
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
ASSUME_TAC2 Polar_fan.RHO_NODE1_INJECTIVE;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL[` v: real^3 `;` v': real^3 `]));
ASM_SIMP_TAC[];
REWRITE_TAC[IN_INSERT];
GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM];
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC `v: real^3 `;
ASM_REWRITE_TAC[INSERT_COMM];
ASM_REWRITE_TAC[];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` rho_node1 FF v `;
ASM_REWRITE_TAC[];
SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET];



UNDISCH_TAC` (x': real^3 # real^3) IN {v,w | w,v IN FF} `;
EXPAND_TAC "FF";
REWRITE_TAC[IN_ELIM_THM; PAIR_EQ];
STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "ff";
REWRITE_TAC[PAIR_EQ];
ASSUME_TAC2 (
SPEC` v': real^3 ` (
GEN`v: real^3 ` Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND));
ASM_REWRITE_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET];
SUBGOAL_THEN` EE ((f:real^3 -> real^3) v') E'= { f (rho_node1 FF v'), f (ivs_rho_node1 FF v' )} ` MP_TAC;
REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET];

UNDISCH_TAC` INJ (f: real^3 -> real^3) V V' `;
REWRITE_TAC[INJ];
STRIP_TAC;


CONJ_TAC;
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM; Collect_geom.PAIR_EQ_EXPAND];
REPEAT STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL [` v': real^3 `;` v'': real^3 `]));
ASM_REWRITE_TAC[IN_INSERT];

FIRST_X_ASSUM (MP_TAC o (SPECL [` v': real^3 `;` rho_node1 FF v'' `]));
ANTS_TAC;
ASM_REWRITE_TAC[IN_INSERT];
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (
SPEC ` v'': real^3 ` (
GEN`v: real^3 ` Local_lemmas.IVS_RHO_IDD));
ASM_REWRITE_TAC[IN_INSERT];

REWRITE_TAC[IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` v': real^3 `;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` ivs_rho_node1 FF v' `;
ASM_REWRITE_TAC[];
ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V;
CONJ_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
ASSUME_TAC2 (
SPEC` v': real ^3 ` (
GEN`v: real^3 ` Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS ));
ASM_REWRITE_TAC[INSERT_COMM];
SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET]]);;



let NODE_EDGE_COMM_LEMMA = 
prove_by_refinement (` local_fan (V,E,FF) /\
     BIJ f V V' /\
     IMAGE (\s. IMAGE f s) E = E' /\
     FAN (vec 0,V',E') /\
     (\(x,y). f x,f y) = ff
     ==> 
         (!x. x IN darts_of_hyp E V
              ==> nn_of_hyp (vec 0,V',E') (ff x) =
                  ff (nn_of_hyp (vec 0,V,E) x)  /\
            ee_of_hyp (vec 0,V',E') (ff x) =
                  ff (ee_of_hyp (vec 0,V,E) x) ) `,




[REWRITE_TAC[hyp_iso; local_fan];
LET_TAC;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC;
REWRITE_TAC[local_fan];
LET_TAC;
ASM_REWRITE_TAC[];
DOWN;
ASM_SIMP_TAC[];
STRIP_TAC;
CONJ_TAC;
EXISTS_TAC` (x: real^3 # real^3) `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `;
DISCH_THEN SUBST_ALL_TAC;
ASM_SIMP_TAC[];
UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ;
ASM_SIMP_TAC[];

ASSUME_TAC2 LOCAL_FAN_SET_E;
ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF;
ASSUME_TAC2 LOCAL_FAN_FACE_FF;
SUBST_ALL_TAC (
MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `);
ASM_REWRITE_TAC[];


SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC;
EXPAND_TAC "E'";
REWRITE_TAC[EXTENSION];
GEN_TAC;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM; IN_IMAGE];
EQ_TAC;
STRIP_TAC;
EXISTS_TAC` {v, rho_node1 FF v} `;
REWRITE_TAC[IMAGE_CLAUSES];
ASM_REWRITE_TAC[];
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];

STRIP_TAC;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[IMAGE_CLAUSES];
UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `;
PAT_REWRITE_TAC `\x. x ==> y ` [BIJ];
NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1;
STRIP_TAC;

SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC;
REWRITE_TAC[self_pairs];
EXPAND_TAC "V'";
EXPAND_TAC "E'";
REWRITE_TAC[IN_IMAGE];


MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `);
GEN_TAC;
STRIP_TAC;
DOWN;
PHA;
REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM];
EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `;
EXISTS_TAC` x': real^3 `;
ASM_REWRITE_TAC[];

STRIP_TAC;
SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs];

SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC;
REWRITE_TAC[INJ];
REPEAT STRIP_TAC;
REWRITE_TAC[IN_IMAGE];
EXISTS_TAC` x': real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` (s: real^3 -> bool) IN E `;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;

ASM_CASES_TAC` x' = (y:real^3) `;
DOWN THEN SIMP_TAC[];
REPLICATE_TAC 6 DOWN THEN PHA;
NHANH (
MESON[SET2_DETER]` x' IN s /\
 y IN s /\
 f x' = f y /\
 v IN V /\
 s = {v, rho_node1 FF v} /\
 ~(x' = y) ==> s = {x', y} `);
STRIP_TAC;
SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC;
DOWN;
ASM_REWRITE_TAC[IMAGE_CLAUSES];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC `v: real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `;
REWRITE_TAC[FAN; fan6];
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `));
DOWN;
UNDISCH_TAC` s = {x', y:real^3} `;
SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY];
ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2];
NHANH ORD_PAIRS_INJ_IMAGE;
REWRITE_TAC[GSYM ord_pairs];










SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC;
REWRITE_TAC[EXTENSION; IN_IMAGE];
GEN_TAC;
EQ_TAC;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `));
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
DOWN THEN DOWN;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
REPEAT STRIP_TAC;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
REPLICATE_TAC 4 DOWN THEN PHA;
CONV_TAC SET_RULE;




EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` {v, rho_node1 FF v }`;
ASM_REWRITE_TAC[];
EXPAND_TAC "E";
DOWN THEN DOWN;
CONV_TAC SET_RULE;
SIMP_TAC[];
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC;
REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM];
GEN_TAC;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `));
PHA;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `;
DISCH_THEN (SUBST1_TAC o SYM);
SIMP_TAC[darts_of_hyp; UNION_EMPTY];

STRIP_TAC;
REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2];
UNDISCH_TAC` darts_of_hyp E V = FF UNION {v:real^3,w | w,v IN FF} `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_SIMP_TAC[];
SUBGOAL_THEN`(! x. x IN darts_of_hyp E (V:real^3 -> bool) ==> ((ff x): real^3 # real^3) IN darts_of_hyp E' V' )` MP_TAC;
ASM_REWRITE_TAC[FUN_IN_IMAGE];
STRIP_TAC;
FIRST_ASSUM NHANH;
ASM_SIMP_TAC[];

SUBGOAL_THEN` ! v. v IN V ==> ivs_rho_node1 FF (rho_node1 FF v) = v ` ASSUME_TAC;
GEN_TAC THEN STRIP_TAC;
MATCH_MP_TAC Local_lemmas.IVS_RHO_IDD;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ! v. v IN V ==> rho_node1 FF (ivs_rho_node1 FF v) = v ` ASSUME_TAC;
GEN_TAC THEN STRIP_TAC;
MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS;
ASM_REWRITE_TAC[];


SUBGOAL_THEN` !v . v IN V ==> rho_node1 FF v IN V ` ASSUME_TAC;
GEN_TAC THEN STRIP_TAC;
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_SIMP_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];


SUBGOAL_THEN` !v . v IN V ==> ivs_rho_node1 FF v IN V ` ASSUME_TAC;
MATCH_MP_TAC Polar_fan.IVS_RHO_NODE1_IN_V;
EXISTS_TAC` E: (real^3 -> bool) -> bool `;
ASM_REWRITE_TAC[];



UNDISCH_TAC` INJ (f: real^3 -> real^3) V V' `;
REWRITE_TAC[INJ];
STRIP_TAC;


SUBGOAL_THEN` !v. v IN V
          ==> EE v E = {rho_node1 FF v,  (ivs_rho_node1 FF v)} ` ASSUME_TAC;
REPEAT STRIP_TAC;
MATCH_MP_TAC Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND;
ASM_REWRITE_TAC[];





SUBGOAL_THEN`!v. v IN V ==> EE ((f:real^3 -> real^3) v ) E' = {f (rho_node1 FF v), f (ivs_rho_node1 FF v ) } ` ASSUME_TAC;
REPEAT STRIP_TAC;
REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
CONJ_TAC;
GEN_TAC THEN STRIP_TAC;
DOWN;
REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND];
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL [` v: real^3 `;` v': real^3 `]));
ASM_REWRITE_TAC[IN_INSERT];
FIRST_X_ASSUM (MP_TAC o (SPECL [` v: real^3 `;` rho_node1 FF v' `]));
ANTS_TAC;
ASM_REWRITE_TAC[IN_INSERT];
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
STRIP_TAC;

ASM_SIMP_TAC[IN_INSERT];
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
GEN_TAC THEN STRIP_TAC;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
EXISTS_TAC` ivs_rho_node1 FF v `;
ASM_SIMP_TAC[INSERT_COMM];

GEN_TAC THEN STRIP_TAC;
SUBGOAL_THEN` x' IN FF UNION {v:real^3,w | w,v IN FF} ` MP_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[IN_UNION];
STRIP_TAC;
DOWN;
EXPAND_TAC "FF";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "ff";
REWRITE_TAC[];

CONJ_TAC;
ASM_SIMP_TAC[PAIR_EQ];
REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET];

REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2];
UNDISCH_TAC` x' IN darts_of_hyp E (V: real^3 -> bool) `;
UNDISCH_TAC` (ff: real^3 # real^3 -> real^3 # real^3 ) x' IN IMAGE ff (darts_of_hyp E V) `;
ASM_REWRITE_TAC[];
EXPAND_TAC "ff";
SIMP_TAC[];

DOWN;
EXPAND_TAC "FF";
REWRITE_TAC[IN_ELIM_THM; PAIR_EQ];
STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "ff";
REWRITE_TAC[PAIR_EQ];
ASM_SIMP_TAC[];
ONCE_REWRITE_TAC[INSERT_COMM];
REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET];

REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2];
UNDISCH_TAC` x' IN darts_of_hyp E (V: real^3 -> bool) `;
UNDISCH_TAC` (ff: real^3 # real^3 -> real^3 # real^3 ) x' IN IMAGE ff (darts_of_hyp E V) `;
ASM_REWRITE_TAC[];
EXPAND_TAC "ff";
SIMP_TAC[]]);;





let HYP_ISO_LEMMAA = 
prove_by_refinement (` local_fan (V,E,FF) /\
     BIJ f V V' /\
     IMAGE (\s. IMAGE f s) E = E' /\
     FAN (vec 0,V',E') /\
     (\(x,y). f x,f y) = ff
==> hyp_iso ff (hypermap (HYP (vec 0, V, E)), hypermap (HYP (vec 0, V', E')))`,

[REWRITE_TAC[hyp_iso; local_fan];
LET_TAC;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC;
REWRITE_TAC[local_fan];
LET_TAC;
ASM_REWRITE_TAC[];
DOWN;
ASM_SIMP_TAC[];
STRIP_TAC;
CONJ_TAC;
EXISTS_TAC` (x: real^3 # real^3) `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `;
DISCH_THEN SUBST_ALL_TAC;
ASM_SIMP_TAC[];
UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ;
ASM_SIMP_TAC[];

ASSUME_TAC2 LOCAL_FAN_SET_E;
ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF;
ASSUME_TAC2 LOCAL_FAN_FACE_FF;
SUBST_ALL_TAC (
MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `);
ASM_REWRITE_TAC[];


SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC;
EXPAND_TAC "E'";
REWRITE_TAC[EXTENSION];
GEN_TAC;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM; IN_IMAGE];
EQ_TAC;
STRIP_TAC;
EXISTS_TAC` {v, rho_node1 FF v} `;
REWRITE_TAC[IMAGE_CLAUSES];
ASM_REWRITE_TAC[];
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];

STRIP_TAC;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[IMAGE_CLAUSES];
UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `;
PAT_REWRITE_TAC `\x. x ==> y ` [BIJ];
NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1;
STRIP_TAC;

SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC;
REWRITE_TAC[self_pairs];
EXPAND_TAC "V'";
EXPAND_TAC "E'";
REWRITE_TAC[IN_IMAGE];


MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `);
GEN_TAC;
STRIP_TAC;
DOWN;
PHA;
REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM];
EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `;
EXISTS_TAC` x': real^3 `;
ASM_REWRITE_TAC[];

STRIP_TAC;
SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs];

SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC;
REWRITE_TAC[INJ];
REPEAT STRIP_TAC;
REWRITE_TAC[IN_IMAGE];
EXISTS_TAC` x': real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` (s: real^3 -> bool) IN E `;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;

ASM_CASES_TAC` x' = (y:real^3) `;
DOWN THEN SIMP_TAC[];
REPLICATE_TAC 6 DOWN THEN PHA;
NHANH (
MESON[SET2_DETER]` x' IN s /\
 y IN s /\
 f x' = f y /\
 v IN V /\
 s = {v, rho_node1 FF v} /\
 ~(x' = y) ==> s = {x', y} `);
STRIP_TAC;
SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC;
DOWN;
ASM_REWRITE_TAC[IMAGE_CLAUSES];
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC `v: real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `;
REWRITE_TAC[FAN; fan6];
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `));
DOWN;
UNDISCH_TAC` s = {x', y:real^3} `;
SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY];
ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2];
NHANH ORD_PAIRS_INJ_IMAGE;
REWRITE_TAC[GSYM ord_pairs];










SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC;
REWRITE_TAC[EXTENSION; IN_IMAGE];
GEN_TAC;
EQ_TAC;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `));
EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
DOWN THEN DOWN;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
REPEAT STRIP_TAC;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
REPLICATE_TAC 4 DOWN THEN PHA;
CONV_TAC SET_RULE;




EXPAND_TAC "E'";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` {v, rho_node1 FF v }`;
ASM_REWRITE_TAC[];
EXPAND_TAC "E";
DOWN THEN DOWN;
CONV_TAC SET_RULE;
SIMP_TAC[];
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC;
REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM];
GEN_TAC;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `));
PHA;
EXPAND_TAC "E";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `;
DISCH_THEN (SUBST1_TAC o SYM);
SIMP_TAC[darts_of_hyp; UNION_EMPTY];


MP_TAC BIJ_AND_MAP_COMM;
ANTS_TAC;
ASM_REWRITE_TAC[BIJ];

MP_TAC NODE_EDGE_COMM_LEMMA;
ANTS_TAC;
ASM_REWRITE_TAC[BIJ];
ASM_REWRITE_TAC[];
SIMP_TAC[];
REPEAT STRIP_TAC;
DOWN;
NHANH (ISPEC `ff: real^3 # real^3 -> real^3 # real^3 ` FUN_IN_IMAGE);
STRIP_TAC;
ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2];
UNDISCH_TAC` x' IN FF UNION {v,w | w:real^3,v IN FF} `;
REWRITE_TAC[IN_ELIM_THM];
SUBGOAL_THEN` x' IN FF UNION {v:real^3,w | w,v IN FF} ==> ? a b. x' = (a,b) ` MP_TAC;
EXPAND_TAC "FF";
REWRITE_TAC[IN_UNION; IN_ELIM_THM];
MESON_TAC[];
DISCH_THEN NHANH;
STRIP_TAC;
DOWN;
SIMP_TAC[];
EXPAND_TAC "ff";
SIMP_TAC[]]);;




let POWER_COMM = 
REWRITE_RULE[IN_UNIV] (SPEC` (:A) ` Hypermap_iso.power_comm);;

let ITER_COMM = 
REWRITE_RULE[Wrgcvdr_cizmrrh.POWER_TO_ITER] POWER_COMM;;




let IMAGE_FACE_F = 
prove_by_refinement(
` hyp_iso (f: A -> B) (H,HH) ==> ! x . x IN dart H ==> IMAGE f (face H x ) = face HH ( f x ) `,

[REWRITE_TAC[hyp_iso];
STRIP_TAC THEN GEN_TAC THEN STRIP_TAC;
REWRITE_TAC[EXTENSION; face; orbit_map; IN_ELIM_THM];
SUBGOAL_THEN`! x n. x IN dart H ==> (face_map HH POWER n) ((f:A -> B) x) = 
f  ((face_map H POWER n) (x)) ` ASSUME_TAC;
ONCE_REWRITE_TAC[EQ_SYM_EQ];
MATCH_MP_TAC (
REWRITE_RULE[TAUT` a ==> b ==> c <=> a /\ b ==> c `] Hypermap_iso.power_comm);
ASM_SIMP_TAC[Hypermap.lemma_dart_invariant];


ASM_SIMP_TAC[IN_IMAGE; IN_ELIM_THM];
MESON_TAC[]]);;




let COMM_BIJ_HAS_SAME_ORDS = 
prove_by_refinement(`BIJ f (:A) (:B) /\ 
 (! x. (f o h) x = (g o (f: A -> B)) x ) 
/\ has_orders h k
==> has_orders g k`,

[REWRITE_TAC[has_orders];
REPEAT STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` i: num `));
DOWN;
PHA;
REWRITE_TAC[FUN_EQ_THM];
GEN_TAC;
UNDISCH_TAC` BIJ f (:A) (:B) `;
REWRITE_TAC[BIJ; INJ];
STRIP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[IN_UNIV];
UNDISCH_TAC` !x. (f o h) x = (g o (f:A -> B)) x `;
REWRITE_TAC[o_THM];
NHANH ITER_COMM;
SIMP_TAC[];
STRIP_TAC;
ASM_REWRITE_TAC[I_THM];

DOWN_TAC;
REWRITE_TAC[o_THM];
NHANH ITER_COMM;
STRIP_TAC;
SIMP_TAC[FUN_EQ_THM];
UNDISCH_TAC` BIJ f (:A) (:B) `;
REWRITE_TAC[BIJ; INJ; SURJ];
STRIP_TAC;
GEN_TAC;
SUBGOAL_THEN` x IN (:B) ` MP_TAC;
REWRITE_TAC[IN_UNIV];
FIRST_X_ASSUM NHANH;
STRIP_TAC;
EXPAND_TAC "x";
UNDISCH_TAC` !x n. f (ITER n h x) = ITER n g ((f: A -> B) x) `;
ONCE_REWRITE_TAC[EQ_SYM_EQ];
SIMP_TAC[];
STRIP_TAC;
ASM_REWRITE_TAC[I_THM]]);;






let DIH2K_HYP_ISO_LEMMA = 
prove_by_refinement
(` BIJ f (:A) (:B) /\ 
FINITE (dart (H: (A) hypermap) ) /\ dih2k H k /\ hyp_iso (f: A -> B) (H, HH)
==> dih2k HH k `,

[NHANH IMAGE_FACE_F;
REWRITE_TAC[dih2k; hyp_iso];
STRIP_TAC;
CONJ_TAC;
SUBGOAL_THEN` CARD (dart (H: (A) hypermap )) = CARD (dart (HH:(B) hypermap)) ` MP_TAC;
MATCH_MP_TAC (Local_lemmas.BIJ_IMP_CARD_EQ);
ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[];
SIMP_TAC[];
CONJ_TAC;
GEN_TAC;
LET_TAC;
STRIP_TAC;
UNDISCH_TAC` BIJ (f: A -> B) (dart H) (dart HH) `;
NHANH Add_triangle.BIJ_IMAGE;
REWRITE_TAC[BIJ; SURJ];
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` x: B `));
DOWN THEN STRIP_TAC;


SUBGOAL_THEN` (let S = face  (H: (A) hypermap) y in dart H = S UNION IMAGE (node_map H) S) ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
LET_TAC;

SUBGOAL_THEN` IMAGE f (face H (y:A)) = face HH ((f: A -> B) (y:A)) ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;

ASM_REWRITE_TAC[];
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[GSYM IMAGE_o];
UNDISCH_TAC` (y:A) IN dart H ` ;
NHANH Hypermap.lemma_face_subset;
STRIP_TAC;

SUBGOAL_THEN` IMAGE (node_map HH o (f: A -> B)) S' = IMAGE (f o (node_map H )) S' ` ASSUME_TAC;
MATCH_MP_TAC Lvducxu.IDE_ON_S_IMP_SAME_IMAGE;
GEN_TAC THEN DOWN;
ASM_SIMP_TAC[SUBSET];
DISCH_THEN NHANH;
ASM_SIMP_TAC[o_THM];
ASM_REWRITE_TAC[];

REWRITE_TAC[IMAGE_o; GSYM IMAGE_UNION];
SIMP_TAC[];

SUBGOAL_THEN`!x. (x:A) IN dart H <=> ((f x): B) IN dart HH ` ASSUME_TAC;
UNDISCH_TAC` BIJ (f: A -> B) (dart H ) (dart HH ) ` ;
UNDISCH_TAC ` BIJ f (:A) (:B) ` ;
REWRITE_TAC[BIJ; INJ; SURJ];
STRIP_TAC THEN STRIP_TAC;
GEN_TAC THEN EQ_TAC;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM NHANH;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPECL [` y: A `;` x: A `]));
FIRST_X_ASSUM (MP_TAC o (SPECL [` y: A `;` x: A `]));
ANTS_TAC;
ASM_REWRITE_TAC[IN_UNIV];
ASM_SIMP_TAC[];
DISCH_THEN SUBST_ALL_TAC;
FIRST_ASSUM ACCEPT_TAC;

CONJ_TAC;
MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS);
EXISTS_TAC` f: A -> B `;
EXISTS_TAC` face_map (H: (A) hypermap)`;
ASM_REWRITE_TAC[];
GEN_TAC;
ASM_CASES_TAC` (x:A) IN dart H `;
ASM_SIMP_TAC[o_THM];

DOWN;
NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
ASM_REWRITE_TAC[];
NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
SIMP_TAC[o_THM];

CONJ_TAC;
MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS);
EXISTS_TAC` f: A -> B `;
EXISTS_TAC` edge_map (H: (A) hypermap)`;

ASM_REWRITE_TAC[];
GEN_TAC;
ASM_CASES_TAC` (x:A) IN dart H `;
ASM_SIMP_TAC[o_THM];

DOWN;
NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
ASM_REWRITE_TAC[];
NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
SIMP_TAC[o_THM];

MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS);
EXISTS_TAC` f: A -> B `;
EXISTS_TAC` node_map (H: (A) hypermap)`;

ASM_REWRITE_TAC[];
GEN_TAC;
ASM_CASES_TAC` (x:A) IN dart H `;
ASM_SIMP_TAC[o_THM];

DOWN;
NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
ASM_REWRITE_TAC[];
NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
SIMP_TAC[o_THM]]);;





let AUTOMAP_IMP_ALL_ITER_IN2 = 
MESON[IN; Trigonometry2.AUTOMAP_IMP_ALL_ITER_IN] `
p IN W /\ (!x. x IN W ==> f x IN W) ==> ITER N f p IN W `;;


let ITER_COMM_RESTRICTED = 
prove_by_refinement(` (!(x:A). x IN V ==> f x IN V') /\
 (!x. h x IN V <=> x IN V) /\
  (!(y:B). g y IN V' <=> y IN V') /\
(!x. x IN V ==> f (h x) = g (f x)) 
==> ! x. x IN V ==> f (ITER n h x) = ITER n g ( f x ) `,

[
STRIP_TAC;
SPEC_TAC (`n:num `,`n:num `);
INDUCT_TAC;
REWRITE_TAC[ITER];

GEN_TAC THEN STRIP_TAC;
REWRITE_TAC[ITER];
SUBGOAL_THEN` ITER n h (x:A) IN V ` ASSUME_TAC;
MATCH_MP_TAC AUTOMAP_IMP_ALL_ITER_IN2;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x:A `));
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` ITER n h (x:A) `));
ASM_REWRITE_TAC[]]);;


let HAS_THE_SAME_ORD_LEM = 
prove_by_refinement(` (! x. ~( x IN V ) ==> h x = x ) /\
(! y. ~( y IN V') ==> g y = y ) /\
BIJ (f: A -> B) V V' /\
(! x. (h x IN V) <=> x IN V ) /\
(! y. (g y IN V') <=> y IN V' ) /\
(!x. x IN V ==> (f (h  x )) = (g (f x ))) /\ has_orders h k
     ==> has_orders g k `,

[REWRITE_TAC[BIJ; INJ; SURJ; has_orders];
REPEAT STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` i:num `));
DOWN;
PHA;
REWRITE_TAC[FUN_EQ_THM];
GEN_TAC;
ASM_CASES_TAC` (x:A) IN V `;
UNDISCH_TAC` !x y. x IN V /\ y IN V /\ (f: A -> B) x = f y ==> x = y ` ;
DISCH_THEN MATCH_MP_TAC;
ASM_REWRITE_TAC[I_THM];
CONJ_TAC;
MATCH_MP_TAC AUTOMAP_IMP_ALL_ITER_IN2;
ASM_REWRITE_TAC[];
MP_TAC (SPEC `i:num ` (GEN `n:num ` ITER_COMM_RESTRICTED));
ANTS_TAC;
ASM_REWRITE_TAC[];
DISCH_THEN (ASSUME_TAC2 o (SPEC` x: A `));
ASM_REWRITE_TAC[I_THM];

REWRITE_TAC[I_THM];
MATCH_MP_TAC ITER_FIXPOINT;
DOWN;
ASM_REWRITE_TAC[];

REWRITE_TAC[FUN_EQ_THM; I_THM];
GEN_TAC;
ASM_CASES_TAC` x IN (V': B -> bool) `;


DOWN;
UNDISCH_TAC` !x. x IN V' ==> (?y. y IN V /\ (f: A -> B) y = x) `;
DISCH_THEN NHANH;
STRIP_TAC;

MP_TAC (let tt = GEN` n: num ` ITER_COMM_RESTRICTED in SPEC` k: num ` tt);
ANTS_TAC;
ASM_REWRITE_TAC[];
DISCH_THEN (ASSUME_TAC2 o (SPEC` y: A `));
DOWN;
ASM_REWRITE_TAC[I_THM];
MESON_TAC[];
MATCH_MP_TAC ITER_FIXPOINT;
ASM_SIMP_TAC[]]);;



let COMM_THEN_IMAGE_IMAGE_EQ = 
SET_RULE ` (! x. x IN S ==> f ( g x ) = h ( f x )) /\ A SUBSET S 
==> IMAGE f ( IMAGE g A ) = IMAGE h ( IMAGE f A ) `;;


let IN_DART_PRESERVED = 
prove(` (!x: A. face_map H x IN dart H <=> x IN dart H) /\
(!x: A. node_map H x IN dart H <=> x IN dart H) /\
(!x: A. edge_map H x IN dart H <=> x IN dart H)`,

MESON_TAC [Hypermap_iso.h_map_outside; Hypermap.lemma_dart_invariant]);;

let HYP_ISO_DIH2K_PRESERVED = 
prove_by_refinement
(`FINITE (dart H) /\ dih2k H k /\ hyp_iso (f: A -> B) (H,HH)
       ==> dih2k HH k `,

[NHANH Hypermap_iso.iso_components;
REWRITE_TAC[dih2k; hyp_iso];
STRIP_TAC;
CONJ_TAC;
ASSUME_TAC2 (
let tt = GEN_ALL Local_lemmas.BIJ_IMP_CARD_EQ in
ISPECL [` f: A -> B `;` dart (H: (A) hypermap) `;` dart (HH: (B) hypermap) `] tt);
DOWN;
ASM_SIMP_TAC[];

CONJ_TAC;
GEN_TAC THEN STRIP_TAC;
DOWN;
UNDISCH_TAC ` BIJ (f: A -> B) ( dart H ) ( dart HH ) `;
REWRITE_TAC[BIJ; SURJ];
STRIP_TAC;
FIRST_ASSUM NHANH;
STRIP_TAC;
LET_TAC;
SUBGOAL_THEN` (let S = face H (y:A) in dart H = S UNION IMAGE (node_map H) S) ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
LET_TAC;
SUBGOAL_THEN` node HH (f y) = IMAGE f (node H y) /\
              face HH (f y) = IMAGE f (face H y) /\
              edge HH ((f: A -> B) y) = IMAGE f (edge H y) ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
ASM_REWRITE_TAC[];

SIMP_TAC[];
PHA THEN STRIP_TAC;
SUBGOAL_THEN` IMAGE (f: A -> B) (IMAGE (node_map H) S') = IMAGE (node_map HH) (IMAGE f S') ` ASSUME_TAC;
MATCH_MP_TAC (GEN_ALL COMM_THEN_IMAGE_IMAGE_EQ);
EXISTS_TAC` dart (H: (A) hypermap ) `;
UNDISCH_TAC` !x. x IN dart H
          ==> edge_map HH ((f: A -> B) x) = f (edge_map H x) /\
              node_map HH (f x) = f (node_map H x) /\
              face_map HH (f x) = f (face_map H x) `;
SIMP_TAC[];
STRIP_TAC;
EXPAND_TAC "S'";
MATCH_MP_TAC Hypermap.lemma_face_subset;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (SUBST1_TAC o SYM);
REWRITE_TAC[GSYM IMAGE_UNION];
SUBGOAL_THEN` BIJ (f: A -> B) (dart H ) (dart HH ) ` MP_TAC;
ASM_REWRITE_TAC[BIJ; SURJ];
NHANH Add_triangle.BIJ_IMAGE;
SIMP_TAC[];
ASM_REWRITE_TAC[];

ASSUME_TAC Hypermap_iso.h_map_outside;

CONJ_TAC;
MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM);
EXISTS_TAC` dart (HH: (B) hypermap) `;
EXISTS_TAC` dart (H: (A) hypermap) `;
EXISTS_TAC` f: A -> B `;
EXISTS_TAC` face_map (H: (A) hypermap ) `;
ASM_REWRITE_TAC[];
DOWN THEN SIMP_TAC[];
DISCH_THEN NHANH;

NHANH (
ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside);
SIMP_TAC[IN_DART_PRESERVED];
ASM_SIMP_TAC[];


CONJ_TAC;
MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM);
EXISTS_TAC` dart (HH: (B) hypermap) `;
EXISTS_TAC` dart (H: (A) hypermap) `;
EXISTS_TAC` f: A -> B `;
EXISTS_TAC` edge_map (H: (A) hypermap ) `;
ASM_REWRITE_TAC[];
DOWN THEN SIMP_TAC[];
DISCH_THEN NHANH;

NHANH (
ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside);
SIMP_TAC[IN_DART_PRESERVED];
ASM_SIMP_TAC[];

MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM);
EXISTS_TAC` dart (HH: (B) hypermap) `;
EXISTS_TAC` dart (H: (A) hypermap) `;
EXISTS_TAC` f: A -> B `;
EXISTS_TAC` node_map (H: (A) hypermap ) `;
ASM_REWRITE_TAC[];
DOWN THEN SIMP_TAC[];
DISCH_THEN NHANH;

NHANH (
ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside);
SIMP_TAC[IN_DART_PRESERVED];
ASM_SIMP_TAC[]]);;





let CONT_ATREAL_INJ_PRESERVED = 
prove_by_refinement(
` FINITE V /\ (!v. v IN V  ==> (ff: real^N -> real -> real^M) v continuous atreal r) /\
INJ (\v. ff v r ) V (IMAGE (\v. ff v r ) V )
==> ? e. &0 < e /\ (! t. abs ( t - r) < e ==>
INJ (\v. ff v t ) V (IMAGE (\v. ff v t ) V )) `,

[REWRITE_TAC[INJ];
STRIP_TAC;
MP_TAC (SPEC_ALL Local_lemmas1.CONTINUOUS_ATREAL_INJ_PRESERVED);
ANTS_TAC;
ASM_REWRITE_TAC[];
ANTS_TAC;
ASM_REWRITE_TAC[];
DOWN;
MESON_TAC[];
STRIP_TAC;
EXISTS_TAC` d : real `;
ASM_REWRITE_TAC[];
GEN_TAC;
FIRST_X_ASSUM NHANH;
REWRITE_TAC[IN_IMAGE];
MESON_TAC[]]);;

let INJ_BIJ_IMAGE = 
prove(` INJ f S S' /\ A SUBSET S ==> BIJ f A (IMAGE f A) `,

REWRITE_TAC[BIJ; INJ; SURJ] THEN CONV_TAC SET_RULE);;




let XRECQNS_UPDATE = 
prove_by_refinement(`  deformation f V (a,b) /\ local_fan (V,E,FF) 
           ==> (?e. &0 < e /\
                    (!t. abs t < e
                         ==> local_fan (IMAGE (\v. f v t) V,
IMAGE (\s. IMAGE (\v. f v t) s ) E , 
IMAGE (\(u,v). (f u t, f v t )) FF) )) `,


[NHANH_PAT `\x. x ==> y ` Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
STRIP_TAC;
ASSUME_TAC2 Deformation.XRECQNS;
DOWN THEN PHA;
REWRITE_TAC[REAL_BOUNDS_LT];
STRIP_TAC;
DOWN_TAC;
REWRITE_TAC[deformation];
STRIP_TAC;
UNDISCH_TAC` FAN (vec 0, V:real^3 -> bool, E ) `;
REWRITE_TAC[FAN; fan1; fan2];
STRIP_TAC;
SUBGOAL_THEN` FINITE V /\
     (!v. v IN V ==> (f: real^3 -> real -> real^3) v continuous atreal (&0)) /\
     INJ (\v. f v (&0)) V (IMAGE (\v. f v (&0)) V) ` MP_TAC;
ASM_REWRITE_TAC[];
CONJ_TAC;
GEN_TAC THEN STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [` v:real^3 `;` &0 `]));
DOWN THEN SIMP_TAC[];
UNDISCH_TAC` !v. v IN V ==> f v (&0) = v:real^3 `;
REWRITE_TAC[INJ; IN_IMAGE];
MESON_TAC[];
NHANH (
ISPECL [` f: real^3 -> real -> real^3 `;` &0 `] (
GENL [` ff: real^N -> real -> real^M `;` r: real `] CONT_ATREAL_INJ_PRESERVED));
STRIP_TAC;
DOWN THEN REWRITE_TAC[REAL_ARITH` a - &0 = a `];
STRIP_TAC;
EXISTS_TAC ` min e e' `;
ASM_REWRITE_TAC[REAL_LT_MIN];
FIRST_ASSUM NHANH;
SUBGOAL_THEN` ! f s. INJ (f:real^3 -> real^3) s (IMAGE f s) <=> BIJ f s (IMAGE f s ) ` ASSUME_TAC;
REWRITE_TAC[BIJ; SURJ; IN_IMAGE];
MESON_TAC[];


ASM_REWRITE_TAC[];
GEN_TAC THEN STRIP_TAC;
ABBREV_TAC` V' = IMAGE (\v. (f:real^3 -> real -> real^3) v t) V `;
ABBREV_TAC` E' = IMAGE (\s. IMAGE (\v. (f: real^3 -> real -> real^3) v t) s) E `;
ABBREV_TAC` ff = (\(x,y). (f:real^3 -> real -> real^3) x t, f y t) `;

MP_TAC (SPEC` (\v. (f:real^3 -> real -> real^3) v t ) ` (
GEN ` f: real^3 -> real^3 ` HYP_ISO_LEMMAA));
ANTS_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` FAN (vec 0,IMAGE (\v. (f: real^3 -> real -> real^3) v t) V,IMAGE (IMAGE (\v. f v t)) E) ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];

EXPAND_TAC "V'";
EXPAND_TAC "E'";
SIMP_TAC[ETA_AX];

SUBGOAL_THEN` FAN (vec 0,IMAGE (\v. (f: real^3 -> real -> real^3) v t) V,IMAGE (IMAGE (\v. f v t)) E) ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
DOWN THEN DOWN THEN DOWN;
SIMP_TAC[ETA_AX; local_fan];
REPEAT STRIP_TAC;


LET_TAC;
UNDISCH_TAC` local_fan (V,E,FF) `;
REWRITE_TAC[local_fan];
LET_TAC;
STRIP_TAC;
UNDISCH_TAC` hyp_iso (ff: real^3 # real^3 -> real^3 # real^3) (H',H) `;
NHANH IMAGE_FACE_F;
STRIP_TAC;
CONJ_TAC;
EXISTS_TAC ` (ff: real^3 # real^3 -> real^3 # real^3) x `;
DOWN THEN DOWN;
REWRITE_TAC[hyp_iso; BIJ; INJ];
ASM_SIMP_TAC[];

MATCH_MP_TAC (
let tt = GEN_ALL HYP_ISO_DIH2K_PRESERVED in
ISPECL [` (ff: real^3 # real^3 -> real^3 # real^3  ) `;` H': (real^3 #real^3) hypermap `; ` H: (real^3 #real^3) hypermap `; ` k: num `] tt);
ASM_REWRITE_TAC[];

ASSUME_TAC2 (ISPEC` vec 0: real^3 ` (
GEN` x: real^N ` Wrgcvdr_cizmrrh.FAN_IMP_FIMITE_DARTS));
UNDISCH_TAC` FAN (vec 0, V:real^3 -> bool , E ) `;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
ASM_SIMP_TAC[];
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x: real^3 # real^3 `));
FIRST_X_ASSUM (SUBST1_TAC o SYM);
UNDISCH_TAC` (x: real^3 # real^3) IN dart H' `;
NHANH Hypermap.lemma_face_subset;
STRIP_TAC;
SUBGOAL_THEN` FINITE (face H' (x:real^3 # real^3 )) ` MP_TAC;
REWRITE_TAC[Hypermap.FACE_FINITE];
UNDISCH_TAC` hyp_iso (ff: real^3 # real^3 -> real^3 # real^3 ) (H', H) `;
REWRITE_TAC[hyp_iso; BIJ];
NHANH INJ_IMP_BIJ_IMAGE;
STRIP_TAC;
STRIP_TAC;

UNDISCH_TAC` face H' (x: real^3 # real^3) SUBSET dart H' `;
UNDISCH_TAC`  INJ (ff: real^3 # real^3 -> real^3 # real^3 ) (dart H') (dart H) `;
PHA;
NHANH INJ_BIJ_IMAGE;
STRIP_TAC;
DOWN;
UNDISCH_TAC` FINITE (face H' (x: real^3 # real^3)) `;
PHA;
NHANH Misc_defs_and_lemmas.BIJ_CARD;
STRIP_TAC;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
UNDISCH_TAC` dih2k (H': (real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) `;
ASM_REWRITE_TAC[]]);;






let NORM_CROSS_LE = 
prove_by_refinement(` norm ( u cross v) <= norm u * norm v `,

[MP_TAC (SPEC_ALL Trigonometry1.cross_mag);
SIMP_TAC[];
MP_TAC SIN_BOUNDS;
ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `];
REWRITE_TAC[REAL_ARITH` a * b - a * b * c = a * b * ( &1 - c ) `];
MP_TAC NORM_POS_LE;
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_LE_MUL; NORM_POS_LE]]);;




let CONT_ATREAL_REAL_CONTS = 
prove_by_refinement (` f continuous atreal r 
==> (\r. ((f r) cross y ) dot ( x cross y)) real_continuous atreal r `,

[REWRITE_TAC[real_continuous_atreal; continuous_atreal];
REPEAT STRIP_TAC;
REWRITE_TAC[GSYM DOT_LSUB];
REWRITE_TAC[VEC3_RULE` x cross y - z cross y = ( x - z) cross y `];
ASM_CASES_TAC` (y:real^3) = vec 0 `;
ASM_REWRITE_TAC[CROSS_RZERO; DOT_RZERO; REAL_ABS_0];
EXISTS_TAC` e: real `;
ASM_REWRITE_TAC[];
ASM_CASES_TAC` (x:real^3) = vec 0 `;
ASM_REWRITE_TAC[CROSS_LZERO; DOT_RZERO; REAL_ABS_0];
EXISTS_TAC` e:real `;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (MP_TAC o (SPEC` e / (norm (x:real^3) * norm (y:real^3) * norm (y:real^3) ) `));
ANTS_TAC;
MATCH_MP_TAC REAL_LT_DIV;
ASM_REWRITE_TAC[];
MATCH_MP_TAC REAL_LT_MUL;
ASM_REWRITE_TAC[NORM_POS_LT];
MATCH_MP_TAC REAL_LT_MUL;
ASM_REWRITE_TAC[NORM_POS_LT];
STRIP_TAC;
EXISTS_TAC` d:real `;
FIRST_X_ASSUM NHANH;
ASM_REWRITE_TAC[];

REPEAT STRIP_TAC;
MP_TAC (ISPECL [` ( f (x': real) - f r ) cross y `;` x cross y `] NORM_CAUCHY_SCHWARZ_ABS);
ASSUME_TAC (SPECL [` (f:real -> real^3) x' - f r `;` y: real^3 `] (GEN_ALL NORM_CROSS_LE));
MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `);

SUBGOAL_THEN` norm ((f (x':real) - f r) cross y) * norm (x cross y) <= (norm ( f x' - f r) * norm y ) * norm (x cross y ) ` ASSUME_TAC;
MATCH_MP_TAC REAL_LE_RMUL;
ASM_REWRITE_TAC[NORM_POS_LE];

DOWN;
MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `);

MP_TAC (
SPECL [` x:real^3 `;` y: real^3 `] (GEN_ALL NORM_CROSS_LE));
STRIP_TAC;
SUBGOAL_THEN` &0 <= norm ((f: real -> real^3) x' - f r) * norm (y:real^3) ` ASSUME_TAC;
MATCH_MP_TAC REAL_LE_MUL;
REWRITE_TAC[NORM_POS_LE];
UNDISCH_TAC` norm (x cross y) <= norm x * norm y `;
DOWN THEN PHA;
NHANH Real_ext.REAL_LE_RMUL_IMP;
DOWN THEN DOWN;
REWRITE_TAC[dist];
REPEAT STRIP_TAC;
ONCE_REWRITE_TAC[REAL_MUL_SYM];
DOWN;
MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `);
SUBGOAL_THEN ` &0 < norm (x:real^3) /\ &0 < norm (y:real^3) ` MP_TAC;
ASM_REWRITE_TAC[NORM_POS_LT];
STRIP_TAC;
ONCE_REWRITE_TAC[REAL_ARITH` (x * y ) * a * y = a * x * y * y `];
SUBGOAL_THEN` &0 < norm (x:real^3) * norm y * norm (y:real^3) ` MP_TAC;
DOWN THEN DOWN;
MESON_TAC[REAL_LT_MUL];
UNDISCH_TAC` norm ((f:real -> real^3) x' - f r) < e / (norm (x:real^3) * norm y * norm (y:real^3)) `;
PHA;
NHANH REAL_LT_RMUL;
STRIP_TAC THEN DOWN;
ASM_SIMP_TAC[REAL_FIELD` &0 < a ==> e / a * a = e `]]);;







let CONTINUOUS_POS_PRES = 
prove_by_refinement (
` ~ collinear {(x:real^3),y, vec 0} /\ f r = a % x + b % y /\ &0 < a /\
f continuous atreal r
==> ? e. &0 < e /\ ! t. abs t < e ==> ! t1 t2. f ( r + t ) = t1 % x + t2 % y ==> &0 < t1 `,

[NHANH  CONT_ATREAL_REAL_CONTS;
REWRITE_TAC[real_continuous_atreal];
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC` a * norm ( x cross y ) * norm ( x cross y ) `));
ANTS_TAC;
MATCH_MP_TAC REAL_LT_MUL;
ASM_REWRITE_TAC[];
MATCH_MP_TAC REAL_LT_MUL;
REWRITE_TAC[TAUT` a /\ a <=> a `];
REWRITE_TAC[NORM_POS_LT; CROSS_EQ_0];
UNDISCH_TAC` ~collinear {x, y:real^3, vec 0} `;
SIMP_TAC[INSERT_COMM];
STRIP_TAC;
EXISTS_TAC` d: real `; ASM_REWRITE_TAC[] ;
GEN_TAC;
REPEAT STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC` r + (t:real) `));
ANTS_TAC;
ASM_REWRITE_TAC[REAL_ARITH` (a + b) - a = b `];

ASM_REWRITE_TAC[GSYM DOT_LSUB; VEC3_RULE` x cross z - y cross z = ( x - y) cross z `];
REWRITE_TAC[VECTOR_ARITH` (t1 % x + t2 % y) - (a % x + b % y) = ( t1 - a ) % x + ( t2 - b ) % y `; CROSS_LADD; CROSS_LMUL; CROSS_REFL];
REWRITE_TAC[VECTOR_ARITH` x + a % vec 0 = x `; DOT_LMUL; REAL_ABS_MUL; DOT_SQUARE_NORM];
SUBGOAL_THEN` &0 <= norm (x cross y) pow 2 ` MP_TAC;
REWRITE_TAC[REAL_LE_POW_2];

REWRITE_TAC[GSYM REAL_ABS_REFL];
SIMP_TAC[REAL_POW_2];

REWRITE_TAC[REAL_ABS_REFL];
REWRITE_TAC[REAL_ARITH` &0 <= a <=> a = &0 \/ &0 < a `];
STRIP_TAC;
ASM_SIMP_TAC[];
REAL_ARITH_TAC;
ASM_SIMP_TAC[REAL_LT_RMUL_EQ];
UNDISCH_TAC` &0 < a `;
REAL_ARITH_TAC]);;




let IVS_RHO_NODE_V_IN_FF = 
prove_by_refinement(` local_fan (V,E,FF) /\ v IN V ==> ivs_rho_node1 FF v, v IN FF `,

[NHANH Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC`ivs_rho_node1 FF v `));
ANTS_TAC;
MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
ASM_REWRITE_TAC[];
ASSUME_TAC2 Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS;
ASM_REWRITE_TAC[]]);;




let IN_AFF_GT_IMP_AZIMEQ = 
prove_by_refinement(
` x IN aff_gt {u,v} {y} ==> azim u v w  x = azim u v w y `,

[
ASM_CASES_TAC` collinear {u,v,w:real^3} `;
ASM_SIMP_TAC[AZIM_DEGENERATE];
ASM_CASES_TAC` collinear {u,v,y:real^3} `;
ASM_SIMP_TAC[AZIM_DEGENERATE];
DOWN_TAC;
NHANH Fan.th3b;
STRIP_TAC;
DOWN THEN DOWN;
ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL];
MP_TAC (ISPECL [` {u, v:real^3} `;` {y:real^3} `] AFF_GT_SUBSET_AFFINE_HULL);
REWRITE_TAC[SUBSET];
DISCH_THEN NHANH;
REPEAT STRIP_TAC;
SUBGOAL_THEN` affine hull ({u, v:real^3} UNION {y}) = affine hull {u,v} ` ASSUME_TAC;
MATCH_MP_TAC AFFINE_HULLS_EQ;
REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {c,a,b} `];
CONJ_TAC;
ONCE_REWRITE_TAC[INSERT_SUBSET];
ASM_REWRITE_TAC[];
REWRITE_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL];
MP_TAC (SPEC` {u,v:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
MATCH_MP_TAC (SET_RULE` a SUBSET b ==> c SUBSET a ==> c SUBSET b `);
MATCH_MP_TAC HULL_MONO;
CONV_TAC SET_RULE;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN;
ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL; AZIM_DEGENERATE];
DOWN_TAC;
REWRITE_TAC[AZIM_EQ_IMP]]);;



let IN_AFF_GT_IMP_AZIMEQ2 = 
MESON[IN_AFF_GT_IMP_AZIMEQ]` x IN aff_gt {u, v} {y} ==> 
! w. azim u v w x = azim u v w y `;;





let NOT_COLL_IMP_ZERO_DETER = 
prove_by_refinement(` ~ collinear {vec 0, u, v } ==>
(! a b. a % u + b % v = vec 0 <=> a = &0 /\ b = &0) `,

[REWRITE_TAC[Local_lemmas1.COLL_EQ_DEPENDENT];
STRIP_TAC;
GEN_TAC THEN GEN_TAC;
EQ_TAC;
DOWN;
MESON_TAC[];
SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]]);;


let CROSS_IN_SAME_DIRECTION = 
prove_by_refinement (` local_fan (V,E,FF) /\
     v IN V /\
     {ITER n (rho_node1 FF) v | n <= l} = U /\
     plane P /\
     vec 0 IN P /\
     U SUBSET P /\
v cross rho_node1 FF v = e
     ==> (!i. i < l 
              ==> ? k. &0 < k /\
ITER i (rho_node1 FF) v cross ITER ( i + 1) (rho_node1 FF ) v = k % e ) `,

[NHANH Local_lemmas.RHO_NODE_SET_IN_A_PLANE_IMP_POS_DIRECT;
ASM_CASES_TAC` l = 0 `;
ASM_REWRITE_TAC[ARITH_RULE` ~( n < 0) `];
STRIP_TAC;
SUBGOAL_THEN` {vec 0, v, rho_node1 FF v } SUBSET P ` ASSUME_TAC;
ONCE_REWRITE_TAC[INSERT_SUBSET];
ASM_REWRITE_TAC[];
MATCH_MP_TAC SUBSET_TRANS;
EXISTS_TAC` U: real^3 -> bool `;
ASM_REWRITE_TAC[];
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
CONJ_TAC;
EXISTS_TAC` 0 `;
REWRITE_TAC[ITER; ARITH_RULE` 0 <= l `];
EXISTS_TAC` 1 `;
REWRITE_TAC[ITER1];
MATCH_MP_TAC (ARITH_RULE` ~( l = 0) ==> 1 <= l `);
ASM_REWRITE_TAC[];
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
DOWN THEN DOWN;
PHA;
UNDISCH_TAC` plane  (P: real^3 -> bool) `;
PHA;
NHANH Local_lemmas.THREE_NOT_COLL_DETER_PLANE;
STRIP_TAC;
NHANH (ARITH_RULE` i < (l:num) ==> i <= l /\ i + 1 <= l `);
GEN_TAC THEN STRIP_TAC;
SUBGOAL_THEN` ITER i (rho_node1 FF) v IN U /\ ITER (i + 1) (rho_node1 FF) v IN U` ASSUME_TAC;
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
DOWN THEN DOWN;
MESON_TAC[];

DOWN;
UNDISCH_TAC` U SUBSET (P: real^3 -> bool) `;
REWRITE_TAC[SUBSET];
DISCH_THEN NHANH ;
EXPAND_TAC "P";
REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3];
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC ` i:num `));
DOWN;
ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; CROSS_LADD; CROSS_RADD];
REWRITE_TAC[CROSS_LMUL; CROSS_RMUL; CROSS_REFL; VECTOR_MUL_LZERO; VECTOR_MUL_RZERO];
REWRITE_TAC[VECTOR_ADD_LID; VECTOR_ADD_RID];
ASM_REWRITE_TAC[VECTOR_MUL_ASSOC];
ONCE_REWRITE_TAC[CROSS_SKEW];
ASM_REWRITE_TAC[VECTOR_ARITH` (v' * w') % e + (w * v'') % --e = ((v' * w') - (w * v'')) % e `];
REWRITE_TAC[DOT_LMUL];
UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `;
ASM_REWRITE_TAC[GSYM CROSS_EQ_0];
REWRITE_TAC[GSYM DOT_POS_LT];
SIMP_TAC[REAL_LT_MUL_EQ];
STRIP_TAC;
MESON_TAC[]]);;





let ITER_CROSS_SAME_DIRECTION = 
prove_by_refinement
(`local_fan (V,E,FF) /\
     v IN V /\
     {ITER n (rho_node1 FF) v | n <= l} = U /\
     plane P /\
     vec 0 IN P /\
     U SUBSET P 
     ==> (!i j. i < l /\ j < l
               ==> ? k. &0 < k /\
ITER i (rho_node1 FF) v cross ITER ( i + 1) (rho_node1 FF ) v = 
k % (ITER j (rho_node1 FF) v cross ITER ( j + 1) (rho_node1 FF ) v) ) `,

[STRIP_TAC;
ABBREV_TAC ` e = v cross rho_node1 FF v `;
ASSUME_TAC2 CROSS_IN_SAME_DIRECTION;
FIRST_X_ASSUM NHANH;
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
EXISTS_TAC` k / (k': real) `;
CONJ_TAC;
MATCH_MP_TAC REAL_LT_DIV;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[REAL_FIELD` &0 < a ==> x / a * a = x `; VECTOR_MUL_ASSOC]]);;


let ITER_IN_AFF_GT_2_1 = 
prove_by_refinement(` local_fan (V,E,FF) /\
     v IN V /\
     {ITER n (rho_node1 FF) v | n <= l} = U /\
     plane P /\
     vec 0 IN P /\
     U SUBSET P
==> (! i. i < l - 1 ==> 
ITER ( i + 2) (rho_node1 FF) v IN aff_lt {vec 0, ITER (i + 1) (rho_node1 FF) v } {ITER i (rho_node1 FF ) v } ) `,

[STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE3;
GEN_TAC;
FIRST_X_ASSUM (ASSUME_TAC o (SPEC` i:num `));
STRIP_TAC;
SUBGOAL_THEN` {vec 0, ITER i (rho_node1 FF) v, ITER ( i + 1) (rho_node1 FF) v} SUBSET P` ASSUME_TAC;
ONCE_REWRITE_TAC[INSERT_SUBSET];
ASM_REWRITE_TAC[];
MATCH_MP_TAC SUBSET_TRANS;
EXISTS_TAC` U: real^3 -> bool`;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
CONJ_TAC;
EXISTS_TAC` i:num `;
ASM_REWRITE_TAC[];
DOWN;
ARITH_TAC;

EXISTS_TAC` i + 1 `;
ASM_REWRITE_TAC[];
DOWN;
ARITH_TAC;
UNDISCH_TAC` ~collinear
       {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} `;
UNDISCH_TAC` {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} SUBSET
      P `;
UNDISCH_TAC` plane   (P:real^3 -> bool) `;
PHA;
NHANH Local_lemmas.THREE_NOT_COLL_DETER_PLANE;
STRIP_TAC;
SUBGOAL_THEN` ITER (i + 2) (rho_node1 FF) v IN U ` MP_TAC;
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` i + 2 `;
REWRITE_TAC[];
UNDISCH_TAC` i < l - 1 `;
ARITH_TAC;
UNDISCH_TAC` (U:real^3 -> bool) SUBSET P `;
REWRITE_TAC[SUBSET];
STRIP_TAC;
FIRST_ASSUM NHANH;
EXPAND_TAC "P";
REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3];
STRIP_TAC;
MP_TAC ITER_CROSS_SAME_DIRECTION;
ANTS_TAC;
ASM_REWRITE_TAC[SUBSET];
DISCH_THEN (MP_TAC o (SPECL [` i + 1`;` i:num `]));
ASSUME_TAC2 (ARITH_RULE` i < l - 1 ==> i + 1 < l `);
ASSUME_TAC2 (ARITH_RULE` i < l - 1 ==> i < l `);
ANTS_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[ARITH_RULE` (a + 1) + 1 = a + 2 `; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
REWRITE_TAC[CROSS_RADD; CROSS_RMUL; CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID];
STRIP_TAC;
DOWN;
ABBREV_TAC` e1 = ITER i (rho_node1 FF) v cross ITER (i + 1) (rho_node1 FF) v `;
ONCE_REWRITE_TAC[CROSS_SKEW; VECTOR_ARITH` a % -- x = ( -- a ) % x `];
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ~( e1:real^3 = vec 0) ` MP_TAC;
EXPAND_TAC "e1";
REWRITE_TAC[CROSS_EQ_0];
ASM_REWRITE_TAC[];
SIMP_TAC[VECTOR_MUL_RCANCEL; VECTOR_ARITH` a % -- x = ( -- a ) % x `];
STRIP_TAC THEN STRIP_TAC;


UNDISCH_TAC` ~collinear
       {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} `;
ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
NHANH Fan.th3a;
NHANH AFF_LT_2_1;
SIMP_TAC[Collect_geom.PER_SET2];
STRIP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC `u: real `;
EXISTS_TAC` w: real `;
EXISTS_TAC` v':real`;
ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];
CONJ_TAC;
UNDISCH_TAC` --v' = (k: real) `;
UNDISCH_TAC ` &0 < k `;
REAL_ARITH_TAC;
CONJ_TAC;
UNDISCH_TAC` u + v' + w = &1 `;
REAL_ARITH_TAC;
CONV_TAC VECTOR_ARITH]);;



(*
search[` v cross rho_node1 FF v `];;
*)

let AZIM_PI_ITER_LOCAL_FAN = 
prove_by_refinement
(`local_fan (V,E,FF) /\
     v IN V /\
     {ITER n (rho_node1 FF) v | n <= l} = U /\
     plane P /\
     vec 0 IN P /\
     U SUBSET P
==> (!i. i < l - 1
              ==> azim (vec 0) (ITER (i + 1) (rho_node1 FF ) v ) (ITER (i) (rho_node1 FF ) v ) (ITER (i + 2) (rho_node1 FF ) v )  = pi ) `,

[NHANH ITER_IN_AFF_GT_2_1;
STRIP_TAC;
GEN_TAC;
FIRST_X_ASSUM NHANH;
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE3;
FIRST_ASSUM (MP_TAC o (SPEC` i: num `));
FIRST_ASSUM (MP_TAC o (SPEC` i + 1`));
STRIP_TAC;
ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
DOWN THEN DOWN;
DOWN;
REWRITE_TAC[ARITH_RULE` (a + 1) + 1 = a + 2 `];
MESON_TAC[AZIM_EQ_PI_ALT]]);;



let LOCAL_CONVEX_NOT_COLLINEAR = 
prove_by_refinement
(`convex_local_fan (V,E,FF) /\ lunar (v,w) V E
     ==> (!u. u IN V /\ ~(u = v) /\ ~(u = w)
              ==> ~ collinear {vec 0, v, u}) `,

[NHANH LUNAR_IMP_IN_TWO_HAFLS_PLANE;
REWRITE_TAC[lunar; INSERT_SUBSET];
NHANH Local_lemmas.CVX_LO_IMP_LO;
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
FIRST_X_ASSUM NHANH;
GEN_TAC;
DOWN THEN DOWN;
MESON_TAC[Planarity.aff_gt_imp_not_collinear]]);;

let LOCAL_CONVEX_NOT_COLLINEAR2 = 
prove(` convex_local_fan (V,E,FF) /\ lunar (v,w) V E
     ==> (!u. u IN V /\ ~(u = v) /\ ~(u = w) ==> ~collinear {vec 0, w, u})`,

ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM] THEN 
NHANH LOCAL_CONVEX_NOT_COLLINEAR THEN MESON_TAC[]);;


let LOCAL_FAN_RHO_NODE_PROS2 = 
prove(` local_fan (V,E,FF)
     ==> (!x. x IN V ==> x,rho_node1 FF x IN FF) `,
 NHANH Local_lemmas.LOCAL_FAN_RHO_NODE_PROS THEN SIMP_TAC[]);;


(* ============================= 
-======================================
================================

*)

let MHAEYJN_CONVEX_LOCAL_FAN = 
prove_by_refinement (
`!a b V E FF f v w u.
     convex_local_fan (V,E,FF) /\
     lunar (v,w) V E /\
     deformation f V (a,b) /\
     interior_angle1 (vec 0) FF v < pi /\
     u IN V /\
     ~(u = v) /\
     ~(u = w) /\
     (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
     (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})
     ==> (?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> convex_local_fan
                       (IMAGE (\v. f v t) V,
                        IMAGE (IMAGE (\v. f v t)) E,
                        IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF)
                       ))`,

[REPEAT GEN_TAC;
NHANH_PAT`\x. x ==> y ` Local_lemmas.CVX_LO_IMP_LO;
NHANH_PAT`\x. x ==> y ` Local_lemmas.LOCAL_FAN_FINITE_V;
NHANH Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
REWRITE_TAC[FAN; UNIONS_SUBSET];
STRIP_TAC;
MP_TAC SUB_LUNAR_DEFORM_LEMMA;
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` deformation f (V:real^3 -> bool) (a,b) `;
REWRITE_TAC[deformation; real_interval; IN_ELIM_THM];
ASM_SIMP_TAC[];
REWRITE_TAC[REAL_BOUNDS_LT];
STRIP_TAC;
ASSUME_TAC2 XRECQNS_UPDATE;
ASSUME_TAC2 HKIRPEP_ALT;
DOWN THEN DOWN THEN STRIP_TAC;
STRIP_TAC;

SUBGOAL_THEN` ! x y. x IN V /\ y IN V /\ ~ collinear {vec 0, x, y} /\
(? a b .
(f:real^3 -> real -> real^3) u (&0) = a % x + b % y /\ &0 < a ) ==>
(?e. &0 < e /\
                  (!t. abs t < e
                       ==> (!t1 t2. f u (t) = t1 % x + t2 % y ==> &0 < t1))) ` ASSUME_TAC;

SUBGOAL_THEN` deformation (f:real^3 -> real -> real^3) V (a,b) ` MP_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[deformation];
STRIP_TAC;
REPEAT GEN_TAC THEN STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`u: real^3 `;` &0 `]));
REPEAT GEN_TAC;

ONCE_REWRITE_TAC[MESON[REAL_ARITH` t = &0 + t `]` f u t = A <=> f u ( &0 + t ) = A `];
MATCH_MP_TAC (GEN_ALL CONTINUOUS_POS_PRES);
EXISTS_TAC` b': real `;
EXISTS_TAC` a': real `;
UNDISCH_TAC` ~ collinear {vec 0, x, y:real^3} `;
ASM_REWRITE_TAC[INSERT_COMM];
ABBREV_TAC` ss = { (x,y) | x IN V /\
          y IN V /\
          ~collinear {vec 0, x, y} /\
          (?a b. (f:real^3 -> real -> real^3) u (&0) = a % x + b % y /\ &0 < a) } ` ;
SUBGOAL_THEN` ss SUBSET { (x,y) | x IN (V:real^3 -> bool) /\ y IN V} ` MP_TAC;
EXPAND_TAC "ss";
CONV_TAC SET_RULE;
STRIP_TAC;
SUBGOAL_THEN` FINITE {x,y | x IN (V:real^3 -> bool) /\ y IN V} ` ASSUME_TAC;
MATCH_MP_TAC FINITE_PRODUCT;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ss SUBSET {x,y | x IN V /\ (y:real^3) IN V} `;
UNDISCH_TAC` FINITE {x,y | x IN V /\ y:real^3 IN V} `;
PHA;
NHANH FINITE_SUBSET;
STRIP_TAC;

SUBGOAL_THEN`  (!x. (x:real^3 # real^3) IN ss ==> 
(?e. &0 < e /\ (!t. abs t < e
                        ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % (FST x) + t2 % (SND x) ==> &0 < t1))))` MP_TAC;
EXPAND_TAC "ss";
REWRITE_TAC[IN_ELIM_THM];
GEN_TAC;
STRIP_TAC;
ASM_SIMP_TAC[];
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
EXISTS_TAC` a': real `;
EXISTS_TAC` b': real `;
ASM_REWRITE_TAC[];
DOWN;
PHA;
NHANH Deformation.MINIMIZE_OVER_MEMBERS;
STRIP_TAC;
EXISTS_TAC` min b ( min (-- a) ( min e (min e' e''))) `;
SUBGOAL_THEN` deformation f (V: real^3 -> bool) (a,b) ` MP_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[deformation; real_interval; IN_ELIM_THM];
STRIP_TAC;
REWRITE_TAC[REAL_LT_MIN];
CONJ_TAC;
ASM_REWRITE_TAC[REAL_ARITH` &0 < -- a <=> a < &0 `];

REWRITE_TAC[convex_local_fan];
GEN_TAC THEN STRIP_TAC;
ABBREV_TAC` IV = IMAGE (\v. (f:real^3 -> real -> real^3) v t) V `;
ABBREV_TAC` IE = IMAGE (IMAGE (\v. (f: real^3 -> real -> real^3) v t)) E`;
ABBREV_TAC` IF = IMAGE (\uv. (f: real^3 -> real -> real^3) (FST uv) t,f (SND uv) t) FF `;
SUBGOAL_THEN` local_fan (IV, IE , IF) ` MP_TAC;
UNDISCH_TAC` !t. abs t < e'
          ==> local_fan
              (IMAGE (\v. f v t) V,
               IMAGE (\s. IMAGE (\v. f v t) s) E,
               IMAGE (\(u,v). (f: real^3 -> real -> real^3) u t,f v t) FF) `;
DISCH_THEN (ASSUME_TAC2 o SPEC_ALL);
DOWN;
UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[ETA_AX];
SUBGOAL_THEN`! (fg: real^3 -> real^3). (\(u:real^3,v:real^3). fg u,fg v) = (\uv. fg (FST uv),fg (SND uv)) ` ASSUME_TAC;
REWRITE_TAC[FUN_EQ_THM; BETA_THM];
GEN_TAC THEN GEN_TAC;
PAT_ONCE_REWRITE_TAC`\x. f x = y ` [GSYM PAIR];
PURE_ONCE_REWRITE_TAC[BETA_THM];
ABBREV_TAC` x1 = FST (x:real^3 # real^3) `;
ABBREV_TAC` x2 = SND (x:real^3 # real^3) `;
REWRITE_TAC[BETA_THM];
ASM_REWRITE_TAC[];

SIMP_TAC[] THEN STRIP_TAC;
GEN_TAC;

UNDISCH_TAC` local_fan (IV, IE, IF) `;
PHA;  PAT_ONCE_REWRITE_TAC`\x. y /\ x ==> z ` [GSYM PAIR];
ABBREV_TAC` xx = FST (x:real^3 # real^3) `;
NHANH Local_lemmas.LOCAL_FAN_IMP_IN_V;
NHANH Local_lemmas.DETER_RHO_NODE;
STRIP_TAC;
ONCE_REWRITE_TAC[GSYM PAIR];
ABBREV_TAC` xy = SND (x:real^3 # real^3) `;
UNDISCH_TAC` xx:real^3 IN IV `;
UNDISCH_TAC` local_fan (IV,IE,IF) `;
PHA;
UNDISCH_TAC` rho_node1 IF xx = xy `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];


NHANH Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND;
NHANH Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
SIMP_TAC[];
STRIP_TAC;
ASSUME_TAC2 LOCAL_FAN_FACE_FF;
SUBGOAL_THEN` lunar (v:real^3,w) V E ` MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
REWRITE_TAC[lunar; INSERT_SUBSET];
STRIP_TAC;
ASSUME_TAC2 Localization.LOFA_IMP_LT_CARD_SET_V_ALT;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `));
DOWN THEN STRIP_TAC;
ASSUME_TAC2 (SPEC`u: real^3 ` Local_lemmas1.IVS_RHO_NODE_DIFF_ID);
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `));
SUBGOAL_THEN`! v:real^3. v IN V ==> ivs_rho_node1 FF (rho_node1 FF v) = v ` ASSUME_TAC;
GEN_TAC;
STRIP_TAC;
MATCH_MP_TAC Local_lemmas.IVS_RHO_IDD;
ASM_REWRITE_TAC[];
SUBGOAL_THEN`!v. v IN V ==> rho_node1 FF (ivs_rho_node1 FF v) = v ` MP_TAC;
GEN_TAC;
STRIP_TAC;
MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS;
ASM_REWRITE_TAC[];
STRIP_TAC;

SUBGOAL_THEN` ! v. v: real^3 IN V ==> rho_node1 FF v IN V ` ASSUME_TAC;
GEN_TAC THEN STRIP_TAC;
MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_SIMP_TAC[];
SUBGOAL_THEN` deformation f (V: real^3 -> bool) (a,b) ` MP_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[deformation];
STRIP_TAC;
SUBGOAL_THEN` t IN real_interval (a,b) ` ASSUME_TAC;
REWRITE_TAC[IN_ELIM_THM; real_interval];
ASM_REWRITE_TAC[];
UNDISCH_TAC` abs t < b `;
UNDISCH_TAC` abs t < -- a `;
REAL_ARITH_TAC;
ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) (rho_node1 FF u) t = rho_node1 FF u ` ASSUME_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_SIMP_TAC[];
SUBGOAL_THEN` (f:real^3 -> real -> real^3) (rho_node1 FF (rho_node1 FF u)) t = rho_node1 FF (rho_node1 FF u )` ASSUME_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_SIMP_TAC[];
SUBGOAL_THEN` (f:real^3 -> real -> real^3) (ivs_rho_node1 FF u) t = ivs_rho_node1 FF u ` ASSUME_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_SIMP_TAC[];

ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS;
DOWN THEN DISCH_THEN (ASSUME_TAC o GSYM);
UNDISCH_TAC` xx: real^3 IN IV `;
EXPAND_TAC "IV";
REWRITE_TAC[IN_IMAGE];
STRIP_TAC;
SUBGOAL_THEN` ! (v:real^3). v IN V ==> (f:real^3 -> real -> real^3) v t, f (rho_node1 FF v) t IN IF ` ASSUME_TAC;
EXPAND_TAC "IF";
REWRITE_TAC[IN_IMAGE];
EXPAND_TAC "FF";
REWRITE_TAC[IN_ELIM_THM];
GEN_TAC THEN STRIP_TAC;
EXISTS_TAC` v', rho_node1 FF v' `;
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
EXISTS_TAC` v': real^3 `;
ASM_REWRITE_TAC[];

SUBGOAL_THEN` ! (v:real^3). v IN V ==> rho_node1 IF ((f:real^3 -> real -> 
real^3) v t ) = f ( rho_node1 FF v ) t ` ASSUME_TAC;
GEN_TAC THEN STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v': real^3 `));
DOWN;
UNDISCH_TAC` local_fan (IV, IE, IF) `;
PHA;
NHANH Local_lemmas.DETER_RHO_NODE;
SIMP_TAC[];
SUBGOAL_THEN` ! (v:real^3). v IN V ==> ivs_rho_node1 IF ((f:real^3 -> real -> 
real^3) v t ) = f ( ivs_rho_node1 FF v ) t ` ASSUME_TAC;
GEN_TAC THEN STRIP_TAC;
SUBGOAL_THEN` f (ivs_rho_node1 FF v') t, (f:real^3 -> real -> real^3) v' t IN IF ` ASSUME_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v' `));
FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v' `));
ANTS_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];
DOWN;
UNDISCH_TAC` local_fan (IV, IE, IF) `;
PHA;
NHANH Local_lemmas.IVS_RHO_NODE1_DETE;
SIMP_TAC[];
SUBGOAL_THEN` IV SUBSET (f:real^3 -> real -> real^3) u t INSERT V ` ASSUME_TAC;
REWRITE_TAC[SUBSET];
EXPAND_TAC "IV";
REWRITE_TAC[IN_IMAGE];
GEN_TAC THEN STRIP_TAC;
ASM_CASES_TAC` x''' = (u: real^3) `;
ASM_REWRITE_TAC[IN_INSERT];
ASM_SIMP_TAC[IN_INSERT];

UNDISCH_TAC` x': real^3 IN V `;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` (f:real^3 -> real -> real^3) (ivs_rho_node1 FF (ivs_rho_node1 FF u)) t = ivs_rho_node1 FF (ivs_rho_node1 FF u) ` ASSUME_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
CONJ_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];
UNDISCH_TAC` !v. v IN V ==> ~(rho_node1 FF (rho_node1 FF v) = v) `;
DISCH_THEN (MP_TAC o (SPEC` ivs_rho_node1 FF (ivs_rho_node1 FF u) `));
ANTS_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];

SUBGOAL_THEN` convex_local_fan (V,E,FF) ` MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
REWRITE_TAC[convex_local_fan];
STRIP_TAC;


ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS2;
SUBGOAL_THEN` ! v. v IN V
     ==> wedge_in_fan_ge  (v ,rho_node1 FF v) E =
         wedge_ge  (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) ` ASSUME_TAC;
GEN_TAC;
STRIP_TAC;
MATCH_MP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ! v. v IN V
     ==> azim_in_fan (v,rho_node1 FF v) E =
         azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) ` ASSUME_TAC;
GEN_TAC;
STRIP_TAC;
MATCH_MP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND;
ASM_REWRITE_TAC[];

(* ----- *)
ASSUME_TAC2 Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
DOWN;
NHANH IN_CONV0_IMP_AFF_EQ1;
STRIP_TAC;
SUBGOAL_THEN` w IN aff {vec 0, v:real^3 } ` ASSUME_TAC;
UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
MP_TAC (SPEC` {vec 0, w:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
REWRITE_TAC[SUBSET; Sphere.aff];
DISCH_THEN MATCH_MP_TAC;
REWRITE_TAC[IN_INSERT];


SUBGOAL_THEN` ! v:real^3. v IN V ==> ~collinear {vec 0, v, ivs_rho_node1 FF v} ` ASSUME_TAC;
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
DISCH_THEN (ASSUME_TAC o SYM);
GEN_TAC THEN STRIP_TAC;
MATCH_MP_TAC Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
ASM_REWRITE_TAC[];


ASSUME_TAC2 LUNAR_IMP_IN_TWO_HAFLS_PLANE;
SUBGOAL_THEN` ! x. x IN V /\ ~( x = v ) /\ ~( x = w:real^3) ==>
~ collinear {vec 0, v, x} ` ASSUME_TAC;
DOWN THEN PHA;
STRIP_TAC;
FIRST_ASSUM NHANH;
GEN_TAC;



SUBGOAL_THEN` ~collinear {vec 0, v, ivs_rho_node1 FF v} /\
~collinear {vec 0, v, rho_node1 FF v} ` MP_TAC;
ASM_SIMP_TAC[];
MESON_TAC[Planarity.aff_gt_imp_not_collinear];
ASM_SIMP_TAC[];






SUBGOAL_THEN` ! x. x IN V /\ ~( x = v ) /\ ~( x = w:real^3) ==>
rho_node1 FF x IN aff_ge {vec 0, v} {x} /\ ivs_rho_node1 FF x IN aff_ge {vec 0, v} {x} ` ASSUME_TAC;
DOWN THEN DOWN THEN PHA THEN STRIP_TAC;
GEN_TAC;
FIRST_ASSUM NHANH;
STRIP_TAC;
SUBGOAL_THEN` x'': real^3 IN V ` MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
UNDISCH_TAC` ~collinear {vec 0, v, x'':real^3} `;
NHANH Fan.th3a;
STRIP_TAC;
DOWN;
MP_TAC (SET_RULE` {} SUBSET {x'':real^3}`);
PHA;
NHANH AFF_GE_MONO_RIGHT;
REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; GSYM aff];
STRIP_TAC;
ASM_CASES_TAC` n = 0 `;
UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `;
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[ITER];
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_CASES_TAC` n = (i:num) `;
UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `;
ASM_REWRITE_TAC[];
ASSUME_TAC AFF_GT_SUBSET_AFF_GE;


ASM_CASES_TAC` n < (i:num) `;
SUBGOAL_THEN` x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n: num` ;
ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `];

ASM_REWRITE_TAC[IN_INTER];
UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];

SUBGOAL_THEN` ~ collinear {vec 0, v, rho_node1 FF v} ` MP_TAC;
ASM_SIMP_TAC[];
NHANH Fan.th3a;
NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION;
STRIP_TAC;
UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `;
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ONCE_REWRITE_TAC[EQ_SYM_EQ];
STRIP_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ~ collinear {vec 0, v, x'': real^3} ` MP_TAC;
ASM_SIMP_TAC[];
NHANH Fan.th3a;
NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION;
ASM_SIMP_TAC[];


STRIP_TAC;
UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w: real^3} `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
CONJ_TAC;
ASM_CASES_TAC` n = (i - 1) `;
EXPAND_TAC "x''";
REWRITE_TAC[GSYM ITER];
ASM_SIMP_TAC[ARITH_RULE` ~( i = 0) ==> SUC ( i - 1) = i `; IN_UNION];
SUBGOAL_THEN` rho_node1 FF x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` SUC n `;
EXPAND_TAC "x''";
REWRITE_TAC[GSYM ITER];
REWRITE_TAC[ARITH_RULE` 0 < SUC n `];
MATCH_MP_TAC (ARITH_RULE` n < i /\ ~( n = i - 1) ==> SUC n < i `);
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[IN_UNION; IN_INTER];
SIMP_TAC[];
ASM_CASES_TAC` n = 1`;
DOWN;
EXPAND_TAC "x''";
SIMP_TAC[ITER1];
ASM_SIMP_TAC[];
SIMP_TAC[IN_UNION];
REWRITE_TAC[aff];
STRIP_TAC;
DISJ1_TAC;
MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET];

SUBGOAL_THEN` ivs_rho_node1 FF x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n - 1 `;
EXPAND_TAC "x''";
ASSUME_TAC2 (ARITH_RULE`~( n = 0) ==> SUC ( n - 1) = n `);
EXPAND_TAC "n";
REWRITE_TAC[ITER];
SUBGOAL_THEN` ITER (n - 1) (rho_node1 FF) v IN V ` ASSUME_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;
ASM_SIMP_TAC[];

ASM_SIMP_TAC[];
UNDISCH_TAC` ~( n = 0) `;
UNDISCH_TAC` ~( n = 1) `;
UNDISCH_TAC` n < (i:num) `;
ARITH_TAC;
ASM_REWRITE_TAC[IN_INTER; IN_UNION];
SIMP_TAC[];

ASSUME_TAC2 (ARITH_RULE`  ~( n < (i:num) ) ==> (n - i) + i = n `);
SUBGOAL_THEN` x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n - (i:num) `;
ASM_REWRITE_TAC[];
EXPAND_TAC "n";
REWRITE_TAC[GSYM ITER_ADD];
ASM_REWRITE_TAC[];
CONJ_TAC;
UNDISCH_TAC` ~( n = (i:num)) `;
UNDISCH_TAC` ~( n < (i:num)) `;
ARITH_TAC;
ASM_SIMP_TAC[ARITH_RULE` ~( n < (i:num)) ==> ( n - i < j <=> n < i + j )`];

UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[IN_INTER];

SUBGOAL_THEN` ~ collinear {vec 0, v, ivs_rho_node1 FF v}` MP_TAC;
ASM_SIMP_TAC[];
PHA;
NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ONCE_REWRITE_TAC[EQ_SYM_EQ];
STRIP_TAC;
SUBGOAL_THEN` ~ collinear {vec 0, v, x'':real^3} ` MP_TAC;
ASM_SIMP_TAC[];
NHANH Fan.th3a;
NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION;
SIMP_TAC[];
STRIP_TAC;
CONJ_TAC;
ASM_REWRITE_TAC[];
ASM_CASES_TAC` n = (i + j) - 1 `;
EXPAND_TAC "x''";
REWRITE_TAC[GSYM ITER];
ASM_SIMP_TAC[];
ASSUME_TAC2 (ARITH_RULE` n < CARD (V:real^3 -> bool) ==> SUC (CARD V - 1) = CARD V `);
ASM_REWRITE_TAC[];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID;
FIRST_ASSUM (ASSUME_TAC2 o SPEC_ALL);
ASM_REWRITE_TAC[IN_UNION];
UNDISCH_TAC` aff {vec 0, v:real^3} = aff {vec 0, w} `;
DISCH_THEN (SUBST1_TAC o SYM);
REWRITE_TAC[aff];
MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET];


SUBGOAL_THEN` rho_node1 FF x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXPAND_TAC "x''";
REWRITE_TAC[GSYM ITER];
ASM_SIMP_TAC[ARITH_RULE` ~( n < i ) ==> SUC n = SUC ( n - i ) + i `];
REWRITE_TAC[GSYM ITER_ADD];
ASM_REWRITE_TAC[];
EXISTS_TAC ` SUC ( n - i ) `;
REWRITE_TAC[];
UNDISCH_TAC` n < CARD (V:real^3 -> bool) `;
UNDISCH_TAC` i + j = CARD (V: real^3 -> bool) `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~( n < (i:num)) `;
UNDISCH_TAC` ~ ( n = ( i + j ) - 1) `;
ARITH_TAC;
ASM_REWRITE_TAC[IN_INTER; IN_UNION];
SIMP_TAC[];

ASM_CASES_TAC` n = i + 1 `;
REWRITE_TAC[IN_UNION];
EXPAND_TAC "x''";
FIRST_ASSUM SUBST1_TAC;
REWRITE_TAC[GSYM ADD1; ITER];
ASM_SIMP_TAC[aff];
MESON_TAC[HULL_SUBSET; SUBSET; IN_INSERT];


SUBGOAL_THEN` ivs_rho_node1 FF x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` ASSUME_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXPAND_TAC "x''";
ASSUME_TAC2 (ARITH_RULE` ~( n < (i:num) ) /\ ~(n = i + 1) /\ ~( n = i ) ==> SUC ( n - 1 - i ) + i = n `);
EXPAND_TAC "n";
REWRITE_TAC[GSYM ITER_ADD; ITER];
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ITER (n - 1 - i) (rho_node1 FF) w IN V ` ASSUME_TAC;
ASM_SIMP_TAC[];
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];


ASM_SIMP_TAC[];
EXISTS_TAC` n - 1 - i `;
ASM_REWRITE_TAC[];
CONJ_TAC;
UNDISCH_TAC` ~(n = i + 1) `;
UNDISCH_TAC` ~( n < (i:num) ) `;
UNDISCH_TAC` ~( n = (i:num)) `;
ARITH_TAC;
UNDISCH_TAC` n < CARD (V:real^3 -> bool) `;
UNDISCH_TAC` i + j = CARD (V:real^3 -> bool) `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~( n < i:num ) `;
UNDISCH_TAC` ~( n = i:num ) `;
ARITH_TAC;
DOWN;
ASM_REWRITE_TAC[IN_INTER; IN_UNION];
SIMP_TAC[];

SUBGOAL_THEN` ! u:real^3. affine hull {vec 0, v, w, u} = affine hull {vec 0, v, u} ` ASSUME_TAC;
GEN_TAC;
REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ];
CONJ_TAC;
MATCH_MP_TAC HULL_MINIMAL;
REWRITE_TAC[AFFINE_AFFINE_HULL];
MP_TAC (SPEC` {vec 0, v, u': real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
SIMP_TAC[INSERT_SUBSET];
STRIP_TAC;
SUBGOAL_THEN` affine hull {vec 0, v:real^3} SUBSET affine hull {vec 0, v, u'}` MP_TAC;
MATCH_MP_TAC HULL_MONO;
CONV_TAC SET_RULE;
REWRITE_TAC[SUBSET];
DISCH_THEN MATCH_MP_TAC;
UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
ASM_REWRITE_TAC[GSYM aff];
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
UNDISCH_TAC` aff {vec 0, v} = aff { vec 0, w:real^3} `;
DISCH_THEN (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[];


MATCH_MP_TAC HULL_MONO;
CONV_TAC SET_RULE;



SUBGOAL_THEN`! x'. x' IN V ==> (f:real^3 -> real -> real^3) u t IN
wedge_ge  (vec 0) (x') (rho_node1 FF x')
     (ivs_rho_node1 FF x') ` ASSUME_TAC;
GEN_TAC;
STRIP_TAC;
ASM_CASES_TAC` x'' = (v:real^3) `;
UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM];
FIRST_ASSUM (MP_TAC o (SPEC` v, rho_node1 FF v ` ));
ANTS_TAC;
ASM_SIMP_TAC[];
REWRITE_TAC[SUBSET];
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `));
DOWN;
UNDISCH_TAC` !v. v IN V
          ==> wedge_in_fan_ge  (v,rho_node1 FF v) E =
              wedge_ge  (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `;
DISCH_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM];
SUBGOAL_THEN` ~ collinear {vec 0, v , u:real^3 } ` MP_TAC;
ASM_SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN` (!x. x IN (ss:real^3 # real^3 -> bool)
                   ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o (SPEC` (u:real^3, v:real^3) `));
ANTS_TAC;
EXPAND_TAC "ss";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` u:real^3 `;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `;
SIMP_TAC[INSERT_COMM];
STRIP_TAC;

ASM_SIMP_TAC[];
EXISTS_TAC` &1 `;
EXISTS_TAC` &0 `;
CONJ_TAC;
CONV_TAC VECTOR_ARITH;
REAL_ARITH_TAC;
REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[];
REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3];
STRIP_TAC;
DOWN;
REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];
ONCE_REWRITE_TAC[VECTOR_ADD_SYM];
FIRST_ASSUM NHANH;
STRIP_TAC;
UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `;
NHANH Fan.th3a;
NHANH AFF_GT_2_1;
STRIP_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, v} {u} ` ASSUME_TAC;
ASM_REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` u': real `;
EXISTS_TAC` v': real `;
EXISTS_TAC` w': real`;
ASM_REWRITE_TAC[];
CONV_TAC VECTOR_ARITH;
DOWN;
NHANH IN_AFF_GT_IMP_AZIMEQ2;
SIMP_TAC[];  
ASM_CASES_TAC` x'' = w:real^3 `;
UNDISCH_TAC` w = ITER i (rho_node1 FF)  v `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM];
FIRST_ASSUM (MP_TAC o (SPEC` w, rho_node1 FF w `));
ANTS_TAC;
ASM_SIMP_TAC[];

UNDISCH_TAC` !v. v IN V
          ==> wedge_in_fan_ge  (v,rho_node1 FF v) E =
              wedge_ge  (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w: real^3 `));
DOWN;
SIMP_TAC[];
STRIP_TAC;
REWRITE_TAC[SUBSET];
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u:real^3 `));
DOWN;
REWRITE_TAC[wedge_ge; IN_ELIM_THM];
SUBGOAL_THEN` ~collinear {vec 0, v, u:real^3} ` MP_TAC;
ASM_SIMP_TAC[];
ASM_REWRITE_TAC[Fan.collinear_fan];
PHA THEN STRIP_TAC;
SUBGOAL_THEN` ~( w = vec 0: real^3) ` MP_TAC;
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
ASM_SIMP_TAC[];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
ONCE_REWRITE_TAC[EQ_SYM_EQ];
UNDISCH_TAC` ~(u IN aff {vec 0, w: real^3}) `;
PHA;
REWRITE_TAC[GSYM Fan.collinear_fan];
NHANH Fan.th3a;
NHANH AFF_GT_2_1;
STRIP_TAC;
SUBGOAL_THEN` (!x. x IN ss
                   ==> (!t1 t2. (f: real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC` (u:real^3, w:real^3) `));
ANTS_TAC;
EXPAND_TAC "ss";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` u:real^3 `;
EXISTS_TAC` w:real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~collinear {vec 0, w, u: real^3} `;
SIMP_TAC[INSERT_COMM];
ASM_SIMP_TAC[];
STRIP_TAC;
EXISTS_TAC` &1 `;
EXISTS_TAC` &0 `;


CONJ_TAC;
CONV_TAC VECTOR_ARITH;
REAL_ARITH_TAC;


REWRITE_TAC[];
STRIP_TAC;

SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u }` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` affine hull {vec 0, v, w, u} SUBSET affine hull {vec 0, w, u:real^3} ` MP_TAC;
MATCH_MP_TAC HULL_MINIMAL;
REWRITE_TAC[AFFINE_AFFINE_HULL];
MP_TAC (ISPEC` {vec 0, w, u: real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
SIMP_TAC[INSERT_SUBSET];
STRIP_TAC;
MP_TAC (SET_RULE` {vec 0, w:real^3} SUBSET {vec 0, w, u} `);
NHANH (ISPEC` affine ` HULL_MONO);
REWRITE_TAC[SUBSET];
STRIP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `;
REWRITE_TAC[aff];
DISCH_THEN (SUBST1_TAC o SYM);


MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET];
REWRITE_TAC[SUBSET];
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` (f:real^3 -> real -> real^3) u t `));
DOWN;
REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [` w': real `;` v': real `]));
ANTS_TAC;
ASM_REWRITE_TAC[];
CONV_TAC VECTOR_ARITH;
STRIP_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, w} {u}  ` MP_TAC;
ASM_REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` u': real `;
EXISTS_TAC` v': real `;
EXISTS_TAC` w': real `;
ASM_REWRITE_TAC[];
CONV_TAC VECTOR_ARITH;
STRIP_TAC;
UNDISCH_TAC` &0 <= azim (vec 0) w (rho_node1 FF w) u `;
UNDISCH_TAC` azim (vec 0) w (rho_node1 FF w) u <=
      azim (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w) `;
PHA;
DOWN;
NHANH IN_AFF_GT_IMP_AZIMEQ2;
SIMP_TAC[];
SUBGOAL_THEN` interior_angle1 (vec 0) FF x'' = pi /\
              rho_node1 FF x'' IN aff {x'', v, w} /\
              ivs_rho_node1 FF x'' IN aff {x'', v, w} ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY];
ASM_REWRITE_TAC[];
UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
SUBGOAL_THEN` azim (vec 0) x'' (rho_node1 FF x'') (ivs_rho_node1 FF x'') =
              interior_angle1 (vec 0) FF x'' ` MP_TAC;
ASM_SIMP_TAC[];
DISCH_THEN (SUBST1_TAC o SYM);
NHANH Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT;
SIMP_TAC[];  
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC` x'', rho_node1 FF x'' `));
ANTS_TAC;
ASM_SIMP_TAC[];
ASM_REWRITE_TAC[];
UNDISCH_TAC` !v. v IN V
          ==> wedge_in_fan_ge  (v,rho_node1 FF v) E =
              wedge_ge  (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` x'': real^3 `));
ASM_REWRITE_TAC[VECTOR_ARITH` x - vec 0 = x `; SUBSET; IN_ELIM_THM];
STRIP_TAC;
ABBREV_TAC` e1 = x'' cross rho_node1 FF x'' `;
SUBGOAL_THEN` e1 dot v = &0 /\ e1 dot (w:real^3) = &0 ` MP_TAC;
UNDISCH_TAC` vec 0 IN conv0 {v, w:real^3} `;
REWRITE_TAC[Collect_geom.CONV0_SET2; IN_ELIM_THM];
STRIP_TAC;
MP_TAC (ISPEC` e1: real^3 ` DOT_RZERO);
ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL];
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
DOWN THEN DOWN;
UNDISCH_TAC` &0 < a' `;
UNDISCH_TAC` &0 < b' `;
REWRITE_TAC[REAL_ARITH` &0 <= a <=> a = &0 \/ &0 < a `];
MESON_TAC[REAL_LT_ADD; REAL_LT_MUL; REAL_ARITH` &0 < a ==> ~(a = &0) `; REAL_ARITH` &0 < a ==> ~( a + x * &0 = &0 \/ x * &0 + a = &0) `];
STRIP_TAC;
UNDISCH_TAC` !u. u IN V
          ==> ~(u = v)
          ==> ~(u = w)
          ==> u IN aff_gt {vec 0, v} {rho_node1 FF v} \/
              u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} `;
PHA THEN STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u:real^3 `));
SUBGOAL_THEN` rho_node1 FF v IN V /\ ivs_rho_node1 FF v IN V ` MP_TAC;
ASM_SIMP_TAC[];
SUBGOAL_THEN` ~ collinear { vec 0, v,  rho_node1 FF v } /\ ~ collinear {vec 0, v, ivs_rho_node1 FF v } ` MP_TAC;
ASM_SIMP_TAC[];
NHANH Fan.th3a;
NHANH AFF_GT_2_1;
DOWN THEN STRIP_TAC;
STRIP_TAC;
STRIP_TAC;
UNDISCH_TAC` u IN aff_gt {vec 0, v} {rho_node1 FF v} `;
ASM_REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
SUBGOAL_THEN` (!x. x IN ss
                   ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;


ASM_REWRITE_TAC[];
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v, v `));
ANTS_TAC;
EXPAND_TAC "ss";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` rho_node1 FF v `;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v}  `;
SIMP_TAC[INSERT_COMM];
STRIP_TAC;
UNDISCH_TAC` u = t2 % v + t3 % rho_node1 FF v `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_SIMP_TAC[];
EXISTS_TAC` t3: real `;
EXISTS_TAC` t2:real `;
ASM_REWRITE_TAC[];
EXPAND_TAC "u";
CONV_TAC VECTOR_ARITH;
REWRITE_TAC[];
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t  IN affine hull {vec 0, v, w, u } ` MP_TAC;
ASM_SIMP_TAC[];
FIRST_X_ASSUM (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3];
EXPAND_TAC "u";
REWRITE_TAC[VECTOR_ARITH` u % vec 0 + v % v' + w % (t2 % v' + t3 % ax)  = ( v  + w * t2 ) % v' + ( w * t3) % ax`];
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[VECTOR_ARITH` a + b = b + (a:real^N) `];
PHA THEN STRIP_TAC;
UNDISCH_TAC` (f:real^3 -> real -> real^3) u t = (w' * t3) % rho_node1 FF v + (v' + w' * t2) % v `;
ONCE_REWRITE_TAC[VECTOR_ARITH` a + b = b + (a:real^N) `];
FIRST_ASSUM NHANH;
SIMP_TAC[DOT_RADD; DOT_RMUL];
ASM_REWRITE_TAC[REAL_ARITH` a * &0 + x = x `];
STRIP_TAC;
SUBGOAL_THEN` &0 <= e1 dot rho_node1 FF v ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
MATCH_MP_TAC REAL_LE_MUL;
ASM_REWRITE_TAC[];
UNDISCH_TAC` &0 < w' * t3 `;
REAL_ARITH_TAC;  STRIP_TAC;
STRIP_TAC;
UNDISCH_TAC` u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} `;
ASM_REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];
REWRITE_TAC[VECTOR_ARITH` u % vec 0 + v % vv + w % (t2 % vv + t3 % vc) =
( v + w * t2 ) % vv + (w * t3 ) % vc `];
FIRST_X_ASSUM (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` (!x. x IN ss
                   ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v, v `));
ANTS_TAC;
EXPAND_TAC "ss";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` ivs_rho_node1 FF v `;
EXISTS_TAC` v: real^3 `;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[];
UNDISCH_TAC` ~collinear {vec 0, v, ivs_rho_node1 FF v} `;
SIMP_TAC[INSERT_COMM];
STRIP_TAC;
EXISTS_TAC` t3: real`;
EXISTS_TAC` t2: real `;
ASM_REWRITE_TAC[];
EXPAND_TAC "u";
CONV_TAC VECTOR_ARITH;
REWRITE_TAC[];
ONCE_REWRITE_TAC[VECTOR_ADD_SYM];
DISCH_THEN (ASSUME_TAC2 o (SPECL [` w' * t3: real `; ` v' + w' * t2: real`]));
ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_MUL_RZERO; REAL_ADD_LID];
UNDISCH_TAC` !x. x IN V ==> &0 <= e1 dot (x: real^3) `;
DISCH_THEN (ASSUME_TAC2 o (SPEC` ivs_rho_node1 FF v `));
MATCH_MP_TAC REAL_LE_MUL;
ASM_REWRITE_TAC[];
UNDISCH_TAC` &0 < w' * t3 `;
CONV_TAC REAL_ARITH;  
ASM_CASES_TAC` ~( x' = (u:real^3)) /\ ~( rho_node1 FF x' = u ) /\ ~( ivs_rho_node1 FF x' = u ) ` ;
DOWN THEN STRIP_TAC;
UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_SIMP_TAC[];
STRIP_TAC;
UNDISCH_TAC` !x. (x:real^3 # real^3) IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `;
DISCH_THEN (MP_TAC o (SPEC` x', rho_node1 FF x' `));
ANTS_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];
STRIP_TAC;
MATCH_MP_TAC SUBSET_TRANS;
EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `;
ASM_REWRITE_TAC[INSERT_SUBSET];
ASM_SIMP_TAC[];

STRIP_TAC; 
ASM_CASES_TAC` x' = u:real^3 `;
ASM_SIMP_TAC[];
SUBGOAL_THEN` rho_node1 FF u IN aff_ge {vec 0, v} {u} /\
              ivs_rho_node1 FF u IN aff_ge {vec 0, v} {u} ` ASSUME_TAC;
ASM_SIMP_TAC[];
SUBGOAL_THEN` ~collinear {vec 0, v, u:real^3} ` ASSUME_TAC;
ASM_SIMP_TAC[];
SUBGOAL_THEN` (f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t IN IV ` ASSUME_TAC;
EXPAND_TAC "IV";
REWRITE_TAC[IN_IMAGE];
EXISTS_TAC` ivs_rho_node1 FF u `;
ASM_SIMP_TAC[];
ABBREV_TAC` UU = {ITER n (rho_node1 IF) ( (f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t ) | n <= 2} `;
ABBREV_TAC` P = affine hull {vec 0, v, u:real^3} `;
ASSUME_TAC (ISPECL [` {vec 0, v:real^3 }`;` {u:real^3} `] AFF_GE_SUBSET_AFFINE_HULL);
SUBGOAL_THEN` plane  (P:real^3 -> bool) ` ASSUME_TAC;
REWRITE_TAC[plane];
EXISTS_TAC` vec 0: real^3 `;
EXISTS_TAC` v: real^3 `;
EXISTS_TAC` u: real^3 `;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` vec 0 IN (P:real^3 -> bool) ` ASSUME_TAC;
MP_TAC (
prove(` {vec 0, v, u:real^3} SUBSET affine hull {vec 0, v, u}  `,
REWRITE_TAC[HULL_SUBSET]));
UNDISCH_TAC` w = ITER i (rho_node1 FF ) v ` ;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w ` ;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[SUBSET];
DISCH_THEN MATCH_MP_TAC;
REWRITE_TAC[IN_INSERT];
SUBGOAL_THEN` UU SUBSET (P: real^3 -> bool) ` ASSUME_TAC;
EXPAND_TAC "UU";
REWRITE_TAC[SUBSET; IN_ELIM_THM];
GEN_TAC;
REWRITE_TAC[ARITH_RULE` n <= 2 <=> n = 0 \/ n = 1 \/ n = 2 `];
STRIP_TAC;
DOWN;
ASM_REWRITE_TAC[ITER];
STRIP_TAC;
UNDISCH_TAC` aff_ge {vec 0, v:real^3} {u} SUBSET affine hull ({vec 0, v} UNION {u}) `;
UNDISCH_TAC` w = ITER i (rho_node1 FF)  v `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` v = ITER j (rho_node1 FF)  w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
DISCH_THEN MATCH_MP_TAC;
ASM_REWRITE_TAC[];
DOWN;
DOWN;
SIMP_TAC[ITER1];
SUBGOAL_THEN`  rho_node1 IF ((f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t) = f (rho_node1 FF (ivs_rho_node1 FF u)) t` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_SIMP_TAC[];
SIMP_TAC[];
ASM_SIMP_TAC[];


SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[];
SIMP_TAC[];
UNDISCH_TAC` x'' = ITER n (rho_node1 IF) ((f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t) ` ;
DOWN THEN SIMP_TAC[];
REWRITE_TAC[Lvducxu.ITER12];
SUBGOAL_THEN` rho_node1 IF (f (ivs_rho_node1 FF u) (t:real)) = f (rho_node1 FF (ivs_rho_node1 FF u)) t ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_SIMP_TAC[];
SIMP_TAC[];
PHA THEN STRIP_TAC;
ASM_SIMP_TAC[];
UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) `;
UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
DISCH_THEN MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (
SPECL [` IE: (real^3 -> bool) -> bool `;` IV: real^3 -> bool `;` UU: real^3 ->
 bool `;` P: real^3  -> bool `;` 2 `;` IF: real^3 # real^3 -> bool `; `((f:real
 ^3 -> real -> real^3) (ivs_rho_node1 FF u) t) `] (GEN_ALL
 AZIM_PI_ITER_LOCAL_FAN));
FIRST_X_ASSUM (MP_TAC o (SPEC` 0 `));
ANTS_TAC;
ARITH_TAC;

UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);
REWRITE_TAC[ADD; ITER; ITER1; Lvducxu.ITER12];
SUBGOAL_THEN` rho_node1 IF (f (ivs_rho_node1 FF u) (t:real)) = f (rho_node1 FF (ivs_rho_node1 FF u)) t ` MP_TAC;
ASM_SIMP_TAC[];
SIMP_TAC[];
ASM_SIMP_TAC[];
NHANH (MESON[PI_POS]` x = pi ==> &0 < x `);
NHANH Local_lemmas1.AZIM_POS_IMP_SUM_2PI;
STRIP_TAC;
DOWN;
ASM_REWRITE_TAC[REAL_ARITH` a + x = &2 * a <=> x = a `];
SIMP_TAC[REAL_LE_REFL];
STRIP_TAC;



SUBGOAL_THEN` wedge_ge  (vec 0) (f u (t:real)) (rho_node1 FF u) (ivs_rho_node1 FF u) =
wedge_ge  (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) ` ASSUME_TAC;
DOWN;
SUBGOAL_THEN` interior_angle1 (vec 0) FF u = pi ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY];
SUBGOAL_THEN` azim (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) = pi ` MP_TAC;
DOWN;
ASM_SIMP_TAC[];
NHANH Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT;
SIMP_TAC[VECTOR_SUB_RZERO];
PHA THEN STRIP_TAC;
SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, rho_node1 FF u } ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ ;
ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET];
CONJ_TAC;
EXPAND_TAC "P";
MP_TAC (ISPECL [` affine: (real^3 -> bool) -> bool `;
` { vec 0, v, u:real^3} `] HULL_SUBSET);
REWRITE_TAC[SUBSET];
DISCH_THEN MATCH_MP_TAC;
REWRITE_TAC[IN_INSERT];
UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) `;
REWRITE_TAC[SUBSET;SET_RULE` {a,b} UNION {c} = {a,b,c} `];
ASM_REWRITE_TAC[];
DISCH_THEN MATCH_MP_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` f u (t:real) IN affine hull {vec 0, v, w, u:real^3} ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
DOWN;
ASM_REWRITE_TAC[];
SIMP_TAC[IN_ELIM_THM; AFFINE_HULL_3];
PHA THEN STRIP_TAC;
SUBGOAL_THEN` (!x. x IN ss
                   ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `));
ANTS_TAC;
EXPAND_TAC "ss";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` u: real^3 `;
EXISTS_TAC` rho_node1 FF u `;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[];
EXISTS_TAC` &1 `;
EXISTS_TAC` &0 `;
CONJ_TAC;
CONV_TAC VECTOR_ARITH;
REAL_ARITH_TAC;
REWRITE_TAC[];
DISCH_THEN (MP_TAC o (SPECL [` v': real `;` w': real `]));
ANTS_TAC;
ASM_REWRITE_TAC[];
CONV_TAC VECTOR_ARITH;
ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; CROSS_LADD; CROSS_LMUL; CROSS_REFL; VECTOR_ADD_RID; DOT_LMUL];
SIMP_TAC[REAL_LE_MUL_EQ];


ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `));
ANTS_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];
UNDISCH_TAC` !v. v IN V
          ==> wedge_in_fan_ge  (v,rho_node1 FF v) E =
              wedge_ge  (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `;
DISCH_THEN (ASSUME_TAC2 o (SPEC` u:real^3 `));
DOWN;
SIMP_TAC[];

STRIP_TAC;
MATCH_MP_TAC SUBSET_TRANS;
EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[INSERT_SUBSET];
SUBGOAL_THEN`  azim_in_fan (u, rho_node1 FF u) E <= pi /\ V SUBSET wedge_in_fan_ge   (u, rho_node1 FF u) E ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_SIMP_TAC[];
DOWN THEN STRIP_TAC;
DOWN;
UNDISCH_TAC` wedge_in_fan_ge  (u,rho_node1 FF u) E =
      wedge_ge  (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) `;
SIMP_TAC[];

SUBGOAL_THEN` (!x. (x :real^3 # real^3) IN ss
                   ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];

UNDISCH_TAC` w = ITER i (rho_node1 FF ) v ` ;
UNDISCH_TAC` v = ITER j (rho_node1 FF ) w ` ;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);
ASM_CASES_TAC` rho_node1 FF x' = u `;
ASM_SIMP_TAC[];
SUBGOAL_THEN` ~(rho_node1 FF (rho_node1 FF ( ivs_rho_node1 FF x')) = (ivs_rho_node1 FF x')) ` MP_TAC;
FIRST_ASSUM MATCH_MP_TAC;
ASM_SIMP_TAC[];

SUBGOAL_THEN` rho_node1 FF (ivs_rho_node1 FF x') = x' ` SUBST1_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, ivs_rho_node1 FF u }` MP_TAC;
MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ;
ASM_SIMP_TAC[];
ASSUME_TAC2 (ISPECL [` {vec 0, v:real^3} `;` {u:real^3} `] AFF_GE_SUBSET_AFFINE_HULL);
MP_TAC (ISPECL [` affine: (real^3 -> bool) -> bool `;` {vec 0, v, u:real^3} `] HULL_SUBSET);
SIMP_TAC[INSERT_SUBSET];
STRIP_TAC;
UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u: real^3}) `;
REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
DISCH_THEN MATCH_MP_TAC; 
ASM_SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;

SUBGOAL_THEN` ~ collinear {vec 0, u, ivs_rho_node1 FF u } ` ASSUME_TAC;
ASM_SIMP_TAC[];
FIRST_ASSUM (MP_TAC o (SPEC` u, ivs_rho_node1 FF u ` ));
ANTS_TAC;
EXPAND_TAC "ss"; 
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` u:real^3 `;
EXISTS_TAC` ivs_rho_node1 FF u `;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[];
EXISTS_TAC` &1 `;
EXISTS_TAC` &0 `;
CONJ_TAC;
CONV_TAC VECTOR_ARITH;
REAL_ARITH_TAC;
REWRITE_TAC[];
DISCH_THEN (ASSUME_TAC2 o (SPECL [` v': real `;` w': real `]));
DOWN THEN DOWN;
ONCE_REWRITE_TAC[SET_RULE` {a,b} = {b,a} `];
DOWN;
SUBGOAL_THEN` ivs_rho_node1 FF u = x' ` ASSUME_TAC;
EXPAND_TAC  "u";
ASM_SIMP_TAC[];
ASM_REWRITE_TAC[];
PHA THEN STRIP_TAC;
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, x'} {u:real^3} ` MP_TAC;
DOWN THEN DOWN;
NHANH Fan.th3a;
NHANH AFF_GT_2_1;
SIMP_TAC[IN_ELIM_THM];
STRIP_TAC;
STRIP_TAC;
EXISTS_TAC` u': real `;
EXISTS_TAC` w': real `;
EXISTS_TAC` v': real` ;
ASM_REWRITE_TAC[];
CONJ_TAC;
UNDISCH_TAC` u' + v' + w' = &1 `;
REAL_ARITH_TAC;
CONV_TAC VECTOR_ARITH;
NHANH IN_AFF_GT_IMP_AZIMEQ2;
REWRITE_TAC[GSYM Rogers.AZIM_EQ_SYM];
SIMP_TAC[wedge_ge];
STRIP_TAC;
UNDISCH_TAC` !x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC` x', rho_node1 FF x' `));
ANTS_TAC;
ASM_SIMP_TAC[];
DOWN THEN PHA;
ASM_SIMP_TAC[GSYM wedge_ge];
UNDISCH_TAC` !v. v IN V
          ==> azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) =
              interior_angle1 (vec 0) FF v `;
DISCH_THEN (ASSUME_TAC o GSYM);
ASM_SIMP_TAC[];
STRIP_TAC;

MATCH_MP_TAC SUBSET_TRANS;
EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `;
UNDISCH_TAC` (f: real^3 -> real -> real^3) u t = v' % u + w' % x' `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_SIMP_TAC[];
UNDISCH_TAC` rho_node1 FF x' = u `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_SIMP_TAC[INSERT_SUBSET];
SUBGOAL_THEN` (f: real^3 -> real -> real^3) u t IN
               wedge_ge  (vec 0) x' (rho_node1 FF x') (ivs_rho_node1 FF x') ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
DOWN;
SIMP_TAC[];

ASM_CASES_TAC` ivs_rho_node1 FF x' = u `;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` x' = rho_node1 FF u ` ASSUME_TAC;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];
UNDISCH_TAC`!x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `;
DISCH_THEN (MP_TAC o (SPEC` x', rho_node1 FF x' `));
ANTS_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];
UNDISCH_TAC` !v. v IN V
          ==> azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) =
              interior_angle1 (vec 0) FF v `;
DISCH_THEN (ASSUME_TAC2 o (SPEC` x': real^3 `));
FIRST_X_ASSUM (MP_TAC o SYM);
ASM_REWRITE_TAC[];
SIMP_TAC[];
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `));
ANTS_TAC;
EXPAND_TAC "ss";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` u: real^3 `;
EXISTS_TAC` rho_node1 FF u `;
ASM_SIMP_TAC[];



EXISTS_TAC` &1 `;
EXISTS_TAC` &0 `;
CONJ_TAC;
CONV_TAC VECTOR_ARITH;
REAL_ARITH_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, rho_node1 FF u } ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ;
ASM_SIMP_TAC[];
MP_TAC (ISPEC ` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
SIMP_TAC[INSERT_SUBSET];
ASM_SIMP_TAC[];
STRIP_TAC;
MP_TAC (ISPECL [` {vec 0, v:real^3} `;` {u: real^3} `] AFF_GE_SUBSET_AFFINE_HULL);
REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
DISCH_THEN MATCH_MP_TAC;
ASM_SIMP_TAC[];
SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
SUBGOAL_THEN` &0 < v' ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
EXISTS_TAC` w': real`;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ~ collinear {vec 0, u, rho_node1 FF u } ` MP_TAC;
ASM_SIMP_TAC[];
ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
NHANH Fan.th3a;
NHANH AFF_GT_2_1;
STRIP_TAC;
SUBGOAL_THEN` (f:real ^3 -> real -> real^3) u t IN aff_gt {vec 0, rho_node1 FF u } {u} ` MP_TAC;
ASM_REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` u': real `;
EXISTS_TAC` w': real `;
EXISTS_TAC` v': real `;
ASM_REWRITE_TAC[];
CONJ_TAC;
UNDISCH_TAC` u' + v' + w' = &1 `;
REAL_ARITH_TAC;
CONV_TAC VECTOR_ARITH;
NHANH IN_AFF_GT_IMP_AZIMEQ2;
SIMP_TAC[];
STRIP_TAC THEN STRIP_TAC;
MATCH_MP_TAC SUBSET_TRANS;
EXISTS_TAC` (f: real^3 -> real -> real^3) u t INSERT V `;
UNDISCH_TAC` (f: real^3 -> real -> real^3) u t = v' % u + w' % rho_node1 FF u `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[INSERT_SUBSET; wedge_ge];
ASM_SIMP_TAC[GSYM wedge_ge];
UNDISCH_TAC` !x'. x' IN V
           ==> (f: real^3 -> real -> real^3) u t IN
               wedge_ge  (vec 0) x' (rho_node1 FF x') (ivs_rho_node1 FF x') `;
DISCH_THEN (MP_TAC o (SPEC` rho_node1 FF u `));
ANTS_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[];
UNDISCH_TAC` ~(~(x' = u) /\ ~(rho_node1 FF x' = u) /\ ~(ivs_rho_node1 FF x' = u)) `;
ASM_REWRITE_TAC[]]);;

let MHAEYJN = 
prove_by_refinement(
`!a b V E FF f v w u.
     convex_local_fan (V,E,FF) /\
     lunar (v,w) V E /\
     deformation f V (a,b) /\
     interior_angle1 (vec 0) FF v < pi /\
     u IN V /\
     ~(u = v) /\
     ~(u = w) /\
     (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
     (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})
     ==> (?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> convex_local_fan
                       (IMAGE (\v. f v t) V,
                        IMAGE (IMAGE (\v. f v t)) E,
                        IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
                       lunar (v,w) (IMAGE (\v. f v t) V)
                       (IMAGE (IMAGE (\v. f v t)) E)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (GEN_ALL SUB_LUNAR_DEFORM_LEMMA) [`FF`;`a`;`b`;`u`;`v`;`w`;`V`;`f`;`E`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_REAL_INTERVAL]);
    ASM_SIMP_TAC[];
    TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_SIMP_TAC[Local_lemmas.CVX_LO_IMP_LO]);
    CONJ_TAC;
      MATCH_MP_TAC Local_lemmas.LOCAL_FAN_FINITE_V;
      BY(ASM_REWRITE_TAC[]);
    RULE_ASSUM_TAC(REWRITE_RULE[Localization.local_fan;Fan.FAN;LET_DEF;LET_END_DEF]);
    FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN FIRST_X_ASSUM_ST `UNIONS` MP_TAC THEN SET_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC MHAEYJN_CONVEX_LOCAL_FAN [`a`;`b`;`V`;`E`;`FF`;`f`;`v`;`w`;`u`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `if e < e' then e else e'` EXISTS_TAC;
  REPEAT WEAKER_STRIP_TAC;
  CONJ_TAC;
    BY(COND_CASES_TAC THEN ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  CONJ_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM MATCH_MP_TAC;
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)



end;;