(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Hypermap                                                    *)
(* Author: John Harrison                                                      *)
(* Date: 2012-09-16                                                           *)
(* ========================================================================== *)


(* ------------------------------------------------------------------------- *)
(* Some lemmas that should probably go in the core.                          *)
(* ------------------------------------------------------------------------- *)

module Deformation = struct

  open Fan;;
  open Local_lemmas1;;
  open Ckqowsa_4_points;;
  open Hales_tactic;;

let COMPACT_SPHERE_0 = 
prove
 (`!a. compact {x | norm x = a}`,

  ONCE_REWRITE_TAC[NORM_ARITH `norm x = norm(x - vec 0)`] THEN
  REWRITE_TAC[COMPACT_SPHERE]);;

let SEPARATE_CLOSED_CONES = 
prove
 (`!c d:real^N->bool.
        conic c /\ closed c /\ conic d /\ closed d /\ c INTER d SUBSET {vec 0}
        ==> ?e. &0 < e /\
                !x y. x IN c /\ y IN d ==> dist(x,y)
                      >= e * max (norm x) (norm y)`,

  SUBGOAL_THEN
   `!c d:real^N->bool.
        conic c /\ closed c /\ conic d /\ closed d /\ c INTER d SUBSET {vec 0}
        ==> ?e. &0 < e /\
                !x y. x IN c /\ y IN d ==> dist(x,y)
                      >= e * norm x`
  ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
    MP_TAC(ISPECL [`c INTER {x:real^N | norm x = &1}`; `d:real^N->bool`]
      SEPARATE_COMPACT_CLOSED) THEN
    ASM_SIMP_TAC[CLOSED_INTER_COMPACT; COMPACT_SPHERE_0] THEN ANTS_TAC THENL
     [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
       `c INTER d SUBSET {a} ==> ~(a IN s) ==> (c INTER s) INTER d = {}`)) THEN
      REWRITE_TAC[IN_ELIM_THM; NORM_0] THEN REAL_ARITH_TAC;
      MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `e:real` THEN
      REWRITE_TAC[IN_INTER; IN_ELIM_THM] THEN STRIP_TAC THEN
      ASM_REWRITE_TAC[] THEN
      MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
      ASM_CASES_TAC `x:real^N = vec 0` THEN
      ASM_REWRITE_TAC[DIST_POS_LE; REAL_MUL_RZERO; NORM_0] THEN
      FIRST_X_ASSUM(MP_TAC o SPECL
       [`inv(norm x) % x:real^N`; `inv(norm(x:real^N)) % y:real^N`]) THEN
      REWRITE_TAC[dist; NORM_MUL; GSYM VECTOR_SUB_LDISTRIB] THEN
      REWRITE_TAC[REAL_ARITH `abs x * a = a * abs x`] THEN
      REWRITE_TAC[REAL_ABS_INV; GSYM real_div; REAL_ABS_NORM] THEN
      ASM_SIMP_TAC[REAL_LE_RDIV_EQ; NORM_POS_LT] THEN
      DISCH_THEN MATCH_MP_TAC THEN
      ASM_SIMP_TAC[REAL_DIV_REFL; NORM_EQ_0] THEN
      RULE_ASSUM_TAC(REWRITE_RULE[conic]) THEN
      CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
      ASM_SIMP_TAC[REAL_LE_INV_EQ; NORM_POS_LE]];
    REPEAT STRIP_TAC THEN FIRST_X_ASSUM(fun th ->
      MP_TAC(SPECL [`c:real^N->bool`; `d:real^N->bool`] th) THEN
      MP_TAC(SPECL [`d:real^N->bool`; `c:real^N->bool`] th)) THEN
    ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[INTER_COMM] THEN
    ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; real_ge] THEN
    X_GEN_TAC `d:real` THEN STRIP_TAC THEN
    X_GEN_TAC `e:real` THEN STRIP_TAC THEN
    EXISTS_TAC `min d e:real` THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
    MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
    REWRITE_TAC[real_max] THEN COND_CASES_TAC THEN
    MATCH_MP_TAC REAL_LE_TRANS THENL
     [EXISTS_TAC `d * norm(y:real^N)` THEN ONCE_REWRITE_TAC[DIST_SYM];
      EXISTS_TAC `e * norm(x:real^N)`] THEN
    ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_LE_RMUL THEN NORM_ARITH_TAC]);;

(* ------------------------------------------------------------------------- *)
(* More Flyspeck-specific lemmas.                                            *)
(* ------------------------------------------------------------------------- *)

let AFF_GE_1_2_0 = 
prove
 (`!v w.
        ~(v = vec 0) /\ ~(w = vec 0)
        ==> aff_ge {vec 0} {v,w} = {a % v + b % w | &0 <= a /\ &0 <= b}`,

  SIMP_TAC[Fan.AFF_GE_1_2;
           SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
  REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
  ONCE_REWRITE_TAC[MESON[]
   `(?a b c. P b c /\ Q b c /\ R a b c /\ S b c) <=>
    (?b c. P b c /\ Q b c /\ S b c /\ ?a. R a b c)`] THEN
  REWRITE_TAC[REAL_ARITH `t + s:real = &1 <=> t = &1 - s`; EXISTS_REFL] THEN
  SET_TAC[]);;

let AFF_GE_1_1_0 = 
prove
 (`!v. ~(v = vec 0) ==> aff_ge {vec 0} {v} = {a % v | &0 <= a}`,

  REPEAT STRIP_TAC THEN
  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SET_RULE `{a} = {a,a}`] THEN
  ASM_SIMP_TAC[AFF_GE_1_2_0; GSYM VECTOR_ADD_RDISTRIB] THEN
  REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
  MESON_TAC[REAL_LE_ADD; REAL_ARITH
   `&0 <= a ==> &0 <= a / &2 /\ a / &2 + a / &2 = a`]);;

let CONIC_AFF_GE_0 = 
prove
 (`!s:real^N->bool. FINITE s /\ ~(vec 0 IN s) ==> conic(aff_ge {vec 0} s)`,

  REPEAT STRIP_TAC THEN ASM_SIMP_TAC[AFF_GE_0_N; conic] THEN
  REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN X_GEN_TAC `c:real` THEN
  DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN `u:real^N->real` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `\v. c * (u:real^N->real) v` THEN
  REWRITE_TAC[GSYM VECTOR_MUL_ASSOC; VSUM_LMUL] THEN
  ASM_MESON_TAC[REAL_LE_MUL]);;

(* ------------------------------------------------------------------------- *)
(* More economical characterization of "fan7"                                *)
(* ------------------------------------------------------------------------- *)

let GMLWKPK = 
prove
 (`!x:real^N V E.
        graph E
        ==> (fan7(x,V,E) <=>
             !e1 e2. e1 IN E UNION {{v} | v IN V} /\
                     e2 IN E UNION {{v} | v IN V}
                     ==> (e1 INTER e2 = {}
                          ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\
                         (!v. e1 INTER e2 = {v}
                              ==> aff_ge {x} e1 INTER aff_ge {x} e2 =
                                  aff_ge {x} {v}))`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[Fan.fan7] THEN EQ_TAC THENL
   [SIMP_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]; ALL_TAC] THEN
  MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e1:real^N->bool` THEN
  MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e2:real^N->bool` THEN
  MATCH_MP_TAC(TAUT `(p ==> q ==> r) ==> (q ==> p) ==> q ==> r`) THEN
  STRIP_TAC THEN DISCH_TAC THEN
  SUBGOAL_THEN `e1 = e2 \/ e1 INTER e2 = {} \/ (?v:real^N. e1 INTER e2 = {v})`
  MP_TAC THENL
   [ALL_TAC;
    STRIP_TAC THEN ASM_REWRITE_TAC[INTER_IDEMPOT] THEN
    ASM_MESON_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]] THEN
  SUBGOAL_THEN `?a b:real^N c d:real^N. e1 = {a,b} /\ e2 = {c,d}` MP_TAC THENL
   [ALL_TAC;
    DISCH_THEN(REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN SUBST_ALL_TAC)) THEN
    SET_TAC[]] THEN
  FIRST_ASSUM(CONJUNCTS_THEN MP_TAC) THEN
  REWRITE_TAC[IN_UNION; IN_ELIM_THM] THEN
  SUBGOAL_THEN `!e:real^N->bool. e IN E ==> ?v w. ~(v = w) /\ e = {v,w}`
  (LABEL_TAC "*") THENL
   [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [graph]) THEN
    MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
    MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[IN] THEN
    CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN REWRITE_TAC[];
    ASM_MESON_TAC[SET_RULE `{v,v} = {v}`]]);;

let GMLWKPK_ALT = 
prove
 (`!x:real^N V E.
        graph E /\ (!e. e IN E ==> ~(x IN e))
        ==> (fan7(x,V,E) <=>
             (!e1 e2. e1 IN E UNION {{v} | v IN V} /\
                      e2 IN E UNION {{v} | v IN V} /\
                      e1 INTER e2 = {}
                          ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\
             (!e1 e2 v. e1 IN E /\ e2 IN E /\ e1 INTER e2 = {v}
                        ==> aff_ge {x} e1 INTER aff_ge {x} e2 =
                            aff_ge {x} {v}))`,

  REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN
  EQ_TAC THEN SIMP_TAC[IN_UNION] THEN STRIP_TAC THEN
  MATCH_MP_TAC(MESON[]
   `(!x y. R x y ==> R y x) /\
    (!x y. P x /\ P y ==> R x y) /\
    (!x y. Q x /\ Q y ==> R x y) /\
    (!x y. P x /\ Q y ==> R x y)
    ==> !x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y`) THEN
  CONJ_TAC THENL [REWRITE_TAC[INTER_ACI]; ASM_SIMP_TAC[]] THEN CONJ_TAC THEN
  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THENL
   [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> a = c /\ b = c`] THEN SET_TAC[];
    X_GEN_TAC `e1:real^N->bool` THEN DISCH_TAC THEN X_GEN_TAC `v:real^N`] THEN
  SUBGOAL_THEN `(e1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
   [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`u:real^N`; `w:real^N`] THEN
  STRIP_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  SIMP_TAC[SET_RULE `{a,b} INTER {c} = {d} <=> d = c /\ (a = c \/ b = c)`] THEN
  REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
  GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]);;

let GMLWKPK_SIMPLE = 
prove
 (`!E V x:real^N.
        UNIONS E SUBSET V /\ graph E /\ fan6(x,V,E) /\
        (!e. e IN E ==> ~(x IN e))
        ==> (fan7 (x,V,E) <=>
             !e1 e2.
                e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} /\
                e1 INTER e2 = {}
                ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x})`,

  
let lemma = prove
   (`!x u v w:real^N.
      ~collinear{x,u,v} /\ ~collinear{x,v,w}
      ==> (~(aff_ge {x} {u,v} INTER aff_ge {x} {v,w} =
             aff_ge {x} {v}) <=>
           u IN aff_ge {x} {v,w} \/ w IN aff_ge {x} {u,v})`,
    REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `x:real^N` THEN
    REPEAT GEN_TAC THEN
    MAP_EVERY (fun t ->
      ASM_CASES_TAC t THENL
       [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC])
     [`u:real^N = v`; `w:real^N = v`;
      `u:real^N = vec 0`; `v:real^N = vec 0`; `w:real^N = vec 0`] THEN
    STRIP_TAC THEN EQ_TAC THENL
     [DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE
       `~(s INTER s' = t)
        ==> t SUBSET s /\ t SUBSET s' ==> t PSUBSET s INTER s'`)) THEN
      ANTS_TAC THENL
       [CONJ_TAC THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
        REWRITE_TAC[PSUBSET_ALT]] THEN
      DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
      ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; LEFT_IMP_EXISTS_THM] THEN
      REWRITE_TAC[IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN
      MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
      DISCH_TAC THEN DISCH_TAC THEN
      REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
      MAP_EVERY X_GEN_TAC [`c:real`; `d:real`] THEN STRIP_TAC THEN
      ASM_CASES_TAC `a = &0` THENL
       [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]; ALL_TAC] THEN
      ASM_CASES_TAC `d = &0` THENL
       [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID]; ALL_TAC] THEN
      DISCH_THEN(K ALL_TAC) THEN DISJ_CASES_TAC
       (REAL_ARITH `b <= c \/ c <= b`)
      THENL
       [FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH
         `a % u + b % v:real^N = c % v + d % w
          ==> a % u = (c - b) % v + d % w`)) THEN
        DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a):real^N->real^N`) THEN
        ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
        DISCH_THEN(K ALL_TAC) THEN DISJ1_TAC THEN
        REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
        MAP_EVERY EXISTS_TAC [`inv a * (c - b):real`; `inv a * d:real`] THEN
        ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE];
        FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH
         `a % u + b % v:real^N = c % v + d % w
          ==> d % w = (b - c) % v + a % u`)) THEN
        DISCH_THEN(MP_TAC o AP_TERM `(%) (inv d):real^N->real^N`) THEN
        ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
        DISCH_THEN(K ALL_TAC) THEN DISJ2_TAC THEN
        REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
        MAP_EVERY EXISTS_TAC [`inv d * a:real`; `inv d * (b - c):real`] THEN
        ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE] THEN
        REWRITE_TAC[VECTOR_ADD_SYM]];
      STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
       `(?x. x IN s /\ x IN t /\ ~(x IN u)) ==> ~(s INTER t = u)`)
      THENL
       [EXISTS_TAC `u:real^N` THEN ASM_REWRITE_TAC[] THEN
        ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN
        CONJ_TAC THENL
         [MAP_EVERY EXISTS_TAC [`&1`; `&0`] THEN
          REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC;
          DISCH_THEN(X_CHOOSE_THEN `a:real`
           (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
          UNDISCH_TAC `~collinear{vec 0:real^N,a % v,v}` THEN
          REWRITE_TAC[] THEN
          ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
          REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]];
        EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[] THEN
        ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN
        CONJ_TAC THENL
         [MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
          REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC;
          DISCH_THEN(X_CHOOSE_THEN `a:real`
           (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
          UNDISCH_TAC `~collinear{vec 0:real^N,v,a % v}` THEN
          REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]]]]) in
  REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN
  EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN
  REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(MESON[]
   `(!x y. R x y ==> R y x) /\
    (!x. Q x ==> !y. Q y ==> R x y) /\
    (!x. P x ==> (!y. Q y ==> R x y) /\ (!y. P y ==> R x y))
    ==> (!x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y)`) THEN
  CONJ_TAC THENL [SIMP_TAC[INTER_ACI]; ALL_TAC] THEN
  REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL
   [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> c = a /\ b = a`] THEN
    REWRITE_TAC[INTER_IDEMPOT];
    ALL_TAC] THEN
  X_GEN_TAC `ee1:real^N->bool` THEN DISCH_TAC THEN CONJ_TAC THENL
   [X_GEN_TAC `v:real^N` THEN DISCH_TAC THEN
    REWRITE_TAC[SET_RULE `s INTER {a} = {b} <=> b = a /\ a IN s`] THEN
    SIMP_TAC[IMP_CONJ; FORALL_UNWIND_THM2] THEN DISCH_TAC THEN
    REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
    MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
    ALL_TAC] THEN
  X_GEN_TAC `ee2:real^N->bool` THEN DISCH_TAC THEN
  SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
     [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
  SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL
   [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
  ONCE_REWRITE_TAC[SET_RULE
   `{a,b} INTER {c,d} = {v} <=>
    v = a /\ {a,b} INTER {c,d} = {v} \/
    v = b /\ {a,b} INTER {c,d} = {v}`] THEN
  REWRITE_TAC[TAUT
   `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN
  REWRITE_TAC[FORALL_AND_THM; FORALL_UNWIND_THM2] THEN
  MAP_EVERY UNDISCH_TAC [`{v1:real^N,w1} IN E`; `~(v1:real^N = w1)`] THEN
  MAP_EVERY (fun s -> SPEC_TAC(s,s))
   [`w1:real^N`; `v1:real^N`] THEN
  REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[]
   `(!v w. P v w ==> P w v) /\
    (!v w. R v w ==> Q w v) /\
    (!v w. P v w ==> R v w)
    ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN
  REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN
  MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
  ONCE_REWRITE_TAC[SET_RULE
   `{a,b} INTER {c,d} = {v} <=>
    v = c /\ {a,b} INTER {c,d} = {v} \/
    v = d /\ {a,b} INTER {c,d} = {v}`] THEN
  REWRITE_TAC[TAUT
   `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN
  MAP_EVERY UNDISCH_TAC [`{v2:real^N,w2} IN E`; `~(v2:real^N = w2)`] THEN
  MAP_EVERY (fun s -> SPEC_TAC(s,s)) [`w2:real^N`; `v2:real^N`] THEN
  REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[]
   `(!v w. P v w ==> P w v) /\
    (!v w. Q v w ==> R w v) /\
    (!v w. P v w ==> Q v w)
    ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN
  REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN
  MAP_EVERY X_GEN_TAC [`v':real^N`; `w:real^N`] THEN STRIP_TAC THEN
  ONCE_REWRITE_TAC[IMP_CONJ] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
  ASM_CASES_TAC `u:real^N = w` THENL [ASM SET_TAC[]; ALL_TAC] THEN
  DISCH_TAC THEN W(MP_TAC o PART_MATCH (rand o lhand o rand) lemma o goal_concl) THEN
  ANTS_TAC THENL
   [REWRITE_TAC[SET_RULE `{x,v,w} = {x} UNION {v,w}`] THEN
    ASM_MESON_TAC[fan6; INSERT_AC];
    ALL_TAC] THEN
  MATCH_MP_TAC(TAUT `~q ==> (~p <=> q) ==> p`) THEN
  REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THEN MATCH_MP_TAC(SET_RULE
   `aff_ge {x} {v} INTER aff_ge {x} s = {x} /\
    v IN aff_ge {x} {v} /\ ~(v = x)
    ==> ~(v IN aff_ge {x} s)`) THEN
  REPEAT CONJ_TAC THENL
   [FIRST_X_ASSUM MATCH_MP_TAC THEN
    ASM_REWRITE_TAC[IN_UNION] THEN
    CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN
    REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `u:real^N` THEN
    REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN
    FIRST_X_ASSUM MATCH_MP_TAC THEN
    REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{u:real^N,v}` THEN
    ASM SET_TAC[];
    SUBGOAL_THEN `DISJOINT {x:real^N} {u:real^N}` ASSUME_TAC THENL
     [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN
      ASM_MESON_TAC[IN_INSERT];
      ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN
      MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
      REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC];
    ASM_MESON_TAC[IN_INSERT];
    FIRST_X_ASSUM MATCH_MP_TAC THEN
    ASM_REWRITE_TAC[IN_UNION] THEN
    CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN
    REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `w:real^N` THEN
    REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN
    FIRST_X_ASSUM MATCH_MP_TAC THEN
    REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{v:real^N,w}` THEN
    ASM SET_TAC[];
    SUBGOAL_THEN `DISJOINT {x:real^N} {w:real^N}` ASSUME_TAC THENL
     [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN
      ASM_MESON_TAC[IN_INSERT];
      ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN
      MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
      REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC];
    ASM_MESON_TAC[IN_INSERT]]);;

(* ------------------------------------------------------------------------- *)
(* Two major lemmas in the proof.                                            *)
(* ------------------------------------------------------------------------- *)

let lemma_1 = 
prove
 (`!x:real^N e.
        ~(x = vec 0) /\ &0 < e
        ==> ?d. &0 < d /\
                !x'. dist(x,x') < d
                     ==> !z'. z' IN aff_ge {vec 0} {x'}
                              ==> ?z. z IN aff_ge {vec 0} {x} /\
                                      norm(z' - z) <= e * norm(z)`,

  REPEAT STRIP_TAC THEN
  EXISTS_TAC `min (e * norm(x:real^N)) (norm x)` THEN
  ASM_SIMP_TAC[REAL_LT_MUL; REAL_LT_MIN; NORM_POS_LT] THEN
  X_GEN_TAC `x':real^N` THEN
  STRIP_TAC THEN FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP
   (NORM_ARITH `dist(x,x') < norm(x:real^N) ==> ~(x' = vec 0)`)) THEN
  ASM_SIMP_TAC[AFF_GE_1_1_0; FORALL_IN_GSPEC; EXISTS_IN_GSPEC] THEN
  X_GEN_TAC `a:real` THEN DISCH_TAC THEN EXISTS_TAC `a:real` THEN
  ASM_REWRITE_TAC[GSYM VECTOR_SUB_LDISTRIB; NORM_MUL] THEN
  ONCE_REWRITE_TAC[REAL_ARITH `a * b * c:real = b * a * c`] THEN
  MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
  ASM_SIMP_TAC[ONCE_REWRITE_RULE[DIST_SYM] (GSYM dist); REAL_LT_IMP_LE]);;

let lemma_2 = 
prove
 (`!x y:real^N e.
        ~collinear{vec 0,x,y} /\ &0 < e
        ==> ?d. &0 < d /\
                !x' y'. dist(x,x') < d /\ dist(y,y') < d
                        ==> !z'. z' IN aff_ge {vec 0} {x',y'}
                                 ==> ?z. z IN aff_ge {vec 0} {x,y} /\
                                         norm(z' - z) <= e * norm(z)`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `x:real^N = vec 0` THENL
   [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
  ASM_CASES_TAC `y:real^N = vec 0` THENL
   [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
  ASM_CASES_TAC `x:real^N = y` THENL
   [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
  REPEAT STRIP_TAC THEN
  MP_TAC(ISPEC `(\a. a$1 % x + a$2 % y):real^2->real^N`
        LINEAR_INJECTIVE_BOUNDED_BELOW_POS) THEN
  SIMP_TAC[IMP_CONJ; LINEAR_INJECTIVE_0] THEN ANTS_TAC THENL
   [REWRITE_TAC[linear; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
    VECTOR_ARITH_TAC;
    REWRITE_TAC[FORALL_VECTOR_2; VECTOR_2]] THEN
  ANTS_TAC THENL
   [MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
    GEN_REWRITE_TAC RAND_CONV [CART_EQ] THEN
    REWRITE_TAC[FORALL_2; VECTOR_2; VEC_COMPONENT; DIMINDEX_2] THEN
    ASM_CASES_TAC `a = &0` THEN
    ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_EQ_0] THEN
    ASM_CASES_TAC `b = &0` THEN
    ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_EQ_0] THEN
    DISCH_THEN(MP_TAC o MATCH_MP (VECTOR_ARITH
     `a + b:real^N = vec 0 ==> b = --a`)) THEN
    DISCH_THEN(MP_TAC o AP_TERM `(%) (inv b) :real^N->real^N`) THEN
    ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_MUL_LID; REAL_MUL_LINV] THEN
    DISCH_TAC THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
     [COLLINEAR_LEMMA]) THEN
    ASM_REWRITE_TAC[VECTOR_MUL_RNEG; VECTOR_MUL_ASSOC] THEN
    REWRITE_TAC[GSYM VECTOR_MUL_LNEG] THEN MESON_TAC[];
    DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC)] THEN
  EXISTS_TAC `min (e * B / &2) (min (norm(x:real^N)) (norm(y:real^N)))` THEN
  ASM_SIMP_TAC[REAL_LT_MUL; REAL_HALF; REAL_LT_MIN; NORM_POS_LT] THEN
  MAP_EVERY X_GEN_TAC [`x':real^N`; `y':real^N`] THEN
  REPEAT(STRIP_TAC THEN FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP
   (NORM_ARITH `dist(x,x') < norm(x:real^N) ==> ~(x' = vec 0)`))) THEN
  ASM_SIMP_TAC[AFF_GE_1_2_0; FORALL_IN_GSPEC; EXISTS_IN_GSPEC] THEN
  MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THEN
  MAP_EVERY EXISTS_TAC [`a:real`; `b:real`] THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC(NORM_ARITH
   `norm(x' - x:real^N) <= e / &2 /\ norm(y' - y) <= e / &2
    ==> norm((x' + y') - (x + y)) <= e`) THEN
  REWRITE_TAC[GSYM VECTOR_SUB_LDISTRIB; NORM_MUL] THEN CONJ_TAC THEN
  MATCH_MP_TAC REAL_LE_TRANS THENL
   [EXISTS_TAC `abs a * e * B / &2`; EXISTS_TAC `abs b * e * B / &2`] THEN
  ASM_SIMP_TAC[REAL_LE_LMUL; REAL_LT_IMP_LE; REAL_ABS_POS;
               ONCE_REWRITE_RULE[DIST_SYM] (GSYM dist);
               REAL_ARITH `a * x / &2 <= y / &2 <=> a * x <= y`] THEN
  REWRITE_TAC[REAL_ARITH `a * e * B / &2 <= (e * n) / &2 <=>
                          e * a * B <= e * n`] THEN
  ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC `norm(vector[a;b]:real^2) * B` THEN
  ASM_SIMP_TAC[REAL_LE_RMUL_EQ] THENL
   [MP_TAC(ISPECL [`vector[a;b]:real^2`; `1`] COMPONENT_LE_NORM);
    MP_TAC(ISPECL [`vector[a;b]:real^2`; `2`] COMPONENT_LE_NORM)] THEN
  REWRITE_TAC[VECTOR_2; DIMINDEX_2; ARITH]);;

(* ------------------------------------------------------------------------- *)
(* Convenient lemmas for choosing minima.                                    *)
(* ------------------------------------------------------------------------- *)

let MINIMIZE_OVER_MEMBERS = 
prove
 (`!P s:A->bool.
        FINITE s /\
        (!x. x IN s
             ==> ?e. &0 < e /\ !t. abs(t) < e ==> P x t)
        ==> ?e. &0 < e /\ !t. abs t < e ==> !x. x IN s ==> P x t`,

  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  ASM_CASES_TAC `s:A->bool = {}` THENL
   [ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN MESON_TAC[REAL_LT_01]; ALL_TAC] THEN
  GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [RIGHT_IMP_EXISTS_THM] THEN
  REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
  X_GEN_TAC `dd:A->real` THEN DISCH_TAC THEN
  EXISTS_TAC `inf(IMAGE (dd:A->real) s)` THEN
  ASM_SIMP_TAC[REAL_LT_INF_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
  ASM_SIMP_TAC[FORALL_IN_IMAGE]);;

let MINIMIZE_OVER_2 = 
prove
 (`!P Q. (?e. &0 < e /\ !t. abs(t) < e ==> P t) /\
         (?e. &0 < e /\ !t. abs(t) < e ==> Q t)
         ==> ?e. &0 < e /\ !t. abs(t) < e ==> P t /\ Q t`,

  REPEAT GEN_TAC THEN DISCH_THEN
   (CONJUNCTS_THEN2 (X_CHOOSE_TAC `d:real`) (X_CHOOSE_TAC `e:real`)) THEN
  EXISTS_TAC `min d e:real` THEN
  ASM_SIMP_TAC[REAL_MIN_LT; REAL_LT_MIN]);;

let MINIMIZE_OVER_STRONGER = 
prove
 (`!P Q. (!t. P t ==> Q t) /\ (?e. &0 < e /\ !t. abs(t) < e ==> P t)
         ==> ?e. &0 < e /\ !t. abs(t) < e ==> Q t`,

  MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* The main theorem.                                                         *)
(* ------------------------------------------------------------------------- *)

let deformation = new_definition
 `deformation ff V (a,b) <=> (&0) IN real_interval (a,b) /\
  (!v r. v IN V /\ r IN real_interval (a,b) ==> (ff v) continuous atreal r) /\
  (!v. v IN V ==> ff v (&0) = v )`;;

let FAN7_SMALL_DEFORMATION = 
prove
 (`!V:real^N->bool E a b phii.
    deformation phii V (a,b) /\ FAN (vec 0,V,E)
    ==> ?e. &0 < e /\
            !t. --e < t /\ t < e
                ==> fan7
                    (vec 0,
                     IMAGE (\v. phii v t) V,
                     IMAGE (IMAGE (\v. phii v t)) E)`,

  
let lemma = prove
   (`closed {z | collinear {vec 0:real^N,fstcart z,sndcart z}}`,
    REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQUAL] THEN
    ONCE_REWRITE_TAC[SET_RULE `{x | P x} = {x | x IN (:real^N) /\ P x}`] THEN
    ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
    REWRITE_TAC[GSYM LIFT_EQ; LIFT_NUM] THEN
    MATCH_MP_TAC CONTINUOUS_CLOSED_PREIMAGE_CONSTANT THEN
    REWRITE_TAC[CLOSED_UNIV; LIFT_SUB] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
    CONJ_TAC THENL
     [REWRITE_TAC[GSYM NORM_LIFT] THEN
      MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE THEN
      MATCH_MP_TAC CONTINUOUS_ON_LIFT_DOT2;
      REWRITE_TAC[LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
      REWRITE_TAC[o_DEF] THEN CONJ_TAC THEN
      MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE] THEN
    SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_FSTCART; LINEAR_SNDCART]) in
  REWRITE_TAC[deformation; FAN] THEN REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `FINITE(V:real^N->bool) /\ ~(V = {})` STRIP_ASSUME_TAC THENL
   [ASM_MESON_TAC[fan1; SUBSET_EMPTY]; ALL_TAC] THEN
  SUBGOAL_THEN `!e. e IN E ==> ~((vec 0:real^N) IN e)` ASSUME_TAC THENL
   [RULE_ASSUM_TAC(REWRITE_RULE[fan2]) THEN ASM SET_TAC[]; ALL_TAC] THEN
  SUBGOAL_THEN `FINITE(E:(real^N->bool)->bool)` ASSUME_TAC THENL
   [MATCH_MP_TAC FINITE_SUBSET THEN
    EXISTS_TAC `IMAGE (\(v:real^N,w). {v,w}) (V CROSS V)` THEN
    ASM_SIMP_TAC[FINITE_IMAGE; FINITE_CROSS] THEN
    REWRITE_TAC[SUBSET] THEN X_GEN_TAC `ee:real^N->bool` THEN DISCH_TAC THEN
    SUBGOAL_THEN `(ee:real^N->bool) HAS_SIZE 2` MP_TAC THENL
     [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
    REWRITE_TAC[IN_IMAGE; EXISTS_PAIR_THM; IN_CROSS] THEN
    REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN ASM SET_TAC[];
    ALL_TAC] THEN
  UNDISCH_TAC `fan7(vec 0:real^N,V,E)` THEN
  ASM_SIMP_TAC[GMLWKPK_SIMPLE] THEN DISCH_THEN(LABEL_TAC "0") THEN
  SUBGOAL_THEN
   `!e. &0 < e
        ==> ?d. &0 < d /\
                !v:real^N t. v IN V /\ abs(t) < d ==> norm(phii v t - v) < e`
  MP_TAC THENL
   [X_GEN_TAC `e:real` THEN DISCH_TAC THEN ONCE_REWRITE_TAC[MESON[]
     `(!v t. P v /\ Q t ==> R v t) <=> (!t. Q t ==> !v. P v ==> R v t)`] THEN
    MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN ASM_REWRITE_TAC[] THEN
    X_GEN_TAC `v:real^N` THEN DISCH_TAC THEN
    FIRST_X_ASSUM(MP_TAC o ISPECL [`v:real^N`; `&0:real`]) THEN
    REWRITE_TAC[continuous_atreal] THEN ASM_SIMP_TAC[] THEN
    REWRITE_TAC[dist; REAL_SUB_RZERO] THEN ASM_MESON_TAC[];
    GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
    REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
    REWRITE_TAC[TAUT `p ==> q /\ r <=> (p ==> q) /\ (p ==> r)`] THEN
    REWRITE_TAC[FORALL_AND_THM; RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
    X_GEN_TAC `dd:real->real` THEN STRIP_TAC] THEN
  SUBGOAL_THEN
   `?e1. &0 < e1 /\
         !t. abs(t) < e1
             ==> graph (IMAGE (IMAGE (\v. (phii:real^N->real->real^N) v t)) E)`
  STRIP_ASSUME_TAC THENL
   [ASM_REWRITE_TAC[Fan.GRAPH; FORALL_IN_IMAGE] THEN
    MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN ASM_REWRITE_TAC[] THEN
    X_GEN_TAC `ee:real^N->bool` THEN DISCH_TAC THEN
    SUBGOAL_THEN `(ee:real^N->bool) HAS_SIZE 2` MP_TAC THENL
     [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`v:real^N`; `w:real^N`] THEN STRIP_TAC THEN
    SUBGOAL_THEN `(v:real^N) IN V /\ w IN V` STRIP_ASSUME_TAC THENL
     [ASM SET_TAC[]; ALL_TAC] THEN
    ASM_REWRITE_TAC[IMAGE_CLAUSES] THEN
    EXISTS_TAC `dd(norm(v - w:real^N) / &2):real` THEN
    ASM_SIMP_TAC[REAL_HALF; VECTOR_SUB_EQ; NORM_POS_LT] THEN
    REWRITE_TAC[Local_lemmas1.SET2_HAS_SIZE2] THEN
    GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC(NORM_ARITH
     `norm(phii v t - v) < norm(v - w) / &2 /\
      norm(phii w t - w) < norm(v - w) / &2
      ==> ~(phii v t = phii w t)`) THEN
    ASM_SIMP_TAC[REAL_HALF; VECTOR_SUB_EQ; NORM_POS_LT];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `?e2. &0 < e2 /\
         !t. abs(t) < e2
             ==> !e. e IN IMAGE (IMAGE (\v. (phii:real^N->real->real^N) v t)) E
                     ==> ~((vec 0) IN e)`
  STRIP_ASSUME_TAC THENL
   [REWRITE_TAC[FORALL_IN_IMAGE] THEN MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN
    ASM_REWRITE_TAC[] THEN X_GEN_TAC `ee:real^N->bool` THEN DISCH_TAC THEN
    SUBGOAL_THEN `(ee:real^N->bool) HAS_SIZE 2` MP_TAC THENL
     [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`v:real^N`; `w:real^N`] THEN STRIP_TAC THEN
    SUBGOAL_THEN `(v:real^N) IN V /\ w IN V` STRIP_ASSUME_TAC THENL
     [ASM SET_TAC[]; ALL_TAC] THEN
    SUBGOAL_THEN `~(v:real^N = vec 0) /\ ~(w:real^N = vec 0)`
    STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[fan2]; ALL_TAC] THEN
    EXISTS_TAC `dd(min (norm(v:real^N)) (norm(w:real^N))):real` THEN
    ASM_SIMP_TAC[REAL_HALF; VECTOR_SUB_EQ; NORM_POS_LT; REAL_LT_MIN] THEN
    REWRITE_TAC[IMAGE_CLAUSES; IN_INSERT; DE_MORGAN_THM; NOT_IN_EMPTY] THEN
    GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC(NORM_ARITH
     `norm(phii v t - v) < min (norm v) (norm w) /\
      norm(phii w t - w) < min (norm v) (norm w)
      ==> ~(vec 0 = phii v t) /\ ~(vec 0 = phii w t)`) THEN
    ASM_SIMP_TAC[REAL_HALF; VECTOR_SUB_EQ; NORM_POS_LT; REAL_LT_MIN];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `?e3. &0 < e3 /\
         !t. abs(t) < e3
             ==> !e1 e2.
                   e1 IN
                   IMAGE (IMAGE (\v. (phii:real^N->real->real^N) v t)) E UNION
                   {{v} | v IN IMAGE (\v. phii v t) V} /\
                   e2 IN
                   IMAGE (IMAGE (\v. phii v t)) E UNION
                   {{v} | v IN IMAGE (\v. phii v t) V} /\
                   e1 INTER e2 = {}
                   ==> aff_ge {vec 0} e1 INTER aff_ge {vec 0} e2 = {vec 0}`
  STRIP_ASSUME_TAC THENL
   [REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
    REWRITE_TAC[SET_RULE
     `x IN s UNION t ==> P x <=> (x IN s ==> P x) /\ (x IN t ==> P x)`] THEN
    REWRITE_TAC[FORALL_AND_THM; FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
    MATCH_MP_TAC MINIMIZE_OVER_2 THEN
    CONJ_TAC THEN MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN
    ASM_REWRITE_TAC[] THENL
     [X_GEN_TAC `ee1:real^N->bool`; X_GEN_TAC `v1:real^N`] THEN
    (DISCH_TAC THEN MATCH_MP_TAC MINIMIZE_OVER_2 THEN CONJ_TAC THEN
     MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN ASM_REWRITE_TAC[] THENL
      [X_GEN_TAC `ee2:real^N->bool`; X_GEN_TAC `v2:real^N`]) THEN
    DISCH_TAC THENL
     [SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
       [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
      REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
      MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN
      DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
      SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL
       [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
      REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
      MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN
      DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
      ASM_CASES_TAC `{v1:real^N,w1} INTER {v2,w2} = {}` THENL
       [ALL_TAC;
        EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN ASM SET_TAC[]] THEN
      SUBGOAL_THEN `~collinear{vec 0:real^N,v1,w1} /\
                    ~collinear{vec 0:real^N,v2,w2}`
      MP_TAC THENL
       [ASM_MESON_TAC[fan6; SET_RULE `{a} UNION {b,c} = {a,b,c}`];
        ALL_TAC] THEN
      MAP_EVERY (fun t -> ASM_CASES_TAC t THENL
       [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
       [`v1:real^N = vec 0`; `w1:real^N = vec 0`;
        `v2:real^N = vec 0`; `w2:real^N = vec 0`] THEN
      STRIP_TAC THEN
      MP_TAC(ISPECL
       [`aff_ge {vec 0:real^N} {v1,w1}`;
        `aff_ge {vec 0:real^N} {v2,w2}`] SEPARATE_CLOSED_CONES) THEN
      ANTS_TAC THENL
       [SIMP_TAC[CLOSED_AFF_GE; FINITE_INSERT; FINITE_EMPTY] THEN
        ASM_SIMP_TAC[IN_UNION; SUBSET_REFL] THEN
        CONJ_TAC THEN MATCH_MP_TAC CONIC_AFF_GE_0 THEN
        REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ASM SET_TAC[];
        ALL_TAC] THEN
      SUBGOAL_THEN `(v1:real^N) IN V /\ v2 IN V /\ w1 IN V /\ w2 IN V`
      STRIP_ASSUME_TAC THENL
       [REPEAT CONJ_TAC THEN
        FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
        REWRITE_TAC[IN_UNIONS] THEN ASM_MESON_TAC[IN_INSERT];
        ALL_TAC] THEN
      DISCH_THEN(X_CHOOSE_THEN `d:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
      MP_TAC(ISPECL [`v1:real^N`; `w1:real^N`; `d / &3`] lemma_2) THEN
      ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
      DISCH_THEN(X_CHOOSE_THEN `d1:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
      MP_TAC(ISPECL [`v2:real^N`; `w2:real^N`; `d / &3`] lemma_2) THEN
      ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
      DISCH_THEN(X_CHOOSE_THEN `d2:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
      EXISTS_TAC `(dd:real->real) ((min d1 d2) / &3)` THEN
      ASM_SIMP_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`; REAL_LT_MIN] THEN
      X_GEN_TAC `t:real` THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
      REWRITE_TAC[IMAGE_CLAUSES] THEN MATCH_MP_TAC(SET_RULE
       `(v IN s /\ v IN t /\ !x. x IN s INTER t ==> x = v)
        ==> s INTER t = {v}`) THEN
      REWRITE_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; IN_INTER] THEN
      X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
      REMOVE_THEN "1" (MP_TAC o SPECL
       [`(phii:real^N->real->real^N) v1 t`;
        `(phii:real^N->real->real^N) w1 t`]) THEN
      ANTS_TAC THENL
       [CONJ_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN
        EXISTS_TAC `min d1 d2 / &3` THEN
        (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
        REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
        ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
        DISCH_THEN(X_CHOOSE_THEN `x1:real^N` STRIP_ASSUME_TAC)] THEN
      REMOVE_THEN "2" (MP_TAC o SPECL
       [`(phii:real^N->real->real^N) v2 t`;
        `(phii:real^N->real->real^N) w2 t`]) THEN
      ANTS_TAC THENL
       [CONJ_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN
        EXISTS_TAC `min d1 d2 / &3` THEN
        (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
        REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
        ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
        DISCH_THEN(X_CHOOSE_THEN `x2:real^N` STRIP_ASSUME_TAC)];

      SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
       [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
      REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
      MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN
      DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
      ASM_CASES_TAC `{v1:real^N,w1} INTER {v2} = {}` THENL
       [ALL_TAC;
        EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN ASM SET_TAC[]] THEN
      SUBGOAL_THEN `~collinear{vec 0:real^N,v1,w1}`
      MP_TAC THENL
       [ASM_MESON_TAC[fan6; SET_RULE `{a} UNION {b,c} = {a,b,c}`];
        ALL_TAC] THEN
      MAP_EVERY (fun t -> ASM_CASES_TAC t THENL
       [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
       [`v1:real^N = vec 0`; `w1:real^N = vec 0`] THEN
      STRIP_TAC THEN
      SUBGOAL_THEN `~(v2:real^N = vec 0)` ASSUME_TAC THENL
       [ASM_MESON_TAC[fan2]; ALL_TAC] THEN
      MP_TAC(ISPECL
       [`aff_ge {vec 0:real^N} {v1,w1}`;
        `aff_ge {vec 0:real^N} {v2}`] SEPARATE_CLOSED_CONES) THEN
      ANTS_TAC THENL
       [SIMP_TAC[CLOSED_AFF_GE; FINITE_INSERT; FINITE_EMPTY] THEN
        REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
         [CONJ_TAC THEN MATCH_MP_TAC CONIC_AFF_GE_0 THEN
          REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ASM SET_TAC[];
          MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]];
        ALL_TAC] THEN
      SUBGOAL_THEN `(v1:real^N) IN V /\ w1 IN V`
      STRIP_ASSUME_TAC THENL
       [REPEAT CONJ_TAC THEN
        FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
        REWRITE_TAC[IN_UNIONS] THEN ASM_MESON_TAC[IN_INSERT];
        ALL_TAC] THEN
      DISCH_THEN(X_CHOOSE_THEN `d:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
      MP_TAC(ISPECL [`v1:real^N`; `w1:real^N`; `d / &3`] lemma_2) THEN
      ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
      DISCH_THEN(X_CHOOSE_THEN `d1:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
      MP_TAC(ISPECL [`v2:real^N`; `d / &3`] lemma_1) THEN
      ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
      DISCH_THEN(X_CHOOSE_THEN `d2:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
      EXISTS_TAC `(dd:real->real) ((min d1 d2) / &3)` THEN
      ASM_SIMP_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`; REAL_LT_MIN] THEN
      X_GEN_TAC `t:real` THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
      REWRITE_TAC[IMAGE_CLAUSES] THEN MATCH_MP_TAC(SET_RULE
       `(v IN s /\ v IN t /\ !x. x IN s INTER t ==> x = v)
        ==> s INTER t = {v}`) THEN
      REWRITE_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; IN_INTER] THEN
      CONJ_TAC THENL
       [MESON_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; INSERT_AC];
        ALL_TAC] THEN
      X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
      REMOVE_THEN "1" (MP_TAC o SPECL
       [`(phii:real^N->real->real^N) v1 t`;
        `(phii:real^N->real->real^N) w1 t`]) THEN
      ANTS_TAC THENL
       [CONJ_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN
        EXISTS_TAC `min d1 d2 / &3` THEN
        (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
        REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
        ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
        DISCH_THEN(X_CHOOSE_THEN `x1:real^N` STRIP_ASSUME_TAC)] THEN
      REMOVE_THEN "2" (MP_TAC o SPEC `(phii:real^N->real->real^N) v2 t`) THEN
      ANTS_TAC THENL
       [MATCH_MP_TAC REAL_LT_TRANS THEN
        EXISTS_TAC `min d1 d2 / &3` THEN
        (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
        REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
        ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
        DISCH_THEN(X_CHOOSE_THEN `x2:real^N` STRIP_ASSUME_TAC)];

      SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL
       [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
      REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
      MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN
      DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
      ASM_CASES_TAC `{v1} INTER {v2:real^N,w2} = {}` THENL
       [ALL_TAC;
        EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN ASM SET_TAC[]] THEN
      SUBGOAL_THEN `~collinear{vec 0:real^N,v2,w2}`
      MP_TAC THENL
       [ASM_MESON_TAC[fan6; SET_RULE `{a} UNION {b,c} = {a,b,c}`];
        ALL_TAC] THEN
      MAP_EVERY (fun t -> ASM_CASES_TAC t THENL
       [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
       [`v2:real^N = vec 0`; `w2:real^N = vec 0`] THEN
      STRIP_TAC THEN
      SUBGOAL_THEN `~(v1:real^N = vec 0)` ASSUME_TAC THENL
       [ASM_MESON_TAC[fan2]; ALL_TAC] THEN
      MP_TAC(ISPECL
       [`aff_ge {vec 0:real^N} {v1}`;
        `aff_ge {vec 0:real^N} {v2,w2}`] SEPARATE_CLOSED_CONES) THEN
      ANTS_TAC THENL
       [SIMP_TAC[CLOSED_AFF_GE; FINITE_INSERT; FINITE_EMPTY] THEN
        REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
         [CONJ_TAC THEN MATCH_MP_TAC CONIC_AFF_GE_0 THEN
          REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ASM SET_TAC[];
          MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]];
        ALL_TAC] THEN
      SUBGOAL_THEN `(v2:real^N) IN V /\ w2 IN V`
      STRIP_ASSUME_TAC THENL
       [REPEAT CONJ_TAC THEN
        FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
        REWRITE_TAC[IN_UNIONS] THEN ASM_MESON_TAC[IN_INSERT];
        ALL_TAC] THEN
      DISCH_THEN(X_CHOOSE_THEN `d:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
      MP_TAC(ISPECL [`v2:real^N`; `w2:real^N`; `d / &3`] lemma_2) THEN
      ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
      DISCH_THEN(X_CHOOSE_THEN `d2:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
      MP_TAC(ISPECL [`v1:real^N`; `d / &3`] lemma_1) THEN
      ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
      DISCH_THEN(X_CHOOSE_THEN `d1:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
      EXISTS_TAC `(dd:real->real) ((min d1 d2) / &3)` THEN
      ASM_SIMP_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`; REAL_LT_MIN] THEN
      X_GEN_TAC `t:real` THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
      REWRITE_TAC[IMAGE_CLAUSES] THEN MATCH_MP_TAC(SET_RULE
       `(v IN s /\ v IN t /\ !x. x IN s INTER t ==> x = v)
        ==> s INTER t = {v}`) THEN
      REWRITE_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; IN_INTER] THEN
      CONJ_TAC THENL
       [MESON_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; INSERT_AC];
        ALL_TAC] THEN
      X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
      REMOVE_THEN "1" (MP_TAC o SPECL
       [`(phii:real^N->real->real^N) v2 t`;
        `(phii:real^N->real->real^N) w2 t`]) THEN
      ANTS_TAC THENL
       [CONJ_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN
        EXISTS_TAC `min d1 d2 / &3` THEN
        (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
        REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
        ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
        DISCH_THEN(X_CHOOSE_THEN `x1:real^N` STRIP_ASSUME_TAC)] THEN
      REMOVE_THEN "2" (MP_TAC o SPEC `(phii:real^N->real->real^N) v1 t`) THEN
      ANTS_TAC THENL
       [MATCH_MP_TAC REAL_LT_TRANS THEN
        EXISTS_TAC `min d1 d2 / &3` THEN
        (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
        REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
        ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
        DISCH_THEN(X_CHOOSE_THEN `x2:real^N` STRIP_ASSUME_TAC)];

      ASM_CASES_TAC `{v1:real^N} INTER {v2} = {}` THENL
       [ALL_TAC;
        EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN ASM SET_TAC[]] THEN
      SUBGOAL_THEN `~(v1:real^N = vec 0) /\ ~(v2:real^N = vec 0)`
      STRIP_ASSUME_TAC THENL
       [ASM_MESON_TAC[fan2]; ALL_TAC] THEN
      MP_TAC(ISPECL
       [`aff_ge {vec 0:real^N} {v1}`;
        `aff_ge {vec 0:real^N} {v2}`] SEPARATE_CLOSED_CONES) THEN
      ANTS_TAC THENL
       [SIMP_TAC[CLOSED_AFF_GE; FINITE_INSERT; FINITE_EMPTY] THEN
        REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
         [CONJ_TAC THEN MATCH_MP_TAC CONIC_AFF_GE_0 THEN
          REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ASM SET_TAC[];
          MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]];
        ALL_TAC] THEN
      DISCH_THEN(X_CHOOSE_THEN `d:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
      MP_TAC(ISPECL [`v1:real^N`; `d / &3`] lemma_1) THEN
      ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
      DISCH_THEN(X_CHOOSE_THEN `d1:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
      MP_TAC(ISPECL [`v2:real^N`; `d / &3`] lemma_1) THEN
      ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
      DISCH_THEN(X_CHOOSE_THEN `d2:real`
       (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
      EXISTS_TAC `(dd:real->real) ((min d1 d2) / &3)` THEN
      ASM_SIMP_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`; REAL_LT_MIN] THEN
      X_GEN_TAC `t:real` THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
      REWRITE_TAC[IMAGE_CLAUSES] THEN MATCH_MP_TAC(SET_RULE
       `(v IN s /\ v IN t /\ !x. x IN s INTER t ==> x = v)
        ==> s INTER t = {v}`) THEN
      REWRITE_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; IN_INTER] THEN
      REPEAT(CONJ_TAC THENL
       [MESON_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; INSERT_AC];
        ALL_TAC]) THEN
      X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
      REMOVE_THEN "1" (MP_TAC o SPEC `(phii:real^N->real->real^N) v1 t`) THEN
      ANTS_TAC THENL
       [MATCH_MP_TAC REAL_LT_TRANS THEN
        EXISTS_TAC `min d1 d2 / &3` THEN
        (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
        REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
        ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
        DISCH_THEN(X_CHOOSE_THEN `x1:real^N` STRIP_ASSUME_TAC)] THEN
      REMOVE_THEN "2" (MP_TAC o SPEC `(phii:real^N->real->real^N) v2 t`) THEN
      ANTS_TAC THENL
       [MATCH_MP_TAC REAL_LT_TRANS THEN
        EXISTS_TAC `min d1 d2 / &3` THEN
        (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
        REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
        ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
        DISCH_THEN(X_CHOOSE_THEN `x2:real^N` STRIP_ASSUME_TAC)]] THEN

   (SUBGOAL_THEN
     `d * max (norm(x1:real^N)) (norm(x2:real^N))
      <= d * (norm x1 + norm x2) / &3`
    MP_TAC THENL
     [MATCH_MP_TAC(NORM_ARITH
       `norm(x - x1) <= d / &3 * norm x1 /\
        norm(x - x2) <= d / &3 * norm x2 /\
        dist(x1,x2) >= a
        ==> a <= d * (norm x1 + norm x2) / &3`) THEN
      ASM_SIMP_TAC[] THEN ASM_MESON_TAC[DIST_SYM; REAL_MAX_SYM];
      ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN
      DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
       `max x1 x2 <= (x1 + x2) / &3
          ==> &0 <= x1 /\ &0 <= x2 ==> x1 = &0 /\ x2 = &0`)) THEN
      REWRITE_TAC[NORM_POS_LE; NORM_EQ_0] THEN
      DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
      RULE_ASSUM_TAC(REWRITE_RULE[NORM_0; REAL_MUL_RZERO;
       NORM_ARITH `norm(x - vec 0) <= &0 <=> x = vec 0`]) THEN
      ASM_REWRITE_TAC[]]);
    ALL_TAC] THEN
  SUBGOAL_THEN
   `?e4. &0 < e4 /\
         !t. abs(t) < e4
             ==> fan6(vec 0,
                      IMAGE (\v. (phii:real^N->real->real^N) v t) V,
                      IMAGE (IMAGE (\v. phii v t)) E)`
  STRIP_ASSUME_TAC THENL
   [REWRITE_TAC[fan6; FORALL_IN_IMAGE] THEN
    MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN
    ASM_REWRITE_TAC[] THEN
    X_GEN_TAC `ee:real^N->bool` THEN DISCH_TAC THEN
    SUBGOAL_THEN `(ee:real^N->bool) HAS_SIZE 2` MP_TAC THENL
     [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`v:real^N`; `w:real^N`] THEN
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
    REWRITE_TAC[IMAGE_CLAUSES; SET_RULE `{a} UNION {b,c} = {a,b,c}`] THEN
    MP_TAC(ISPEC `UNIV DIFF {z | collinear{vec 0:real^N,fstcart z,sndcart z}}`
       open_def) THEN
    REWRITE_TAC[lemma; GSYM closed] THEN
    DISCH_THEN(MP_TAC o SPEC `pastecart (v:real^N) (w:real^N)`) THEN
    REWRITE_TAC[IN_DIFF; IN_ELIM_THM; IN_UNIV; FSTCART_PASTECART; 
                SNDCART_PASTECART] THEN
    ANTS_TAC THENL 
     [ASM_MESON_TAC[fan6; SET_RULE `{a} UNION {b,c} = {a,b,c}`]; ALL_TAC] THEN
    REWRITE_TAC[FORALL_PASTECART; FSTCART_PASTECART; SNDCART_PASTECART] THEN
    DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `(dd:real->real) (d / &2)` THEN ASM_SIMP_TAC[REAL_HALF] THEN
    X_GEN_TAC `t:real` THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
    REWRITE_TAC[dist; PASTECART_SUB] THEN
    MATCH_MP_TAC(REAL_ARITH
     `norm x < d / &2 /\ norm y < d / &2 /\ 
      norm(pastecart (x:real^N) (y:real^N)) <= norm x + norm y
      ==> norm(pastecart x y) < d`) THEN
    REWRITE_TAC[NORM_PASTECART_LE] THEN
    CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
    ASM_SIMP_TAC[REAL_HALF] THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
    REWRITE_TAC[IN_UNIONS] THEN ASM_MESON_TAC[IN_INSERT];
    ALL_TAC] THEN
  REWRITE_TAC[REAL_ARITH `--e < t /\ t < e <=> abs t < e`] THEN
  EXISTS_TAC `min (e1:real) (min e2 (min e3 e4))` THEN
  ASM_REWRITE_TAC[REAL_LT_MIN] THEN X_GEN_TAC `t:real` THEN STRIP_TAC THEN
  W(MP_TAC o PART_MATCH (lhs o rand) GMLWKPK_SIMPLE o goal_concl) THEN
  ASM_SIMP_TAC[] THEN ANTS_TAC THENL
   [CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
    REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_IMAGE] THEN ASM SET_TAC[];
    DISCH_THEN SUBST1_TAC THEN ASM_MESON_TAC[]]);;

let XRECQNS = 
prove_by_refinement(
  `!a b V E f.
    deformation f V (a,b) /\ FAN (vec 0,V,E) ==>
     (?e. &0 < e /\ (!t. --e < t /\ t < e ==>
        FAN(vec 0,
	    IMAGE (\v. f (v:real^3) t) V,
                               IMAGE (IMAGE (\v. f v t)) E)))`,

  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  REWRITE_TAC[Fan.FAN];
  INTRO_TAC Localization.ALL_TO_THE_NONPARALLEL_PART_ALT [`a`;`b`;`V`;`E`;`f`];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  INTRO_TAC FAN7_SMALL_DEFORMATION [`V`;`E`;`a`;`b`;`f`];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  TYPIFY `if (e < e') then e else e'` EXISTS_TAC;
  COND_CASES_TAC;
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    BY(ASM_MESON_TAC[arith `&0 < e /\ e < e' /\ -- e < t /\ t < e ==> -- e' < t /\ t < e'`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_MESON_TAC[arith `&0 < e' /\ ~(e < e') /\ -- e' < t /\ t < e' ==> -- e < t /\ t < e`])
  ]);;
  (* }}} *)


end;;