(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Tame Hypermap                                                     *)
(* Author: Alexey Solovyev                                                    *)
(* Date: 2010-07-07                                                           *)
(* (V,ESTD V) is a fan (4-point case)                                         *)
(* ========================================================================== *)

flyspeck_needs "tame/CKQOWSA_3.hl";;


module Ckqowsa_4_points = struct


open Ckqowsa_3_points;;



(* General *)

let IN_INTERVAL_1 = 
prove(`!a b c. lift c IN interval [lift a, lift b] <=> a <= c /\ c <= b`,

   REPEAT STRIP_TAC THEN
     SIMP_TAC[IN_INTERVAL; DIMINDEX_1; ARITH_RULE `1 <= i /\ i <= 1 <=> i = 1`] THEN
     REWRITE_TAC[GSYM drop; LIFT_DROP] THEN
     EQ_TAC THEN SIMP_TAC[] THEN
     DISCH_THEN (MP_TAC o SPEC `1`) THEN
     SIMP_TAC[]);;

let DIST_SQR = 
prove(`!v (w:real^N) d. dist(v,w) = d <=> dist(v,w) pow 2 = d pow 2 /\ &0 <= d`,

                     REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL
                       [
                         FIRST_X_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
                           REWRITE_TAC[DIST_POS_LE];
                         ASSUME_TAC (REAL_ARITH `!d. &0 <= d ==> d = abs(d)`) THEN
                           FIRST_ASSUM (MP_TAC o SPEC `d:real`) THEN
                           FIRST_X_ASSUM (MP_TAC o SPEC `dist(v:real^N,w)`) THEN
                           ASM_REWRITE_TAC[DIST_POS_LE] THEN
                           REPLICATE_TAC 2 (DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th])) THEN
                           ASM_REWRITE_TAC[REAL_EQ_SQUARE_ABS]
                       ]);;

let estd_non_collinear_lemma = 
prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\
                                       &2 <= dist (v,w) /\ dist (v,w) <= &2 * h0
                                       ==> ~collinear {vec 0, v, w}`,

   REWRITE_TAC[in_ball_annulus] THEN
     REWRITE_TAC[COLLINEAR_BETWEEN_CASES; between; DIST_0; DIST_SYM] THEN
     REWRITE_TAC[Sphere.h0] THEN
     REAL_ARITH_TAC);;


let zero_not_between = 
prove(`!v w:real^N. ~between (vec 0) (v, w) ==> ~(v = vec 0) /\ ~(w = vec 0) /\
                                                       (!a b. a < &0 /\ &0 < b ==> ~(a % w = b % v))`,

   REPEAT GEN_TAC THEN DISCH_TAC THEN
     SUBGOAL_THEN `~(v = vec 0:real^N) /\ ~(w = vec 0:real^N)` ASSUME_TAC THENL
     [
       POP_ASSUM MP_TAC THEN
         REWRITE_TAC[GSYM NORM_EQ_0] THEN
         REWRITE_TAC[between; DIST_0] THEN
         ASM_CASES_TAC `norm (v:real^N) = &0` THEN ASM_REWRITE_TAC[] THENL
         [
           POP_ASSUM MP_TAC THEN REWRITE_TAC[NORM_EQ_0] THEN
             DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
             REWRITE_TAC[DIST_0; REAL_ADD_LID];
           ALL_TAC
         ] THEN
         ASM_CASES_TAC `norm (w:real^N) = &0` THEN ASM_REWRITE_TAC[] THEN
         POP_ASSUM MP_TAC THEN REWRITE_TAC[NORM_EQ_0] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         REWRITE_TAC[DIST_0; REAL_ADD_RID];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN

     REPEAT STRIP_TAC THEN
     UNDISCH_TAC `~between (vec 0:real^N) (v,w)` THEN
     REWRITE_TAC[between; DIST_0] THEN
     POP_ASSUM (MP_TAC o AP_TERM `\v:real^N. inv(a) % v`) THEN
     REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
     ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> ~(a = &0)`; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
     DISCH_TAC THEN
     REWRITE_TAC[dist; VECTOR_ARITH `v - a % v = (&1 - a) % v:real^N`] THEN
     REWRITE_TAC[NORM_MUL] THEN

     SUBGOAL_THEN `&0 <= --(inv a * b)` ASSUME_TAC THENL
     [
       REWRITE_TAC[REAL_ARITH `&0 <= --(a * b) <=> &0 <= --a * b`] THEN
         MATCH_MP_TAC REAL_LE_MUL THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
         REWRITE_TAC[GSYM REAL_INV_NEG] THEN
         MATCH_MP_TAC REAL_LE_INV THEN
         ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> &0 <= --a`];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `abs (&1 - inv a * b) = &1 - inv a * b` (fun th -> REWRITE_TAC[th]) THENL
     [
       REWRITE_TAC[REAL_ABS_REFL] THEN
         REWRITE_TAC[REAL_ARITH `&1 - a = &1 + (--a)`] THEN
         MATCH_MP_TAC REAL_LE_ADD THEN
         ASM_REWRITE_TAC[REAL_LE_01];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `abs (inv a * b) = --(inv a * b)` (fun th -> REWRITE_TAC[th]) THENL
     [
       POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     REAL_ARITH_TAC);;

let zero_not_between_estd = 
prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\ dist (v,w) <= &2 * h0
                                    ==> ~between (vec 0) (v,w)`,

   REWRITE_TAC[in_ball_annulus; between; DIST_0; Sphere.h0] THEN
     REAL_ARITH_TAC);;


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

(* Some properties of projections *)

let projection = Sphere.projection;;


let PROJECTION_ORTHOGONAL = 
prove(`!d v:real^N. projection d v dot d = &0`,

   REWRITE_TAC[DOT_SYM; projection; VECTOR_SUB_PROJECT_ORTHOGONAL]);;

let VECTOR_PROJECTION = 
prove(`!d v:real^N. v = projection d v + (v dot d) / (d dot d) % d`,

   REWRITE_TAC[projection] THEN VECTOR_ARITH_TAC);;


let PROJECTION_0 = 
prove(`!d:real^N. projection d (vec 0) = vec 0`,

   REWRITE_TAC[projection; DOT_LZERO; real_div; REAL_MUL_LZERO] THEN
     VECTOR_ARITH_TAC);;

let PROJECTION_ZERO = 
prove(`!d:real^N. ~(d = vec 0) ==> projection d d = vec 0`,

   REWRITE_TAC[GSYM NORM_EQ_0] THEN GEN_TAC THEN DISCH_TAC THEN
     REWRITE_TAC[NORM_EQ_0; projection; DOT_SQUARE_NORM] THEN
     SUBGOAL_THEN `norm d pow 2 / norm (d:real^N) pow 2 = &1` (fun th -> REWRITE_TAC[th]) THENL
     [
       REWRITE_TAC[real_div; REAL_POW_2; REAL_INV_MUL] THEN
         REWRITE_TAC[REAL_ARITH `(d * d) * id * id = d * (d * id) * id`] THEN
         ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID];
       ALL_TAC
     ] THEN
     VECTOR_ARITH_TAC);;

let PROJECTION_LINEAR = 
prove(`!(d:real^N) v w a. projection d (v + w) = projection d v + projection d w /\
                                         projection d (a % v) = a % projection d v`,

   REPEAT GEN_TAC THEN
     REWRITE_TAC[projection; DOT_LMUL; DOT_LADD; real_div; REAL_ADD_RDISTRIB; VECTOR_SUB_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_ASSOC] THEN
     REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
     VECTOR_ARITH_TAC);;

let PROJECTION_NEG = 
prove(`!(d:real^N) v. projection d (--v) = --projection d v`,

                           REWRITE_TAC[VECTOR_ARITH `--v:real^N = -- &1 % v`; PROJECTION_LINEAR]);;

let PROJECTION_SUB = 
prove(`!(d:real^N) v w. projection d (v - w) = projection d v - projection d w`,

    REWRITE_TAC[VECTOR_ARITH `a - b:real^N = a + (--b)`; PROJECTION_LINEAR; PROJECTION_NEG]);;


let PROJECTION_DIST2 = 
prove(`!d v w:real^N. ~(d = vec 0) ==>
                               dist (projection d v, projection d w) pow 2 = dist (v,w) pow 2 - ((v - w) dot d) pow 2 / (norm d pow 2)`,

   REWRITE_TAC[GSYM NORM_EQ_0] THEN REPEAT STRIP_TAC THEN
     REWRITE_TAC[dist; projection] THEN
     REWRITE_TAC[VECTOR_ARITH `v - a % d - (w - b % d) = (v - w) - (a - b) % d:real^N`] THEN

     ABBREV_TAC `x = v - w:real^N` THEN
     ABBREV_TAC `y = ((v dot d) / (d dot d) - (w dot d) / (d dot d)) % d:real^N` THEN

     SUBGOAL_THEN `!a. a / (d dot d) * (d dot d:real^N) = a` ASSUME_TAC THENL
     [
       REWRITE_TAC[real_div; DOT_SQUARE_NORM; REAL_POW_2; REAL_INV_MUL] THEN
         REWRITE_TAC[REAL_ARITH `(a * id * id) * d * d = a * (id * (id * d) * d)`] THEN
         ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_LID; REAL_MUL_RID];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `x:real^N dot y = y dot y` ASSUME_TAC THENL
     [
       EXPAND_TAC "y" THEN
         REWRITE_TAC[real_div] THEN
         REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
         EXPAND_TAC "x" THEN
         REWRITE_TAC[DOT_LMUL; DOT_RMUL; DOT_SYM] THEN
         REWRITE_TAC[REAL_ARITH `(dv * id) * (dv * id) * d = ((dv * dv * id) * id) * d`] THEN
         ASM_REWRITE_TAC[GSYM real_div] THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
     REWRITE_TAC[REAL_ARITH `x - y - (y - y) = x - z <=> y = z`] THEN
     EXPAND_TAC "y" THEN
     REWRITE_TAC[real_div] THEN
     ASM_REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
     REWRITE_TAC[DOT_LMUL; DOT_RMUL] THEN
     ASM_REWRITE_TAC[GSYM real_div; DOT_SYM] THEN
     REAL_ARITH_TAC);;


let PROJECTION_SUM_DIST = 
prove(`!(d:real^N) x y a b. x dot d = &0 /\ y dot d = &0
                     ==> dist (x + a % d, y + b % d) pow 2 = dist (x, y) pow 2 + (a - b) pow 2 * (d dot d)`,

   REPEAT STRIP_TAC THEN
     GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [dist] THEN
     REWRITE_TAC[VECTOR_ARITH `(x + a % d) - (y + b % d) = (x - y) + (a - b) % d:real^N`] THEN
     SUBGOAL_THEN `(x - y:real^N) dot ((a - b) % d) = &0` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[DOT_RMUL; DOT_LSUB; REAL_MUL_RZERO; REAL_SUB_RZERO];
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM] THEN
     REWRITE_TAC[GSYM dist] THEN
     REWRITE_TAC[NORM_MUL; REAL_POW_MUL; REAL_POW2_ABS; DOT_SQUARE_NORM]);;


let PROJECTION_DIST_SPECIAL_EQ = 
prove(`!d x v w:real^N. ~(d = vec 0) /\ x dot d = &0
                                    ==> dist (x + (v - projection d v), w) pow 2 = dist (x, projection d w) pow 2 - dist (projection d v, projection d w) pow 2 + dist (v, w) pow 2`,

   REWRITE_TAC[GSYM NORM_EQ_0] THEN
     REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `!a. a / (d dot d) * (d dot d:real^N) = a` ASSUME_TAC THENL
     [
       REWRITE_TAC[real_div; DOT_SQUARE_NORM; REAL_POW_2; REAL_INV_MUL] THEN
         REWRITE_TAC[REAL_ARITH `(a * id * id) * d * d = a * (id * (id * d) * d)`] THEN
         ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_LID; REAL_MUL_RID];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `dist (x + v - projection d v, w) pow 2 = dist (x, projection d w) pow 2 + ((v - w) dot d:real^N) pow 2 / norm d pow 2` (fun th -> REWRITE_TAC[th]) THENL
     [
       MP_TAC (SPECL [`d:real^N`; `w:real^N`] VECTOR_PROJECTION) THEN
         DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
         SUBGOAL_THEN `v - projection d (v:real^N) = (v dot d) / (d dot d) % d` (fun th -> REWRITE_TAC[th]) THENL
         [
           REWRITE_TAC[projection] THEN
             VECTOR_ARITH_TAC;
           ALL_TAC
         ] THEN
         ASM_SIMP_TAC[PROJECTION_ORTHOGONAL; PROJECTION_SUM_DIST] THEN
         REWRITE_TAC[real_div] THEN
         REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
         REWRITE_TAC[REAL_ARITH `(a * b) pow 2 * c = ((a pow 2 * b) * b) * c`] THEN
         ASM_REWRITE_TAC[GSYM real_div; NORM_POW_2];
       ALL_TAC
     ] THEN
     MP_TAC (SPECL [`d:real^N`; `v:real^N`; `w:real^N`] PROJECTION_DIST2) THEN
     ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
     REAL_ARITH_TAC);;


let PROJECTION_DIST_SPECIAL_LE = 
prove(`!d x v w:real^N. ~(d = vec 0) /\ x dot d = &0 /\ dist (x, projection d w) <= dist (projection d v, projection d w)
                                        ==> dist (x + v - projection d v, w) <= dist (v, w)`,

   REPEAT STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     REWRITE_TAC[dist] THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
     REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
     REWRITE_TAC[GSYM dist] THEN
     ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ] THEN
     REAL_ARITH_TAC);;


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


(* General properties of affine hull and aff_ge *)

let aff_ge_0_2_eq_segment = 
prove(`!v:real^N. aff_ge {vec 0} {vec 0,v} = segment [vec 0,v] /\ aff_ge {vec 0} {v,vec 0} = segment [vec 0,v]`,

   GEN_TAC THEN
     REWRITE_TAC[SET_RULE `{v:real^N, vec 0} = {vec 0,v}`] THEN
     ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF] THEN
     REWRITE_TAC[SET_RULE `{vec 0} DIFF {vec 0,v:real^N} = {}`] THEN
     REWRITE_TAC[GSYM CONVEX_HULL_AFF_GE; SEGMENT_CONVEX_HULL]);;

let in_segment_imp_in_aff_ge_0_2 = 
prove(`!v v1 v2:real^N. v IN segment [v1,v2] ==> v IN aff_ge {vec 0} {v1,v2}`,

   REPEAT GEN_TAC THEN
     ASM_CASES_TAC `v1:real^N = vec 0` THENL
     [
       ASM_SIMP_TAC[aff_ge_0_2_eq_segment];
       ALL_TAC
     ] THEN
     ASM_CASES_TAC `v2:real^N = vec 0` THENL
     [
       ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; SEGMENT_SYM];
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[aff_ge_0_2] THEN
     REWRITE_TAC[IN_SEGMENT; IN_ELIM_THM] THEN
     STRIP_TAC THEN
     MAP_EVERY EXISTS_TAC [`&1 - u`; `u:real`] THEN
     ASM_REWRITE_TAC[] THEN
     UNDISCH_TAC `u <= &1` THEN REAL_ARITH_TAC);;


let points_in_aff_ge_0_2 = 
prove(`!v1 v2:real^N. vec 0 IN aff_ge {vec 0} {v1, v2} /\
                                                 v1 IN aff_ge {vec 0} {v1, v2} /\
                                                 v2 IN aff_ge {vec 0} {v1, v2}`,

   REPEAT GEN_TAC THEN
     ASM_CASES_TAC `v1:real^N = vec 0` THENL
     [
       ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; ENDS_IN_SEGMENT];
       ALL_TAC
     ] THEN
     ASM_CASES_TAC `v2:real^N = vec 0` THENL
     [
       ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; ENDS_IN_SEGMENT];
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
     REPEAT CONJ_TAC THENL
     [
       MAP_EVERY EXISTS_TAC [`&0`; `&0`];
       MAP_EVERY EXISTS_TAC [`&1`; `&0`];
       MAP_EVERY EXISTS_TAC [`&0`; `&1`]
     ] THEN
     REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID; VECTOR_ADD_RID]);;


let aff_ge_0_2_SUBSET = 
prove(`!v1 v2 v w:real^N. ~(v1 = vec 0) /\ ~(v2 = vec 0) /\
                                v IN aff_ge {vec 0} {v1,v2} /\ w IN aff_ge {vec 0} {v1,v2}
                                ==> aff_ge {vec 0} {v,w} SUBSET aff_ge {vec 0} {v1,v2}`,

   REPEAT STRIP_TAC THEN
     MP_TAC (ISPECL [`{vec 0:real^N}`; `{v1:real^N,v2}`] CONVEX_AFF_GE) THEN
     REWRITE_TAC[CONVEX_CONTAINS_SEGMENT] THEN DISCH_TAC THEN
     ASM_CASES_TAC `v:real^N = vec 0` THENL
     [
       ASM_REWRITE_TAC[aff_ge_0_2_eq_segment] THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         ASM_REWRITE_TAC[points_in_aff_ge_0_2];
       ALL_TAC
     ] THEN
     ASM_CASES_TAC `w:real^N = vec 0` THENL
     [
       ASM_REWRITE_TAC[aff_ge_0_2_eq_segment] THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         ASM_REWRITE_TAC[points_in_aff_ge_0_2];
       ALL_TAC
     ] THEN
     REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
     ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; SUBSET] THEN
     REPEAT STRIP_TAC THEN
     MAP_EVERY EXISTS_TAC [`t1'' * t1 + t2'' * t1'`; `t1'' * t2 + t2'' * t2'`] THEN
     REWRITE_TAC[CONJ_ASSOC] THEN
     CONJ_TAC THENL
     [
       CONJ_TAC THEN MATCH_MP_TAC REAL_LE_ADD THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN
     VECTOR_ARITH_TAC);;


let segment_inter_aff_ge_ends = 
prove(`!v1 v2 v w n:real^N. ~(v1 = vec 0) /\ ~(v2 = vec 0) /\
                                                            v1 dot n = &0 /\ v2 dot n = &0 /\
                                                            v dot n = &0 /\ ~(w dot n = &0) /\
                                                            ~(segment [v,w] INTER aff_ge {vec 0} {v1,v2} = {})
                                                            ==> v IN aff_ge {vec 0} {v1,v2}`,

   REPEAT STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
     REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
     REPEAT STRIP_TAC THEN
     FIRST_ASSUM MP_TAC THEN
     SUBGOAL_THEN `?t1 t2. &0 <= t1 /\ &0 <= t2 /\ x = t1 % v1 + t2 % v2:real^N` MP_TAC THENL
     [
       POP_ASSUM MP_TAC THEN
         ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN
     SUBGOAL_THEN `u = &0` ASSUME_TAC THENL
     [
       POP_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
         FIRST_X_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
         UNDISCH_TAC `~(w dot n:real^N = &0)` THEN
         CONV_TAC REAL_FIELD;
       ALL_TAC
     ] THEN
     UNDISCH_TAC `x = (&1 - u) % v + u % w:real^N` THEN
     POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
     REMOVE_ASSUM THEN
     REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_RID] THEN
     DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]));;



let in_affine_hull_lemma = 
prove(`!v1 v2 v:real^N. ~collinear {vec 0,v1,v2} /\ v IN affine hull {vec 0,v1,v2}
                                   ==> ?t1 t2. v = t1 % v1 + t2 % v2 /\
                                       (!t1' t2'. v = t1' % v1 + t2' % v2 ==> t1' = t1 /\ t2' = t2)`,

   REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
     REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
     REPEAT STRIP_TAC THEN
     UNDISCH_TAC `~collinear {vec 0,v1,v2:real^N}` THEN DISCH_TAC THEN
     FIRST_ASSUM MP_TAC THEN REWRITE_TAC[COLLINEAR_LEMMA] THEN
     FIRST_X_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{vec 0:real^N,v1,v2} = {vec 0,v2,v1}`] THEN
     REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
     REPEAT STRIP_TAC THEN

     MAP_EVERY EXISTS_TAC [`v':real`; `w:real`] THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT STRIP_TAC THENL
     [
       ASM_CASES_TAC `t1' = v':real` THEN ASM_REWRITE_TAC[] THEN
         SUBGOAL_TAC "A" `~(v' - t1' = &0)` [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
         FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
         REWRITE_TAC[VECTOR_ARITH `t1 % v1 + t2 % v2 = t1' % v1 + t2' % v2 <=> (t1 - t1') % v1 = (t2' - t2) % v2:real^N`] THEN
         DISCH_THEN (MP_TAC o AP_TERM `(\v:real^N. inv(v' - t1') % v)`) THEN BETA_TAC THEN
         REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
         ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID];
       ASM_CASES_TAC `t2' = w:real` THEN ASM_REWRITE_TAC[] THEN
         SUBGOAL_TAC "A" `~(w - t2' = &0)` [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
         FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
         REWRITE_TAC[VECTOR_ARITH `t1 % v1 + t2 % v2 = t1' % v1 + t2' % v2 <=> (t2 - t2') % v2 = (t1' - t1) % v1:real^N`] THEN
         DISCH_THEN (MP_TAC o AP_TERM `(\v:real^N. inv(w - t2') % v)`) THEN BETA_TAC THEN
         REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
         ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID]
     ]);;



let affine_hull_3_plane = 
prove(`!v1 v2 n:real^3. ~collinear {vec 0,v1,v2} /\ ~(n = vec 0) /\
                                  v1 dot n = &0 /\ v2 dot n = &0
                                  ==> affine hull {vec 0,v1,v2} = {v | v dot n = &0}`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `dim {n,v1,v2:real^3} = 3` ASSUME_TAC THENL
     [
       ONCE_REWRITE_TAC[DIM_INSERT] THEN
         SUBGOAL_THEN `~(n IN span {v1,v2:real^3})` (fun th -> REWRITE_TAC[th]) THENL
         [
           REWRITE_TAC[SPAN_2; IN_UNIV; IN_ELIM_THM] THEN
             STRIP_TAC THEN
             POP_ASSUM (MP_TAC o AP_TERM `(dot) (n:real^3)`) THEN
             POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
             SIMP_TAC[DOT_RADD; DOT_RMUL; DOT_SYM] THEN
             ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID; DOT_EQ_0];
           ALL_TAC
         ] THEN

         ONCE_REWRITE_TAC[DIM_INSERT] THEN
         SUBGOAL_THEN `~(v1:real^3 IN span {v2})` (fun th -> REWRITE_TAC[th]) THENL
         [
           REWRITE_TAC[SPAN_SING; IN_ELIM_THM; IN_UNIV] THEN
             UNDISCH_TAC `~collinear {vec 0:real^3,v1,v2}` THEN
             ONCE_REWRITE_TAC[SET_RULE `{vec 0:real^3,v1,v2} = {vec 0,v2,v1}`] THEN
             SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM];
           ALL_TAC
         ] THEN
         REWRITE_TAC[DIM_SING] THEN
         UNDISCH_TAC `~collinear {vec 0:real^3,v1,v2}` THEN
         SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
         ARITH_TAC;
       ALL_TAC
     ] THEN
     MP_TAC (ISPEC `{n:real^3,v1,v2}` DIM_EQ_FULL) THEN
     ASM_REWRITE_TAC[AFFINE_HULL_3; DIMINDEX_3; SPAN_3; IN_UNIV; EXTENSION; IN_ELIM_THM] THEN DISCH_TAC THEN
     REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
     GEN_TAC THEN
     EQ_TAC THENL
     [
       STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID];
       ALL_TAC
     ] THEN
     POP_ASSUM (MP_TAC o SPEC `x:real^3`) THEN
     STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
     ASM_REWRITE_TAC[REAL_ENTIRE; DOT_EQ_0] THEN
     DISCH_TAC THEN
     MAP_EVERY EXISTS_TAC [`&1 - v - w`; `v:real`; `w:real`] THEN
     CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
     ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);;



let intersection_point_exists = 
prove(`!v1 v2 n v w:real^3.
                                        ~collinear {vec 0,v1,v2} /\ ~(n = vec 0) /\
                                        v1 dot n = &0 /\ v2 dot n = &0 /\
                                        v dot n <= &0 /\
                                        &0 <= w dot n
                                        ==> ?p. p IN segment [v,w] INTER affine hull {vec 0,v1,v2}`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[IN_INTER; IN_SEGMENT; affine_hull_3_plane; IN_ELIM_THM] THEN
     ABBREV_TAC `d = (\u. ((&1 - u) % v + u % w) dot n:real^3)` THEN
     SUBGOAL_THEN `?u. (&0 <= u /\ u <= &1) /\ d u = &0` ASSUME_TAC THENL
     [
       REWRITE_TAC[GSYM IN_REAL_INTERVAL] THEN
         MATCH_MP_TAC REAL_IVT_INCREASING THEN
         REWRITE_TAC[REAL_LE_01] THEN
         EXPAND_TAC "d" THEN
         ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_LID; REAL_SUB_REFL] THEN
         ASM_REWRITE_TAC[VECTOR_ADD_LID] THEN
         EXPAND_TAC "d" THEN
         REWRITE_TAC[VECTOR_ARITH `((&1 - u) % v + u % w:real^3) dot n = v dot n + u * ((w - v) dot n)`] THEN
         MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
         REWRITE_TAC[REAL_CONTINUOUS_ON_CONST] THEN
         MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
         REWRITE_TAC[REAL_CONTINUOUS_ON_CONST; REAL_CONTINUOUS_ON_ID];
       ALL_TAC
     ] THEN
     POP_ASSUM MP_TAC THEN STRIP_TAC THEN
     EXISTS_TAC `(&1 - u) % v + u % w:real^3` THEN
     POP_ASSUM MP_TAC THEN EXPAND_TAC "d" THEN SIMP_TAC[] THEN
     DISCH_TAC THEN
     EXISTS_TAC `u:real` THEN ASM_REWRITE_TAC[]);;




let aux_ineq = 
prove(`!a b x. &0 < a /\ &0 < b /\ x = (&1 - a * a - b * b) / (&2 * a * b) /\ -- &1 <= x /\ x <= &1
                       ==> x * (&1 - a) <= b`,

   REPEAT GEN_TAC THEN
     REWRITE_TAC[GSYM IMP_IMP] THEN
     DISCH_TAC THEN DISCH_TAC THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     REPEAT DISCH_TAC THEN

     SUBGOAL_THEN `&0 < &2 * a * b` ASSUME_TAC THENL
     [
       MATCH_MP_TAC REAL_LT_MUL THEN
         REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
         MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `&1 <= (a + b) pow 2` ASSUME_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o check (is_binop `(<=):real->real->bool` o concl)) THEN
         MP_TAC (GEN_ALL RAT_LEMMA4) THEN
         DISCH_THEN (MP_TAC o SPECL [`&1 - a * a - b * b`; `&1`; `&1`; `&2 * a * b`]) THEN
         ASM_REWRITE_TAC[REAL_ARITH `&0 < &1`; REAL_ARITH `&1 / &1 = &1`] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `(a - b) pow 2 <= &1` ASSUME_TAC THENL
     [
       UNDISCH_TAC `-- &1 <= (&1 - a * a - b * b) / (&2 * a * b)` THEN
         MP_TAC (GEN_ALL RAT_LEMMA4) THEN
         DISCH_THEN (MP_TAC o SPECL [`-- &1`; `&2 * a * b`; `&1 - a * a - b * b`; `&1`]) THEN
         ASM_REWRITE_TAC[REAL_ARITH `&0 < &1`; REAL_ARITH `-- &1 / &1 = -- &1`] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN
     DISJ_CASES_TAC (REAL_ARITH `&0 < &1 - a \/ &1 - a = &0 \/ &1 - a < &0`) THENL
     [
       ASM_CASES_TAC `(&1 - a * a - b * b) / (&2 * a * b) < &0` THENL
         [
           MATCH_MP_TAC REAL_LE_TRANS THEN
             EXISTS_TAC `&0` THEN
             ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
             REWRITE_TAC[REAL_ARITH `a * b <= &0 <=> &0 <= (--a) * b`] THEN
             MATCH_MP_TAC REAL_LE_MUL THEN
             ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `x < &0 ==> &0 <= --x`];
           ALL_TAC
         ] THEN
         POP_ASSUM MP_TAC THEN
         REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
         ONCE_REWRITE_TAC[REAL_ARITH `x <= b <=> x <= &1 * b`] THEN
         MATCH_MP_TAC REAL_LE_MUL2 THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
         REWRITE_TAC[REAL_ARITH `&1 - a <= b <=> &1 <= a + b`] THEN
         SUBGOAL_THEN `&0 <= a + b` MP_TAC THENL
         [
           MATCH_MP_TAC REAL_LE_ADD THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
           ALL_TAC
         ] THEN
         ONCE_REWRITE_TAC[GSYM REAL_ABS_REFL] THEN
         DISCH_THEN (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
         ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
         ASM_REWRITE_TAC[REAL_LE_SQUARE_ABS; REAL_ARITH `&1 pow 2 = &1`];
       ALL_TAC
     ] THEN
     POP_ASSUM DISJ_CASES_TAC THENL
     [
       ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_LT_IMP_LE];
       ALL_TAC
     ] THEN
     ASM_CASES_TAC `&0 < (&1 - a * a - b * b) / (&2 * a * b)` THENL
     [
       MATCH_MP_TAC REAL_LE_TRANS THEN
         EXISTS_TAC `&0` THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
         REWRITE_TAC[REAL_ARITH `a * b <= &0 <=> &0 <= a * (--b)`] THEN
         MATCH_MP_TAC REAL_LE_MUL THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `x < &0 ==> &0 <= --x`];
       ALL_TAC
     ] THEN
     POP_ASSUM MP_TAC THEN
     REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
     ONCE_REWRITE_TAC[REAL_ARITH `x * y <= b <=> (--x) * (--y) <= &1 * b`] THEN
     MATCH_MP_TAC REAL_LE_MUL2 THEN
     ASM_SIMP_TAC[REAL_ARITH `x <= &0 ==> &0 <= --x`; REAL_ARITH `&1 - a < &0 ==> &0 <= --(&1 - a)`] THEN
     ASM_REWRITE_TAC[REAL_ARITH `-- x <= &1 <=> -- &1 <= x`] THEN
     REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
     REWRITE_TAC[ABS_SQUARE_LE_1] THEN
     REAL_ARITH_TAC);;


let rotation_dist_decrease_lemma = 
prove(`!v w u:real^N. u IN aff_ge {vec 0} {v,w} /\ norm u = norm v
                                   ==> dist (u,w) <= dist (v,w)`,

   REPEAT STRIP_TAC THEN
     ASM_CASES_TAC `v:real^N = vec 0` THENL
     [
       UNDISCH_TAC `norm (u:real^N) = norm (v:real^N)` THEN
         ASM_REWRITE_TAC[NORM_0; NORM_EQ_0] THEN
         SIMP_TAC[REAL_LE_REFL];
       ALL_TAC
     ] THEN
     ASM_CASES_TAC `w:real^N = vec 0` THENL
     [
       ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL];
       ALL_TAC
     ] THEN
     REWRITE_TAC[dist] THEN
     ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
     REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
     REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB] THEN
     ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
     REWRITE_TAC[REAL_ARITH `v - uw - (uw - w) <= v - vw - (vw - w) <=> vw <= uw`] THEN
     SUBGOAL_THEN `~(u = vec 0:real^N)` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
         ASM_REWRITE_TAC[NORM_EQ_0];
       ALL_TAC
     ] THEN

     MAP_EVERY ABBREV_TAC [`v':real^N = inv (norm v) % v`; `w':real^N = inv (norm w) % w`; `u':real^N = inv (norm u) % u`] THEN
     SUBGOAL_THEN `norm (v':real^N) = &1 /\ norm (w':real^N) = &1 /\ norm (u':real^N) = &1` ASSUME_TAC THENL
     [
       REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
         REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
         REWRITE_TAC[GSYM NORM_EQ_0; NORM_MUL] THEN
         SUBGOAL_THEN `!v:real^N. abs (inv (norm v)) = inv (norm v)` (fun th -> REWRITE_TAC[th]) THENL
         [
           REWRITE_TAC[REAL_ABS_REFL] THEN
             GEN_TAC THEN MATCH_MP_TAC REAL_LE_INV THEN
             REWRITE_TAC[NORM_POS_LE];
           ALL_TAC
         ] THEN
         SIMP_TAC[REAL_MUL_LINV];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `v:real^N = norm v % v' /\ w:real^N = norm w % w' /\ u:real^N = norm u % u'` ASSUME_TAC THENL
     [
       REMOVE_ASSUM THEN
         REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
         REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
         REWRITE_TAC[VECTOR_ARITH `a % b % v = (a * b) % v:real^N`; GSYM NORM_EQ_0] THEN
         SIMP_TAC[REAL_MUL_RINV] THEN
         REWRITE_TAC[VECTOR_MUL_LID];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `?a b. &0 <= a /\ &0 <= b /\ u':real^N = a % v' + b % w'` ASSUME_TAC THENL
     [
       REMOVE_ASSUM THEN REMOVE_ASSUM THEN
         REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
         FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
         ASM_SIMP_TAC[aff_ge_0_2] THEN
         REWRITE_TAC[IN_ELIM_THM] THEN
         REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
         REWRITE_TAC[GSYM NORM_EQ_0] THEN REPEAT STRIP_TAC THEN
         MAP_EVERY EXISTS_TAC [`t1:real`; `inv (norm (v:real^N)) * t2 * norm (w:real^N)`] THEN
         CONJ_TAC THEN ASM_REWRITE_TAC[] THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC REAL_LE_MUL THEN
             CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN REWRITE_TAC[NORM_POS_LE]; ALL_TAC ] THEN
             MATCH_MP_TAC REAL_LE_MUL THEN
             ASM_REWRITE_TAC[NORM_POS_LE];
           ALL_TAC
         ] THEN
         REWRITE_TAC[VECTOR_ARITH `(vv * t2 * ww) % iw % w = (vv * t2 * (ww * iw)) % (w:real^N)`] THEN
         ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN
     POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
     REPLICATE_TAC 3 (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_eq o concl))) THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[DOT_LMUL; DOT_RMUL] THEN
     MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
     MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN

     ASM_CASES_TAC `a = &0` THENL
     [
       UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
         ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
         DISCH_THEN (MP_TAC o AP_TERM `norm:real^N->real`) THEN
         ASM_REWRITE_TAC[NORM_MUL; REAL_MUL_LZERO; REAL_ADD_LID] THEN
         ASM_SIMP_TAC[REAL_ARITH `&0 <= b ==> abs b = b`; REAL_MUL_RID] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
         REWRITE_TAC[DOT_LMUL; DOT_SQUARE_NORM; REAL_MUL_LID] THEN
         ASM_REWRITE_TAC[VECTOR_ANGLE; REAL_POW_2; REAL_MUL_LID] THEN
         REWRITE_TAC[COS_BOUNDS];
       ALL_TAC
     ] THEN

     ASM_CASES_TAC `b = &0` THENL
     [
       UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
         ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
         DISCH_THEN (MP_TAC o AP_TERM `norm:real^N -> real`) THEN
         ASM_SIMP_TAC[NORM_MUL; REAL_ARITH `&0 <= t1 ==> abs t1 = t1`; REAL_MUL_RID] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
         REWRITE_TAC[DOT_LMUL; REAL_MUL_LID; REAL_LE_REFL];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; DOT_SQUARE_NORM; REAL_POW_2; REAL_MUL_RID] THEN
     REWRITE_TAC[REAL_ARITH `vw <= a * vw + b <=> vw * (&1 - a) <= b`] THEN
     MATCH_MP_TAC aux_ineq THEN
     ASM_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`] THEN
     CONJ_TAC THENL
     [
       UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
         DISCH_THEN (MP_TAC o AP_TERM `norm:real^N->real`) THEN
         ASM_REWRITE_TAC[] THEN
         ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
         ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
         REWRITE_TAC[REAL_EQ_SQUARE_ABS; NORM_POW_2; DOT_LADD; DOT_RADD; DOT_SYM; DOT_LMUL; DOT_RMUL] THEN
         ASM_REWRITE_TAC[DOT_SQUARE_NORM; REAL_MUL_RID; REAL_POW_2; REAL_MUL_RID] THEN
         REWRITE_TAC[REAL_ARITH `abs(&1) = &1`] THEN
         POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
         CONV_TAC REAL_FIELD;
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[VECTOR_ANGLE; REAL_MUL_LID; COS_BOUNDS]);;


let rotation_dist_decrease_special_case = 
prove(`!(v:real^N) w u a. &0 <= a /\ w = --a % v /\ norm u = norm v ==> dist (u,w) <= dist (v,w)`,

    REPEAT STRIP_TAC THEN
      REWRITE_TAC[dist] THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
      REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
      REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB] THEN
      REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
      ASM_REWRITE_TAC[DOT_RMUL] THEN
      REWRITE_TAC[REAL_ARITH `vv - uv - (uv - ww) <= vv - v2 - (v2 - ww) <=> --uv <= --v2`] THEN
      REWRITE_TAC[REAL_NEG_LMUL; REAL_NEG_NEG] THEN
      MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[] THEN
      ASM_REWRITE_TAC[VECTOR_ANGLE] THEN
      REPEAT (MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[NORM_POS_LE]) THEN
      REWRITE_TAC[VECTOR_ANGLE_REFL] THEN
      ASM_CASES_TAC `v:real^N = vec 0` THEN ASM_REWRITE_TAC[] THENL
      [
        REWRITE_TAC[vector_angle; REAL_LE_REFL];
        REWRITE_TAC[COS_0; COS_BOUNDS]
      ]);;



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

(* Lemmas about continuous functions *)


let continuous_lemma_inc = 
prove(`!f c t1. &0 <= t1 /\
                                f real_continuous_on real_interval [&0,t1] /\
                                f (&0) <= c /\ c <= f t1
                                ==> ?x. &0 <= x /\ x <= t1 /\ f x = c /\
                                        (!t. &0 <= t /\ t < x ==> f t < c)`,

   REPEAT STRIP_TAC THEN
     ABBREV_TAC `s = {t | &0 <= t /\ t <= t1 /\ c <= f t}` THEN
     SUBGOAL_THEN `t1:real IN s` ASSUME_TAC THENL
     [
       EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM; REAL_LE_REFL];
       ALL_TAC
     ] THEN
     EXISTS_TAC `inf s` THEN
     MP_TAC (SPEC `s:real->bool` INF) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
         CONJ_TAC THENL [ EXISTS_TAC `t1:real` THEN ASM_REWRITE_TAC[]; EXISTS_TAC `&0` ] THEN
         GEN_TAC THEN EXPAND_TAC "s" THEN
         SIMP_TAC[IN_ELIM_THM];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN

     (* 0 <= inf s *)
     SUBGOAL_THEN `&0 <= inf s` ASSUME_TAC THENL
     [
       POP_ASSUM (MP_TAC o SPEC `&0`) THEN
         ANTS_TAC THEN SIMP_TAC[] THEN
         GEN_TAC THEN EXPAND_TAC "s" THEN
         SIMP_TAC[IN_ELIM_THM];
       ALL_TAC
     ] THEN

     (* inf s <= t1 *)
     SUBGOAL_THEN `inf s <= t1` ASSUME_TAC THENL
     [
       REMOVE_ASSUM THEN POP_ASSUM (MP_TAC o SPEC `t1:real`) THEN
         ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     (* f t < c for all t IN [0,inf s) *)
     SUBGOAL_THEN `!t. &0 <= t /\ t < inf s ==> f t < c` ASSUME_TAC THENL
     [
       GEN_TAC THEN
         DISCH_THEN (LABEL_TAC "A") THEN
         SUBGOAL_THEN `&0 <= t /\ t <= t1` ASSUME_TAC THENL
         [
           ASM_REWRITE_TAC[] THEN
             MATCH_MP_TAC REAL_LT_IMP_LE THEN
             MATCH_MP_TAC REAL_LTE_TRANS THEN
             EXISTS_TAC `inf s` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         USE_THEN "A" MP_TAC THEN
         ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
         REWRITE_TAC[REAL_NOT_LT; DE_MORGAN_THM] THEN
         DISCH_TAC THEN DISJ2_TAC THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN

     (* f(inf s) = c *)
     DISJ_CASES_TAC (REAL_ARITH `c < f (inf s) \/ f (inf s) = c \/ f (inf s) < c`) THENL
     [
       (* f(inf s) > c *)
       MP_TAC (SPECL [`f:real->real`; `&0`; `inf s`; `c:real`] REAL_IVT_INCREASING) THEN
         ANTS_TAC THENL
         [
           ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
             MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
             EXISTS_TAC `real_interval [&0,t1]` THEN
             ASM_REWRITE_TAC[] THEN
             ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
           ALL_TAC
         ] THEN
         REWRITE_TAC[IN_REAL_INTERVAL] THEN
         STRIP_TAC THEN
         ASM_CASES_TAC `x = inf s` THENL
         [
           UNDISCH_TAC `f (x:real) = c:real` THEN
             ASM_SIMP_TAC[];
           ALL_TAC
         ] THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
         ASM_REWRITE_TAC[REAL_ARITH `x < inf s <=> x <= inf s /\ ~(x = inf s)`] THEN
         REWRITE_TAC[REAL_LT_REFL];
       ALL_TAC
     ] THEN
     POP_ASSUM DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN

     (* f(inf s) < c *)
     UNDISCH_TAC `f real_continuous_on real_interval [&0,t1]` THEN
     REWRITE_TAC[real_continuous_on] THEN
     DISCH_THEN (MP_TAC o SPEC `inf s`) THEN
     ASM_REWRITE_TAC[IN_REAL_INTERVAL] THEN
     DISCH_THEN (MP_TAC o SPEC `c - f (inf s)`) THEN
     ANTS_TAC THENL
     [
       POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
       ALL_TAC
     ] THEN
     STRIP_TAC THEN
     ABBREV_TAC `p = inf s + min (d / &2) (t1 - inf s)` THEN
     SUBGOAL_THEN `!t. &0 <= t /\ t <= p ==> f t < c` ASSUME_TAC THENL
     [
       GEN_TAC THEN
         ASM_CASES_TAC `t < inf s` THENL
         [
           DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN
         REPEAT STRIP_TAC THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
         ANTS_TAC THENL
         [
           ASM_REWRITE_TAC[] THEN
             CONJ_TAC THENL
             [
               MATCH_MP_TAC REAL_LE_TRANS THEN
                 EXISTS_TAC `p:real` THEN
                 ASM_REWRITE_TAC[] THEN
                 EXPAND_TAC "p" THEN
                 REWRITE_TAC[REAL_ARITH `a + b <= t1 <=> b <= t1 - a`] THEN
                 REWRITE_TAC[REAL_MIN_MIN];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC (REAL_ARITH `!a. &0 < d /\ a < d /\ &0 <= a ==> abs a < d`) THEN
             ASM_REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`] THEN
             MATCH_MP_TAC REAL_LET_TRANS THEN
             EXISTS_TAC `p - inf s` THEN
             ASM_REWRITE_TAC[REAL_ARITH `a - b <= c - b <=> a <= c`] THEN
             EXPAND_TAC "p" THEN
             REWRITE_TAC[REAL_ARITH `(a + b) - a = b`] THEN
             MATCH_MP_TAC REAL_LET_TRANS THEN
             EXISTS_TAC `d / &2` THEN
             ASM_SIMP_TAC[REAL_MIN_MIN; REAL_ARITH `&0 < d ==> d / &2 < d`];
           ALL_TAC
         ] THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `p <= inf s` MP_TAC THENL
     [
       FIRST_X_ASSUM MATCH_MP_TAC THEN
         GEN_TAC THEN
         ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
         REWRITE_TAC[REAL_NOT_LE] THEN
         DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
         EXPAND_TAC "s" THEN REWRITE_TAC[IN_ELIM_THM; DE_MORGAN_THM] THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
         ASM_CASES_TAC `&0 <= x` THEN ASM_REWRITE_TAC[] THEN
         SIMP_TAC[REAL_NOT_LE];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `inf s < p` MP_TAC THENL
     [
       EXPAND_TAC "p" THEN
         REWRITE_TAC[REAL_ARITH `a < a + b <=> &0 < b`] THEN
         ASM_SIMP_TAC[REAL_LT_MIN; REAL_ARITH `&0 < d ==> &0 < d / &2`] THEN
         ASM_CASES_TAC `inf s = t1` THENL
         [
           UNDISCH_TAC `f (inf s) < c` THEN
             POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
             UNDISCH_TAC `c <= f (t1:real)` THEN
             REAL_ARITH_TAC;
           ALL_TAC
         ] THEN
         ASM_REWRITE_TAC[REAL_ARITH `&0 < t1 - inf s <=> inf s <= t1 /\ ~(inf s = t1)`];
       ALL_TAC
     ] THEN
     REAL_ARITH_TAC);;


let continuous_lemma_dec = 
prove(`!f c t1. &0 <= t1 /\
                                   f real_continuous_on real_interval [&0,t1] /\
                                   c <= f (&0) /\ f t1 <= c
                                   ==> ?x. &0 <= x /\ x <= t1 /\ f x = c /\
                                        (!t. &0 <= t /\ t < x ==> c < f t)`,

   REPEAT STRIP_TAC THEN
     MP_TAC (SPECL [`\t. --(f:real->real) t`; `--c:real`; `t1:real`] continuous_lemma_inc) THEN
     ASM_REWRITE_TAC[] THEN
     ANTS_TAC THENL
     [
       CONJ_TAC THENL
         [
           MATCH_MP_TAC REAL_CONTINUOUS_ON_NEG THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         ASM_REWRITE_TAC[REAL_LE_NEG];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN
     EXISTS_TAC `x:real` THEN
     ASM_REWRITE_TAC[] THEN
     CONJ_TAC THENL
     [
       ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> --a = --b`] THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     GEN_TAC THEN STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
     ASM_REWRITE_TAC[REAL_LT_NEG]);;








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

(* Rotation lemmas *)


let rotation_lemma_special = 
prove(`!v w n:real^N. ~(v = vec 0) /\ ~(w = vec 0) /\
                                     (v dot n = &0) /\ (w dot n = &0) /\
                                     3 <= dimindex(:N) ==>
                                     ?f:real^1->real^N. f continuous_on UNIV /\
                                                        f(lift (&0)) = v /\ f(lift (&1)) = norm v / norm w % w /\
                                                        (!t. norm (f t) = norm v /\ f t dot n = &0) /\
                                                        (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), w) <= dist (v, w)) /\
                                                        (~collinear {vec 0, v, w} ==> (!t. &0 <= t /\ t <= &1 ==> f (lift t) IN aff_ge {vec 0} {v, w}))`,

   REPEAT GEN_TAC THEN STRIP_TAC THEN
     SUBGOAL_THEN `~(norm (v:real^N) = &0) /\ ~(norm (w:real^N) = &0)` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[NORM_EQ_0];
       ALL_TAC
     ] THEN

     ABBREV_TAC `u = norm (v:real^N) / norm w % w:real^N` THEN
     SUBGOAL_THEN `norm (u:real^N) = norm (v:real^N)` ASSUME_TAC THENL
     [
       POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
         REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; real_div] THEN
         ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `~(u = vec 0:real^N)` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[GSYM NORM_EQ_0];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `aff_ge {vec 0} {v,w} = aff_ge {vec 0:real^N} {v,u}` ASSUME_TAC THENL
     [
       MATCH_MP_TAC aff_ge_eq_lemma THEN
         EXISTS_TAC `norm (v:real^N) / norm (w:real^N)` THEN
         ASM_REWRITE_TAC[] THEN
         MATCH_MP_TAC REAL_LT_DIV THEN
         ASM_REWRITE_TAC[NORM_POS_LE; REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `collinear {vec 0, v, w:real^N} <=> collinear {vec 0, v, u}` (fun th -> REWRITE_TAC[th]) THENL
     [
       MP_TAC (ISPECL [`&1`; `norm (v:real^N) / norm (w:real^N)`; `v:real^N`; `w:real^N`] COLLINEAR_SCALE_ALL) THEN
         ANTS_TAC THENL
         [
           REWRITE_TAC[REAL_ARITH `~(&1 = &0)`] THEN
             MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
             MATCH_MP_TAC REAL_LT_DIV THEN
             ASM_REWRITE_TAC[NORM_POS_LT];
           ALL_TAC
         ] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
         ASM_REWRITE_TAC[VECTOR_MUL_LID];
       ALL_TAC
     ] THEN

     ASM_CASES_TAC `~collinear {vec 0,v,u:real^N}` THENL
     [
       MP_TAC (SPECL [`v:real^N`; `u:real^N`] rotation_lemma) THEN
         ASM_REWRITE_TAC[] THEN
         STRIP_TAC THEN
         EXISTS_TAC `f:real^1->real^N` THEN
         ASM_REWRITE_TAC[] THEN
         CONJ_TAC THENL
         [
           GEN_TAC THEN
             UNDISCH_TAC `!t:real^1. ?a b. f t = a % v + b % u:real^N` THEN
             DISCH_THEN (MP_TAC o SPEC `t:real^1`) THEN STRIP_TAC THEN
             ASM_REWRITE_TAC[] THEN
             UNDISCH_TAC `f (lift (&1)) = u:real^N` THEN
             DISCH_THEN (fun th -> ALL_TAC) THEN
             EXPAND_TAC "u" THEN
             REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
             ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID];
           ALL_TAC
         ] THEN
         CONJ_TAC THENL
         [
           REPEAT STRIP_TAC THEN
             MATCH_MP_TAC rotation_dist_decrease_lemma THEN
             ASM_REWRITE_TAC[] THEN
             FIRST_X_ASSUM MATCH_MP_TAC THEN
             ASM_REWRITE_TAC[IN_INTERVAL_1];
           ALL_TAC
         ] THEN
         REPEAT STRIP_TAC THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         ASM_REWRITE_TAC[IN_INTERVAL_1];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN
     POP_ASSUM MP_TAC THEN
     ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
     STRIP_TAC THEN
     FIRST_ASSUM (MP_TAC o AP_TERM `norm:real^N->real`) THEN
     ASM_REWRITE_TAC[NORM_MUL] THEN
     ASM_REWRITE_TAC[REAL_ARITH `v = c * v <=> v * (c - &1) = &0`; REAL_ENTIRE; REAL_ARITH `abs c - &1 = &0 <=> c = &1 \/ c = -- &1`] THEN
     DISCH_THEN DISJ_CASES_TAC THENL
     [
       EXISTS_TAC `(\t:real^1. v:real^N)` THEN
         ASM_REWRITE_TAC[CONTINUOUS_ON_CONST; VECTOR_MUL_LID; REAL_LE_REFL];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `?e:real^N. e dot v = &0 /\ norm e = norm v /\ e dot n = &0` ASSUME_TAC THENL
     [
       SUBGOAL_THEN `dim {v:real^N,n} < dimindex (:N)` ASSUME_TAC THENL
         [
           MATCH_MP_TAC LET_TRANS THEN
             EXISTS_TAC `2` THEN
             ASM_SIMP_TAC[ARITH_RULE `3 <= a ==> 2 < a`] THEN
             MATCH_MP_TAC LE_TRANS THEN
             EXISTS_TAC `CARD {v:real^N,n}` THEN
             SUBGOAL_THEN `FINITE {v:real^N,n}` ASSUME_TAC THENL
             [
               REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
               ALL_TAC
             ] THEN
             ASM_SIMP_TAC[DIM_LE_CARD] THEN
             REWRITE_TAC[Geomdetail.CARD2];
           ALL_TAC
         ] THEN
         MP_TAC (SPEC `{v:real^N,n}` ORTHOGONAL_TO_SUBSPACE_EXISTS) THEN
         ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; orthogonal] THEN
         STRIP_TAC THEN
         EXISTS_TAC `norm (v:real^N) / norm (x:real^N) % x:real^N` THEN
         FIRST_ASSUM (MP_TAC o SPEC `v:real^N`) THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `n:real^N`) THEN
         REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN
         ASM_REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; real_div; GSYM REAL_MUL_ASSOC; DOT_LMUL; REAL_MUL_RZERO] THEN
         UNDISCH_TAC `~(x:real^N = vec 0)` THEN
         SIMP_TAC[GSYM NORM_EQ_0; REAL_MUL_LINV; REAL_MUL_RID];
       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN STRIP_TAC THEN

     ABBREV_TAC `f = (\t:real^1. cos (pi * drop t) % v + sin (pi * drop t) % e:real^N)` THEN
     EXISTS_TAC `f:real^1->real^N` THEN

     CONJ_TAC THENL
     [
       EXPAND_TAC "f" THEN
         MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
         CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_VMUL THENL
         [
           SUBGOAL_THEN `lift o (\t:real^1. cos (pi * drop t)) = (lift o cos o drop) o (\t:real^1. pi % t)` (fun th -> REWRITE_TAC[th]) THENL
             [
               REWRITE_TAC[FUN_EQ_THM; o_THM; DROP_CMUL];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
             CONJ_TAC THENL [ MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC [CONTINUOUS_ON_ID]; ALL_TAC ] THEN
             MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
             GEN_TAC THEN DISCH_TAC THEN
             MP_TAC (SPEC `drop (x:real^1)` REAL_CONTINUOUS_AT_COS) THEN
             REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS_ATREAL; LIFT_DROP];

           SUBGOAL_THEN `lift o (\t:real^1. sin (pi * drop t)) = (lift o sin o drop) o (\t:real^1. pi % t)` (fun th -> REWRITE_TAC[th]) THENL
             [
               REWRITE_TAC[FUN_EQ_THM; o_THM; DROP_CMUL];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
             CONJ_TAC THENL [ MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC [CONTINUOUS_ON_ID]; ALL_TAC ] THEN
             MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
             GEN_TAC THEN DISCH_TAC THEN
             MP_TAC (SPEC `drop (x:real^1)` REAL_CONTINUOUS_AT_SIN) THEN
             REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS_ATREAL; LIFT_DROP];
         ];
       ALL_TAC
     ] THEN

     CONJ_TAC THENL
     [
       EXPAND_TAC "f" THEN
         REWRITE_TAC[LIFT_DROP; REAL_MUL_RZERO; COS_0; SIN_0; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
       ALL_TAC
     ] THEN

     CONJ_TAC THENL
     [
       EXPAND_TAC "f" THEN
         ASM_REWRITE_TAC[LIFT_DROP; REAL_MUL_RID; COS_PI; SIN_PI; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `!t:real^1. norm ((f:real^1->real^N) t) = norm (v:real^N)` ASSUME_TAC THENL
     [
       EXPAND_TAC "f" THEN
         GEN_TAC THEN
         ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
         REWRITE_TAC[REAL_EQ_SQUARE_ABS] THEN
         ASM_REWRITE_TAC[NORM_POW_2; DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; DOT_SYM; REAL_MUL_RZERO; REAL_ADD_LID; REAL_ADD_RID] THEN
         ASM_REWRITE_TAC[DOT_SQUARE_NORM] THEN
         REWRITE_TAC[REAL_ARITH `c * c * n + s * s * n = (s pow 2 + c pow 2) * n`] THEN
         REWRITE_TAC[SIN_CIRCLE; REAL_MUL_LID];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN
     CONJ_TAC THENL
     [
       GEN_TAC THEN EXPAND_TAC "f" THEN
         ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID];
       ALL_TAC
     ] THEN

     GEN_TAC THEN DISCH_TAC THEN
     MATCH_MP_TAC rotation_dist_decrease_special_case THEN
     ASM_REWRITE_TAC[] THEN
     EXISTS_TAC `norm(w:real^N) / norm(v:real^N)` THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC REAL_LE_DIV THEN
         REWRITE_TAC[NORM_POS_LE];
       ALL_TAC
     ] THEN
     UNDISCH_TAC `norm (v:real^N) / norm (w:real^N) % w = u` THEN
     DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. norm (w:real^N) / norm (v:real^N) % x`) THEN
     REWRITE_TAC[VECTOR_MUL_ASSOC; real_div] THEN
     ONCE_REWRITE_TAC[REAL_ARITH `(w * iv) * v * iw = (w * iw) * (v * iv)`] THEN
     ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID; VECTOR_MUL_LID] THEN
     VECTOR_ARITH_TAC);;


(* Consider properties of intersecting segments *)
let aff_ge_inter_segments = 
prove(`!v w u p:real^N. ~collinear {vec 0, v, u} /\ p IN aff_ge {vec 0} {v, u} /\
                                           ~(segment [v, w] INTER aff_ge {vec 0} {u} = {})
                                           ==> ~(segment [p, w] INTER aff_ge {vec 0} {u} = {})`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `(?x y. &0 <= x /\ x <= &1 /\ &0 <= y /\ (&1 - x) % p + x % w:real^N = y % u) ==> ~(segment [p,w] INTER aff_ge {vec 0} {u} = {})` MP_TAC THENL
     [
       STRIP_TAC THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
         REWRITE_TAC[IN_INTER; IN_SEGMENT; HALFLINE; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
         EXISTS_TAC `(&1 - x) % p + x % w:real^N` THEN
         CONJ_TAC THENL
         [
           REMOVE_ASSUM THEN
             EXISTS_TAC `x:real` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         ASM_REWRITE_TAC[IN_ELIM_THM] THEN
         EXISTS_TAC `y:real` THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[TAUT `~(A ==> ~B) <=> A /\ B`] THEN
     REMOVE_ASSUM THEN

     SUBGOAL_THEN `~(v = vec 0:real^N) /\ ~(u = vec 0:real^N)` ASSUME_TAC THENL
     [
       UNDISCH_TAC `~collinear {vec 0, v, u:real^N}` THEN
         SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM];
       ALL_TAC
     ] THEN

     UNDISCH_TAC `p IN aff_ge {vec 0:real^N} {v, u}` THEN
     ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
     STRIP_TAC THEN

     SUBGOAL_THEN `?a c. &0 <= a /\ a <= &1 /\ &0 <= c /\ (&1 - a) % v + a % w = c % u:real^N` MP_TAC THENL
     [
       UNDISCH_TAC `~(segment [v,w] INTER aff_ge {vec 0} {u:real^N} = {})` THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
         REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
         STRIP_TAC THEN
         MAP_EVERY EXISTS_TAC [`u':real`; `t:real`] THEN
         ASM_REWRITE_TAC[] THEN
         POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN

     ASM_CASES_TAC `a = &0` THENL
     [
       MAP_EVERY EXISTS_TAC [`&0`; `t1 * c + t2:real`] THEN
         REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID] THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC REAL_LE_ADD THEN
             ASM_REWRITE_TAC[] THEN
             MATCH_MP_TAC REAL_LE_MUL THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         ASM_REWRITE_TAC[] THEN
         UNDISCH_TAC `(&1 - a) % v + a % w = c % u:real^N` THEN
         ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN

     FIRST_X_ASSUM (MP_TAC o AP_TERM `\x:real^N. inv a % x` o check (is_eq o concl)) THEN
     ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
     ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
     REWRITE_TAC[VECTOR_ARITH `v + w = z <=> w = z - v:real^N`] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     REWRITE_TAC[VECTOR_ARITH `x % (a % u - b % v) = (x * a) % u + (--x * b) % v:real^N`] THEN
     REWRITE_TAC[VECTOR_ARITH `y % u - (a % v + b % u) = (y - b) % u + (--a) % v:real^N`] THEN

     ABBREV_TAC `b = inv a * (&1 - a)` THEN
     ABBREV_TAC `d = inv a * c` THEN

     ASM_CASES_TAC `t1 = &0` THENL
     [
       MAP_EVERY EXISTS_TAC [`&0`; `t2:real`] THEN
         ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; REAL_MUL_LZERO; VECTOR_MUL_LZERO; REAL_MUL_LNEG; VECTOR_MUL_LNEG; REAL_SUB_RZERO; REAL_SUB_REFL; REAL_MUL_LID];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `&0 <= b /\ &0 <= d` ASSUME_TAC THENL
     [
       SUBGOAL_THEN `&0 <= inv a` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
         EXPAND_TAC "b" THEN EXPAND_TAC "d" THEN
         CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1`];
       ALL_TAC
     ] THEN

     ABBREV_TAC `x = t1 / (b + t1)` THEN
     MAP_EVERY EXISTS_TAC [`x:real`; `(&1 - x) * t2 + x * d`] THEN
     SUBGOAL_THEN `&0 <= x /\ x <= &1` ASSUME_TAC THENL
     [
       EXPAND_TAC "x" THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC REAL_LE_DIV THEN
             ASM_REWRITE_TAC[] THEN
             MATCH_MP_TAC REAL_LE_ADD THEN ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC REAL_LET_ADD THEN
             ASM_REWRITE_TAC[REAL_LT_LE];
           ALL_TAC
         ] THEN
         ASM_REWRITE_TAC[REAL_ARITH `t1 <= b + t1 <=> &0 <= b`];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC REAL_LE_ADD THEN
         CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`];
       ALL_TAC
     ] THEN

     REWRITE_TAC[REAL_ARITH `((&1 - x) * t2 + x * d) - (&1 - x) * t2 = x * d`] THEN
     SUBGOAL_THEN `--x * b = --((&1 - x) * t1)` (fun th -> REWRITE_TAC[th]) THEN
     SUBGOAL_THEN `&1 - x = b * x * inv t1` (fun th -> REWRITE_TAC[th]) THENL
     [
       EXPAND_TAC "x" THEN
         SUBGOAL_THEN `~(b + t1 = &0)` ASSUME_TAC THENL
         [
           MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
             MATCH_MP_TAC REAL_LET_ADD THEN
             ASM_REWRITE_TAC[REAL_LT_LE];
           ALL_TAC
         ] THEN
         MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN
         EXISTS_TAC `b + t1:real` THEN
         FIRST_ASSUM (fun th -> REWRITE_TAC[th; real_div]) THEN
         REWRITE_TAC[REAL_ARITH `bt * (&1 - t1 * ibt) = bt - t1 * (bt * ibt)`] THEN
         REWRITE_TAC[REAL_ARITH `bt * b * (t * ibt) * it = (bt * ibt) * (t * it) * b`] THEN
         ASM_SIMP_TAC[REAL_MUL_RINV] THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
     ASM_SIMP_TAC[REAL_MUL_LINV] THEN
     REAL_ARITH_TAC);;


(* A special version of the rotation lemma for intersecting segments *)
let rotation_lemma_segments = 
prove(`!v w u n:real^N. 3 <= dimindex (:N) /\
                                      ~(v = vec 0) /\ ~(u = vec 0) /\
                                      v dot n = &0 /\ w dot n = &0 /\ u dot n = &0 /\
                                      ~(segment [vec 0,u] INTER segment [v,w] = {})
                                      ==> ?f:real^1->real^N. f continuous_on UNIV /\
                                                             f (lift (&0)) = v /\
                                                             f (lift (&1)) = norm v / norm u % u /\
                                                             (!t. norm (f t) = norm v /\ f t dot n = &0) /\
                                                             (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), u) <= dist (v, u) /\
                                                                       dist (f (lift t), w) <= dist (v, w)) /\
                                                             (!t. &0 <= t /\ t <= &1 ==> ~(segment [f (lift t), w] INTER aff_ge {vec 0} {u} = {}))`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `~collinear {vec 0, v, w:real^N} ==> ~(w = vec 0) /\ (!t. ~((&1 - t) % v + t % w = vec 0))` ASSUME_TAC THENL
     [
       REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN STRIP_TAC THEN
         ASM_REWRITE_TAC[] THEN
         GEN_TAC THEN
         ASM_CASES_TAC `t = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID] THEN
         DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. inv t % x`) THEN
         REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
         ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID; VECTOR_MUL_RZERO] THEN
         ASM_REWRITE_TAC[VECTOR_ARITH `a % v + w = vec 0 <=> w = (--a) % v:real^N`];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `~(segment [v,w] INTER aff_ge {vec 0} {u:real^N} = {})` ASSUME_TAC THENL
     [
       UNDISCH_TAC `~(segment [vec 0,u] INTER segment [v,w:real^N] = {})` THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
         STRIP_TAC THEN
         EXISTS_TAC `x:real^N` THEN
         ASM_REWRITE_TAC[] THEN
         MATCH_MP_TAC Hypermap.lemma_in_subset THEN
         EXISTS_TAC `segment [vec 0,u:real^N]` THEN
         ASM_REWRITE_TAC[SEGMENT_SUBSET_HALFLINE];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `?x c. &0 <= x /\ x <= &1 /\ &0 <= c /\ (&1 - x) % v + x % w = c % u:real^N` MP_TAC THENL
     [
       POP_ASSUM MP_TAC THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
         REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
         STRIP_TAC THEN
         MAP_EVERY EXISTS_TAC [`u':real`; `t:real`] THEN
         ASM_REWRITE_TAC[] THEN
         POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
       ALL_TAC
     ] THEN
     STRIP_TAC THEN

     ASM_CASES_TAC `~collinear {vec 0, v, u:real^N}` THENL
     [
       MP_TAC (SPECL [`v:real^N`; `u:real^N`; `n:real^N`] rotation_lemma_special) THEN
         ASM_SIMP_TAC[] THEN
         STRIP_TAC THEN
         EXISTS_TAC `f:real^1->real^N` THEN
         ASM_REWRITE_TAC[] THEN

         ASM_CASES_TAC `w = vec 0:real^N` THENL
         [
           ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL] THEN
             REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
             REPEAT STRIP_TAC THEN
             EXISTS_TAC `vec 0:real^N` THEN
             REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT; ENDS_IN_HALFLINE];
           ALL_TAC
         ] THEN

         ASM_CASES_TAC `~collinear {vec 0, v, w:real^N}` THENL
         [
           FIRST_ASSUM (fun th -> FIRST_X_ASSUM (MP_TAC o MATCH_MP th)) THEN
             STRIP_TAC THEN
             CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
             [
               ASM_SIMP_TAC[] THEN
                 MATCH_MP_TAC rotation_dist_decrease_lemma THEN
                 ASM_REWRITE_TAC[] THEN
                 SUBGOAL_THEN `?a b. &0 <= a /\ &0 <= b /\ u = a % v + b % w:real^N` MP_TAC THENL
                 [
                   FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
                     DISCH_TAC THEN
                     UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
                     ASM_CASES_TAC `c = &0` THENL [ ASM_REWRITE_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
                     DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv c % v`) THEN
                     ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
                     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
                     MAP_EVERY EXISTS_TAC [`inv c * (&1 - x)`; `inv c * x`] THEN
                     REWRITE_TAC[] THEN
                     SUBGOAL_THEN `&0 <= inv c` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
                     CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`];
                   ALL_TAC
                 ] THEN
                 STRIP_TAC THEN

                 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
                 REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `t:real`)) THEN
                 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
                 STRIP_TAC THEN DISCH_THEN (fun th -> ALL_TAC) THEN
                 MAP_EVERY EXISTS_TAC [`t1 + t2 * a:real`; `t2 * b:real`] THEN
                 CONJ_TAC THENL
                 [
                   MATCH_MP_TAC REAL_LE_ADD THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[];
                   ALL_TAC
                 ] THEN
                 CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
                 ASM_REWRITE_TAC[] THEN
                 VECTOR_ARITH_TAC;
               ALL_TAC
             ] THEN

             MATCH_MP_TAC aff_ge_inter_segments THEN
             EXISTS_TAC `v:real^N` THEN
             ASM_SIMP_TAC[];
           ALL_TAC
         ] THEN

         CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
         [
           ASM_SIMP_TAC[] THEN
             SUBGOAL_THEN `c = &0` ASSUME_TAC THENL
             [
               UNDISCH_TAC `~ ~collinear {vec 0, v, w:real^N}` THEN
                 ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
                 STRIP_TAC THEN
                 UNDISCH_TAC `~collinear {vec 0, v, u:real^N}` THEN
                 ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
                 DISCH_TAC THEN
                 ASM_CASES_TAC `c = &0` THEN ASM_REWRITE_TAC[] THEN
                 UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
                 DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. inv c % x`) THEN
                 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
                 ASM_REWRITE_TAC[VECTOR_ARITH `a % (b % v + c % v) = (a * b + a * c) % v`];
               ALL_TAC
             ] THEN

             SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
             [
               ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THEN
                 UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
                 ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
               ALL_TAC
             ] THEN

             MATCH_MP_TAC rotation_dist_decrease_special_case THEN
             EXISTS_TAC `inv x * (&1 - x)` THEN
             ASM_SIMP_TAC[] THEN
             CONJ_TAC THENL
             [
               MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`] THEN
                 MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[];
               ALL_TAC
             ] THEN

             UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
             ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
             REWRITE_TAC[VECTOR_ARITH `a % v + x % w = vec 0:real^N <=> x % w = --a % v`] THEN
             DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv x % v`) THEN
             ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
             DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
             VECTOR_ARITH_TAC;
           ALL_TAC
         ] THEN

         MATCH_MP_TAC aff_ge_inter_segments THEN
         EXISTS_TAC `v:real^N` THEN
         ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN
     REWRITE_TAC[] THEN
     MP_TAC (ISPECL [`vec 0:real^N`; `u:real^N`; `v:real^N`] (GEN_ALL (CONJUNCT1 Collect_geom.PER_SET3))) THEN
     DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
     ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
     DISCH_THEN (X_CHOOSE_THEN `b:real` (LABEL_TAC "v" o SYM)) THEN
     ASM_CASES_TAC `&0 <= b` THENL
     [
       EXISTS_TAC `\t:real^1. v:real^N` THEN
         ASM_REWRITE_TAC[CONTINUOUS_ON_CONST; REAL_LE_REFL] THEN
         REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
         REWRITE_TAC[NORM_MUL; real_div; GSYM REAL_MUL_ASSOC] THEN
         UNDISCH_TAC `~(u = vec 0:real^N)` THEN
         REWRITE_TAC[GSYM NORM_EQ_0] THEN
         SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
         SUBGOAL_THEN `abs b = b` (fun th -> REWRITE_TAC[th]) THEN
         ASM_REWRITE_TAC[REAL_ABS_REFL];
       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`v:real^N`; `u:real^N`; `n:real^N`] rotation_lemma_special) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     EXISTS_TAC `f:real^1->real^N` THEN
     ASM_SIMP_TAC[] THEN

     ASM_CASES_TAC `w = vec 0:real^N` THENL
     [
       ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL] THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
         REPEAT STRIP_TAC THEN
         EXISTS_TAC `vec 0:real^N` THEN
         REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT; ENDS_IN_HALFLINE];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `?d. &0 <= d /\ w = d % u:real^N` ASSUME_TAC THENL
     [
       SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
         [
           DISCH_TAC THEN
             UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
             ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
             REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
             ASM_REWRITE_TAC[VECTOR_ARITH `b % u = c % u <=> (c + --b) % u = vec 0:real^N`; VECTOR_MUL_EQ_0] THEN
             MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
             MATCH_MP_TAC REAL_LET_ADD THEN
             ASM_REWRITE_TAC[REAL_NEG_GT0];
           ALL_TAC
         ] THEN

         UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
         DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv x % v`) THEN
         ASM_SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
         REWRITE_TAC[VECTOR_ARITH `a + w = b <=> w = b - a:real^N`] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th; VECTOR_MUL_ASSOC; GSYM VECTOR_SUB_RDISTRIB]) THEN
         ABBREV_TAC `d = inv x * c - ((inv x * (&1 - x)) * b)` THEN

         EXISTS_TAC `d:real` THEN
         ASM_REWRITE_TAC[] THEN
         EXPAND_TAC "d" THEN
         REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN
         MATCH_MP_TAC REAL_LE_MUL THEN
         CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
         REWRITE_TAC[REAL_ARITH `c - a * b = c + a * (--b)`] THEN
         MATCH_MP_TAC REAL_LE_ADD THEN
         ASM_REWRITE_TAC[] THEN
         MATCH_MP_TAC REAL_LE_MUL THEN
         ASM_REWRITE_TAC[REAL_NEG_GE0; REAL_ARITH `&0 <= &1 - x <=> x <= &1`] THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE];
       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN STRIP_TAC THEN
     CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
     [
       MATCH_MP_TAC rotation_dist_decrease_special_case THEN
         EXISTS_TAC `--inv b * d` THEN
         ASM_SIMP_TAC[] THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC REAL_LE_MUL THEN
             ASM_REWRITE_TAC[GSYM REAL_INV_NEG] THEN
             MATCH_MP_TAC REAL_LE_INV THEN
             ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
           ALL_TAC
         ] THEN

         REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
         REWRITE_TAC[VECTOR_MUL_ASSOC; REAL_ARITH `--(--inv b * d) * b = d * b * inv b`] THEN
         ASM_SIMP_TAC[REAL_ARITH `b < &0 ==> ~(b = &0)`; REAL_MUL_RINV; REAL_MUL_RID];
       ALL_TAC
     ] THEN

     REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
     EXISTS_TAC `w:real^N` THEN
     CONJ_TAC THENL
     [
       EXISTS_TAC `&1` THEN
         ASM_REWRITE_TAC[REAL_LE_01; REAL_LE_REFL; REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID];
       ALL_TAC
     ] THEN
     EXISTS_TAC `d:real` THEN
     ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID]);;



(* Rotation about an axis lemma *)
let rotation_about_axis = 
prove(`!d v w:real^N. 3 <= dimindex (:N) /\ ~(d = vec 0) /\
                                  ~(projection d w = vec 0) /\
                                  ~(projection d v = vec 0)
                                  ==> ?(f:real^1->real^N) a b. &0 < a /\
                                        f continuous_on UNIV /\
                                        f(lift (&0)) = v /\
                                        f(lift (&1)) = a % w + b % d /\
                                        (!t c. dist (f t, c % d) = dist (v, c % d)) /\
                                        (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), w) <= dist (v, w))`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `~(norm (projection d (v:real^N)) = &0) /\ ~(norm (projection d (w:real^N)) = &0)` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[NORM_EQ_0];
       ALL_TAC
     ] THEN
     MP_TAC (SPECL [`projection d (v:real^N)`; `projection d (w:real^N)`; `d:real^N`] rotation_lemma_special) THEN
     ASM_REWRITE_TAC[PROJECTION_ORTHOGONAL] THEN

     DISCH_THEN (X_CHOOSE_THEN `g:real^1->real^N` MP_TAC) THEN
     STRIP_TAC THEN

     EXISTS_TAC `\t:real^1. g t + (v - projection d (v:real^N))` THEN
     EXISTS_TAC `norm (projection d (v:real^N)) / norm (projection d (w:real^N))` THEN
     ABBREV_TAC `a = norm (projection d (v:real^N)) / norm (projection d (w:real^N))` THEN
     EXISTS_TAC `(v dot (d:real^N)) / norm d pow 2 - a * (w dot d) / norm d pow 2` THEN

     CONJ_TAC THENL
     [
       EXPAND_TAC "a" THEN
         MATCH_MP_TAC REAL_LT_DIV THEN
         ASM_REWRITE_TAC[NORM_POS_LT];
       ALL_TAC
     ] THEN

     CONJ_TAC THENL
     [
       MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
         ASM_REWRITE_TAC[CONTINUOUS_ON_CONST];
       ALL_TAC
     ] THEN

     CONJ_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN

     CONJ_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN
         REWRITE_TAC[projection; VECTOR_SUB_LDISTRIB; NORM_POW_2; real_div; VECTOR_MUL_ASSOC; VECTOR_SUB_RDISTRIB] THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN

     CONJ_TAC THENL
     [
       REPEAT GEN_TAC THEN
         REWRITE_TAC[DIST_EQ] THEN
         ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ; PROJECTION_LINEAR; PROJECTION_ZERO] THEN
         ASM_REWRITE_TAC[VECTOR_MUL_RZERO; DIST_0] THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     REPEAT STRIP_TAC THEN
     REWRITE_TAC[] THEN
     MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
     ASM_SIMP_TAC[]);;




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

(* The main lemma: continuous intersection of [f(t),w] and aff_ge {0} {v1,v2} *)

let continuous_solution_aux = 
prove(`!a11 a12 a21 a22 f g t1 t2.
                                      f real_continuous_on real_interval [t1,t2] /\
                                      g real_continuous_on real_interval [t1,t2] /\
                                      ~(a11 * a22 - a12 * a21 = &0)
                                      ==> ?x1 x2. x1 real_continuous_on real_interval [t1,t2] /\
                                                  x2 real_continuous_on real_interval [t1,t2] /\
                                                  (!t. a11 * x1 t + a12 * x2 t = f t /\
                                                       a21 * x1 t + a22 * x2 t = g t /\
                                                       (!y1 y2. a11 * y1 + a12 * y2 = f t /\
                                                                a21 * y1 + a22 * y2 = g t ==> y1 = x1 t /\ y2 = x2 t))`,

   REPEAT STRIP_TAC THEN
     ABBREV_TAC `d = a11 * a22 - a12 * a21` THEN
     MAP_EVERY EXISTS_TAC [`\t. (a22 * (f:real->real) t - a12 * (g:real->real) t) * inv(d)`; `\t. (a11 * (g:real->real) t - a21 * (f:real->real) t) * inv d`] THEN
     REPEAT CONJ_TAC THENL
     [
       MATCH_MP_TAC REAL_CONTINUOUS_ON_RMUL THEN
         MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
         CONJ_TAC THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN ASM_REWRITE_TAC[];
       MATCH_MP_TAC REAL_CONTINUOUS_ON_RMUL THEN
         MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
         CONJ_TAC THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     GEN_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     BETA_TAC THEN
     CONV_TAC REAL_FIELD);;


let continuous_intersection_point = 
prove(`!v1 v2 n (f:real^1->real^3) w t1.
                                            ~collinear {vec 0,v1,v2} /\
                                            f continuous_on interval [lift (&0), lift (t1)] /\ &0 <= t1 /\
                                            v1 dot n = &0 /\ v2 dot n = &0 /\
                                            &0 < w dot n /\
                                            (!t. &0 <= t /\ t <= t1 ==> f (lift t) dot n <= &0)
                                            ==> (?a b. a real_continuous_on real_interval [&0, t1] /\
                                                       b real_continuous_on real_interval [&0, t1] /\
                                                       (!t. &0 <= t /\ t <= t1 ==> segment [f (lift t),w] INTER affine hull {vec 0,v1,v2} = {a t % v1 + b t % v2}))`,

   REPEAT STRIP_TAC THEN
     ABBREV_TAC `u0 = (\t. --((f o lift) t dot n:real^3) / (w dot n - ((f o lift) t dot n)))` THEN
     ABBREV_TAC `f1 = (\t. ((f o lift) t dot v1:real^3) + u0 t * (w - (f o lift) t) dot v1)` THEN
     ABBREV_TAC `f2 = (\t. ((f o lift) t dot v2:real^3) + u0 t * (w - (f o lift) t) dot v2)` THEN
     MP_TAC (SPECL [`v1 dot v1:real^3`; `v1 dot v2:real^3`; `v1 dot v2:real^3`; `v2 dot v2:real^3`; `f1:real->real`; `f2:real->real`; `&0`; `t1:real`] continuous_solution_aux) THEN
     ANTS_TAC THENL
     [
       SUBGOAL_THEN `!v:real^3. (\t. (f o lift) t dot v) real_continuous_on real_interval [&0,t1]` ASSUME_TAC THENL
         [
           GEN_TAC THEN REWRITE_TAC[REAL_CONTINUOUS_ON] THEN
             SUBGOAL_THEN `lift o (\t. (f o lift) t dot v:real^3) o drop = (lift o (\y. v dot y)) o f` (fun th -> REWRITE_TAC[th]) THENL
             [
               REWRITE_TAC[FUN_EQ_THM; o_THM; DOT_SYM; LIFT_DROP];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
             ASM_REWRITE_TAC[IMAGE_LIFT_REAL_INTERVAL; CONTINUOUS_ON_LIFT_DOT];
           ALL_TAC
         ] THEN

         SUBGOAL_THEN `u0 real_continuous_on real_interval[&0,t1]` ASSUME_TAC THENL
         [
           EXPAND_TAC "u0" THEN
             REWRITE_TAC[real_div] THEN
             MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
             CONJ_TAC THENL [ MATCH_MP_TAC REAL_CONTINUOUS_ON_NEG THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
             REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
             REPEAT STRIP_TAC THEN
             MATCH_MP_TAC REAL_CONTINUOUS_INV_WITHINREAL THEN
             CONJ_TAC THENL
             [
               POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real`, `x:real`) THEN
                 ONCE_REWRITE_TAC[GSYM REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
                 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
             REWRITE_TAC[REAL_ARITH `a - b = a + (--b)`] THEN
             MATCH_MP_TAC REAL_LTE_ADD THEN
             ASM_REWRITE_TAC[] THEN
             FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
             ASM_REWRITE_TAC[GSYM IN_REAL_INTERVAL; o_THM] THEN
             REAL_ARITH_TAC;
           ALL_TAC
         ] THEN

         CONJ_TAC THENL
         [
           EXPAND_TAC "f1" THEN
             MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
             ASM_REWRITE_TAC[] THEN
             MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
             ASM_REWRITE_TAC[VECTOR_ARITH `(w - f) dot v = w dot v - f dot v:real^3`] THEN
             MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
             ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
           ALL_TAC
         ] THEN

         CONJ_TAC THENL
         [
           EXPAND_TAC "f2" THEN
             MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
             ASM_REWRITE_TAC[] THEN
             MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
             ASM_REWRITE_TAC[VECTOR_ARITH `(w - f) dot v = w dot v - f dot v:real^3`] THEN
             MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
             ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
           ALL_TAC
         ] THEN

         REWRITE_TAC[REAL_ARITH `v11 * v22 - v12 * v12 = &0 <=> v12 pow 2 = v11 * v22`] THEN
         ASM_REWRITE_TAC[DOT_CAUCHY_SCHWARZ_EQUAL];
       ALL_TAC
     ] THEN

     STRIP_TAC THEN
     MAP_EVERY EXISTS_TAC [`x1:real->real`; `x2:real->real`] THEN
     ASM_REWRITE_TAC[] THEN
     GEN_TAC THEN DISCH_TAC THEN

     REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `t:real`)) THEN
     ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN

     REWRITE_TAC [SET_RULE `!s (x:A). s = {x} <=> (?x. x IN s) /\ (!y. y IN s ==> y = x)`] THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC intersection_point_exists THEN
         EXISTS_TAC `n:real^3` THEN ASM_REWRITE_TAC[] THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
         DISCH_TAC THEN
         UNDISCH_TAC `&0 < w dot n:real^3` THEN
         ASM_REWRITE_TAC[DOT_RZERO; REAL_LT_REFL];
       ALL_TAC
     ] THEN

     GEN_TAC THEN REWRITE_TAC[IN_INTER; IN_SEGMENT; AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
     STRIP_TAC THEN
     SUBGOAL_THEN `u:real = u0 (t:real)` ASSUME_TAC THENL
     [
       UNDISCH_TAC `y:real^3 = (&1 - u) % f (lift t) + u % w` THEN
         DISCH_THEN (MP_TAC o AP_TERM `(\y:real^3. y dot n)`) THEN
         FIRST_X_ASSUM (fun th -> REWRITE_TAC[th]) THEN
         ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
         EXPAND_TAC "u0" THEN
         REWRITE_TAC[o_THM] THEN
         SUBGOAL_THEN `&0 < w:real^3 dot n - f (lift t) dot n` MP_TAC THENL
         [
           REWRITE_TAC[REAL_ARITH `a - b = a + (--b)`] THEN
             MATCH_MP_TAC REAL_LTE_ADD THEN
             ASM_REWRITE_TAC[REAL_ARITH `&0 <= --a <=> a <= &0`];
           ALL_TAC
         ] THEN
         CONV_TAC REAL_FIELD;
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `v:real = x1 (t:real) /\ w':real = x2 t` ASSUME_TAC THENL
     [
       FIRST_X_ASSUM MATCH_MP_TAC THEN
         REWRITE_TAC[VECTOR_ARITH `(v1 dot v1) * v + (v1 dot v2:real^3) * w' = (v % v1 + w' % v2) dot v1`] THEN
         REWRITE_TAC[VECTOR_ARITH `(v1 dot v2) * v + (v2 dot v2:real^3) * w' = (v % v1 + w' % v2) dot v2`] THEN
         EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN
         POP_ASSUM (fun th -> REWRITE_TAC[SYM th; o_THM]) THEN
         POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
         ASM_REWRITE_TAC[] THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN
     UNDISCH_TAC `y:real^3 = v % v1 + w' % v2` THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     ASM_REWRITE_TAC[]);;


let in_aff_ge_cases_lemma = 
prove(`!v1 v2 v w:real^N. ~collinear {vec 0,v1,v2} /\ ~(between (vec 0) (v,w)) /\
                                    v IN affine hull {vec 0,v1,v2} /\ w IN aff_ge {vec 0} {v1,v2}
                                      ==> v IN aff_ge {vec 0} {v1,v2} \/
                                          v1 IN aff_ge {vec 0} {v,w} \/
                                          v2 IN aff_ge {vec 0} {v,w}`,

   REPEAT STRIP_TAC THEN
     UNDISCH_TAC `~collinear {vec 0, v1, v2:real^N}` THEN DISCH_TAC THEN
     FIRST_ASSUM MP_TAC THEN REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN DISCH_TAC THEN
     FIRST_X_ASSUM (MP_TAC o MATCH_MP zero_not_between) THEN
     STRIP_TAC THEN

     ASM_CASES_TAC `v:real^N IN aff_ge {vec 0} {v1,v2}` THEN ASM_REWRITE_TAC[] THEN
     SUBGOAL_THEN `?t1 t2. v:real^N = t1 % v1 + t2 % v2 /\ (t1 < &0 \/ t2 < &0)` MP_TAC THENL
     [
       UNDISCH_TAC `v IN affine hull {vec 0, v1, v2:real^N}` THEN
         POP_ASSUM MP_TAC THEN
         REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
         ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; NOT_EXISTS_THM] THEN
         DISCH_TAC THEN STRIP_TAC THEN
         MAP_EVERY EXISTS_TAC [`v':real`; `w':real`] THEN
         ASM_REWRITE_TAC[] THEN
         FIRST_X_ASSUM (MP_TAC o SPECL [`v':real`; `w':real`]) THEN
         REWRITE_TAC[DE_MORGAN_THM; REAL_NOT_LE] THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC)) THEN
     DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "v" o SYM) ASSUME_TAC) THEN

     SUBGOAL_THEN `?t3 t4. w:real^N = t3 % v1 + t4 % v2 /\ &0 <= t3 /\ &0 <= t4` MP_TAC THENL
     [
       UNDISCH_TAC `w:real^N IN aff_ge {vec 0} {v1,v2}` THEN
         ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
         STRIP_TAC THEN
         MAP_EVERY EXISTS_TAC [`t1':real`; `t2':real`] THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC)) THEN
     DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "w" o SYM) ASSUME_TAC) THEN

     SUBGOAL_THEN `~(v = vec 0:real^N)` ASSUME_TAC THENL
     [
       ASM_CASES_TAC `v = vec 0:real^N` THEN ASM_REWRITE_TAC[] THEN
         UNDISCH_TAC `~(v IN aff_ge {vec 0} {v1,v2:real^N})` THEN
         ASM_REWRITE_TAC[points_in_aff_ge_0_2];
       ALL_TAC
     ] THEN

     ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
     ASM_CASES_TAC `t3 = &0` THENL
     [
       REMOVE_THEN "w" (MP_TAC o SYM) THEN
         ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
         ASM_CASES_TAC `t4 = &0` THENL [ ASM_REWRITE_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
         DISCH_THEN (MP_TAC o AP_TERM `\w:real^N. inv(t4) % w`) THEN
         ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
         DISCH_TAC THEN
         DISJ2_TAC THEN
         MAP_EVERY EXISTS_TAC [`&0`; `inv t4`] THEN
         ASM_SIMP_TAC[REAL_LE_INV; REAL_LE_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID];
       ALL_TAC
     ] THEN
     ASM_CASES_TAC `t4 = &0` THENL
     [
       REMOVE_THEN "w" (MP_TAC o SYM) THEN
         ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
         DISCH_THEN (MP_TAC o AP_TERM `\w:real^N. inv(t3) % w`) THEN
         ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
         DISCH_THEN (ASSUME_TAC o SYM) THEN
         DISJ1_TAC THEN
         MAP_EVERY EXISTS_TAC [`&0`; `inv t3`] THEN
         ASM_SIMP_TAC[REAL_LE_INV; REAL_LE_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `&0 < t3 /\ &0 < t4` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `~(t2 * t3 - t1 * t4 = &0)` ASSUME_TAC THENL
     [
       REWRITE_TAC[REAL_ARITH `a - b = &0 <=> a = b`] THEN
         ASM_CASES_TAC `t1 < &0` THENL
         [
           DISCH_TAC THEN
             REMOVE_THEN "w" (MP_TAC o AP_TERM `(\x:real^N. t1 % x)`) THEN
             ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_AC] THEN
             POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
             ONCE_REWRITE_TAC[REAL_MUL_AC] THEN
             ONCE_REWRITE_TAC[GSYM VECTOR_MUL_ASSOC] THEN
             ONCE_REWRITE_TAC[GSYM VECTOR_ADD_LDISTRIB] THEN
             ASM_SIMP_TAC[];
           ALL_TAC
         ] THEN
         SUBGOAL_THEN `t2 < &0` ASSUME_TAC THENL
         [
           UNDISCH_TAC `t1 < &0 \/ t2 < &0` THEN
             POP_ASSUM MP_TAC THEN
             SIMP_TAC[];
           ALL_TAC
         ] THEN

         DISCH_TAC THEN
         REMOVE_THEN "w" (MP_TAC o AP_TERM `(\x:real^N. t2 % x)`) THEN
         ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_AC] THEN
         ONCE_REWRITE_TAC[REAL_MUL_AC] THEN
         ONCE_REWRITE_TAC[GSYM VECTOR_MUL_ASSOC] THEN
         ASM_REWRITE_TAC[GSYM VECTOR_ADD_LDISTRIB] THEN
         ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     ABBREV_TAC `d:real = t2 * t3 - t1 * t4` THEN
     SUBGOAL_THEN `v2:real^N = inv(d) % (t3 % v + (--t1) % w)` ASSUME_TAC THENL
     [
       MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
         EXISTS_TAC `d:real` THEN
         ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV; VECTOR_MUL_LID] THEN
         REMOVE_THEN "w" (MP_TAC o AP_TERM `\w:real^N. (--t1) % w`) THEN
         REMOVE_THEN "v" (MP_TAC o AP_TERM `\v:real^N. t3 % v`) THEN
         BETA_TAC THEN EXPAND_TAC "d" THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `v1:real^N = --inv(d) % (t4 % v + (--t2) % w)` ASSUME_TAC THENL
     [
       MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
         EXISTS_TAC `d:real` THEN
         ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RNEG; REAL_MUL_RINV] THEN
         REMOVE_THEN "w" (MP_TAC o AP_TERM `\w:real^N. t2 % w`) THEN
         REMOVE_THEN "v" (MP_TAC o AP_TERM `\v:real^N. t4 % v`) THEN
         BETA_TAC THEN EXPAND_TAC "d" THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN

     ASM_CASES_TAC `t1 < &0` THENL
     [
       ASM_CASES_TAC `t2 < &0` THENL
         [
           ASM_CASES_TAC `d < &0` THENL
             [
               DISJ1_TAC THEN
                 MAP_EVERY EXISTS_TAC [`(--inv d) * t4`; `(--inv d) * (--t2)`] THEN
                 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
                 REWRITE_TAC[GSYM REAL_INV_NEG] THEN
                 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THENL
                 [
                   ASM_REWRITE_TAC[] THEN
                     MATCH_MP_TAC REAL_LE_INV THEN
                     ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
                   ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE] THEN
                     MATCH_MP_TAC REAL_LE_INV THEN
                     ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE]
                 ];
               ALL_TAC
             ] THEN
             POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
             DISJ2_TAC THEN
             MAP_EVERY EXISTS_TAC [`inv d * t3`; `inv d * (--t1)`] THEN
             ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
             CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
         SUBGOAL_THEN `&0 <= inv d` ASSUME_TAC THENL
         [
           EXPAND_TAC "d" THEN
             MATCH_MP_TAC REAL_LE_INV THEN
             REWRITE_TAC[REAL_ARITH `a - t1 * t4 = a + (--t1) * t4`] THEN
             MATCH_MP_TAC REAL_LE_ADD THEN
             CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
           ALL_TAC
         ] THEN

         DISJ2_TAC THEN
         MAP_EVERY EXISTS_TAC [`inv d * t3`; `inv d * (--t1)`] THEN
         ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
         CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `&0 <= t1 /\ t2 < &0` ASSUME_TAC THENL
     [
       UNDISCH_TAC `t1 < &0 \/ t2 < &0` THEN
         ASM_REWRITE_TAC[GSYM REAL_NOT_LT];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `&0 <= --inv d` ASSUME_TAC THENL
     [
       REWRITE_TAC[GSYM REAL_INV_NEG] THEN
         EXPAND_TAC "d" THEN
         MATCH_MP_TAC REAL_LE_INV THEN
         REWRITE_TAC[REAL_ARITH `--(t2 * t3 - t1 * t4) = (--t2) * t3 + t1 * t4`] THEN
         MATCH_MP_TAC REAL_LE_ADD THEN
         CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
       ALL_TAC
     ] THEN

     DISJ1_TAC THEN
     MAP_EVERY EXISTS_TAC [`--inv d * t4`; `--inv d * (--t2)`] THEN
     ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
     CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE]);;


let segment_intersects_aff_ge_lemma = 
prove(`!v1 v2 v w:real^N. ~collinear {vec 0,v1,v2} /\ ~between (vec 0) (v,w) /\
                                              v IN affine hull {vec 0,v1,v2} /\ w IN affine hull {vec 0,v1,v2} /\
                                              ~(segment [v,w] INTER aff_ge {vec 0} {v1,v2} = {})
                                              ==> v IN aff_ge {vec 0} {v1,v2} \/
                                                  v1 IN aff_ge {vec 0} {v,w} \/
                                                  v2 IN aff_ge {vec 0} {v,w}`,

   REPEAT STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
     DISCH_THEN (X_CHOOSE_THEN `p:real^N` MP_TAC) THEN
     REWRITE_TAC[IN_INTER] THEN DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN DISCH_TAC THEN
     FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN_SEGMENT] THEN STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     ASM_CASES_TAC `u = &0` THENL
     [
       ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_RID] THEN
         DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]);
       ALL_TAC
     ] THEN
     DISCH_THEN (LABEL_TAC "p" o SYM) THEN

     FIRST_ASSUM (MP_TAC o MATCH_MP zero_not_between) THEN
     STRIP_TAC THEN

     MP_TAC (SPECL [`v1:real^N`; `v2:real^N`; `v:real^N`; `p:real^N`] in_aff_ge_cases_lemma) THEN
     ASM_REWRITE_TAC[] THEN

     ANTS_TAC THENL
     [
       REWRITE_TAC[BETWEEN_IN_SEGMENT] THEN DISCH_TAC THEN
         UNDISCH_TAC `~between (vec 0:real^N) (v,w)` THEN
         REWRITE_TAC[BETWEEN_IN_SEGMENT] THEN
         MATCH_MP_TAC Hypermap.lemma_in_subset THEN
         EXISTS_TAC `segment [v,p:real^N]` THEN
         ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `p IN aff_ge {vec 0:real^N} {v,w}` ASSUME_TAC THENL
     [
       MATCH_MP_TAC in_segment_imp_in_aff_ge_0_2 THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
     [
       DISJ2_TAC THEN DISJ1_TAC THEN
         MATCH_MP_TAC Hypermap.lemma_in_subset THEN
         EXISTS_TAC `aff_ge {vec 0} {v:real^N,p}` THEN
         ASM_REWRITE_TAC[] THEN
         MATCH_MP_TAC aff_ge_0_2_SUBSET THEN
         ASM_REWRITE_TAC[points_in_aff_ge_0_2];
       ALL_TAC
     ] THEN
     DISJ2_TAC THEN DISJ2_TAC THEN
     MATCH_MP_TAC Hypermap.lemma_in_subset THEN
     EXISTS_TAC `aff_ge {vec 0} {v:real^N,p}` THEN
     ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC aff_ge_0_2_SUBSET THEN
     ASM_REWRITE_TAC[points_in_aff_ge_0_2]);;



(* The main lemma *)

let continuous_lemma_aff_ge = 
prove(`!v1 v2 (f:real^1->real^3) w h. &0 <= h /\
                                      f continuous_on interval [lift (&0), lift h] /\
                                      ~(segment [f (lift (&0)), w] INTER aff_ge {vec 0} {v1,v2} = {}) /\
                                      (!t. t IN interval [lift (&0), lift h] ==> ~between (vec 0) (f t, w)) /\
                                      ~collinear {vec 0,v1,v2}
                                      ==> (!t. t IN interval [lift (&0), lift h] ==> ~(segment [f t, w] INTER aff_ge {vec 0} {v1,v2} = {})) \/
                                          (?x. &0 <= x /\ x <= h /\
                                             (!t. t IN interval [lift (&0), lift x] ==> ~(segment [f t, w] INTER aff_ge {vec 0} {v1,v2} = {})) /\
                                             (f (lift x) IN aff_ge {vec 0} {v1,v2} \/ v1 IN aff_ge {vec 0} {f (lift x), w} \/ v2 IN aff_ge {vec 0} {f (lift x), w}))`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `!y b. (lift y) IN interval [lift (&0), lift b] <=> &0 <= y /\ y <= b` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[IN_INTERVAL_1];
       ALL_TAC
     ] THEN

     (* Aux *)
     SUBGOAL_THEN `lift (&0) IN interval [lift (&0), lift h]` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
       ALL_TAC
     ] THEN

     (* v1, v2, w != 0 *)
     SUBGOAL_THEN `~(v1:real^3 = vec 0) /\ ~(v2:real^3 = vec 0) /\ ~(w:real^3 = vec 0)` ASSUME_TAC THENL
     [
       UNDISCH_TAC `~collinear {vec 0,v1,v2:real^3}` THEN
         SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN DISCH_TAC THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `lift (&0)`) THEN
         ASM_REWRITE_TAC[] THEN
         DISCH_THEN (MP_TAC o MATCH_MP zero_not_between) THEN
         SIMP_TAC[];
       ALL_TAC
     ] THEN

     (* ~between (vec 0) (f(t), w) expanded *)
     SUBGOAL_THEN `!t. &0 <= t /\ t <= h ==> ~(f (lift t) = vec 0) /\ (!u. &0 <= u /\ u <= &1 ==> ~((&1 - u) % f (lift t) + u % w = vec 0:real^3))` (LABEL_TAC "fw") THENL
     [
       GEN_TAC THEN DISCH_TAC THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `lift t`) THEN
         ASM_REWRITE_TAC[IN_INTERVAL_1] THEN
         DISCH_THEN (MP_TAC o MATCH_MP zero_not_between) THEN
         STRIP_TAC THEN
         ASM_REWRITE_TAC[] THEN

         GEN_TAC THEN DISCH_TAC THEN
         ASM_CASES_TAC `u = &0` THENL
         [
           ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
           ALL_TAC
         ] THEN
         ASM_CASES_TAC `u = &1` THENL
         [
           ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID];
           ALL_TAC
         ] THEN
         FIRST_X_ASSUM (MP_TAC o SPECL [`--u:real`; `&1 - u`]) THEN
         ANTS_TAC THENL
         [
           REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
           ALL_TAC
         ] THEN
         REWRITE_TAC[VECTOR_ARITH `--u % (w:real^N) = (&1 - u) % x <=> (&1 - u) % x + u % w = vec 0`];
       ALL_TAC
     ] THEN

     (* First case *)
     ASM_CASES_TAC `!t. t IN interval [lift (&0),lift h] ==> ~(segment [f t,w] INTER aff_ge {vec 0} {v1,v2:real^3} = {})` THEN ASM_REWRITE_TAC[] THEN
     POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN
     REWRITE_TAC[TAUT `~(A ==> ~B) <=> A /\ B`] THEN
     DISCH_THEN (X_CHOOSE_THEN `t1:real^1` (LABEL_TAC "A")) THEN

     (* Find a normal vector to the plane of aff_ge {vec 0} {v1,v2} *)
     SUBGOAL_THEN `?n:real^3. ~(n = vec 0) /\ v1 dot n = &0 /\ v2 dot n = &0 /\ f (lift (&0)) dot n <= &0` MP_TAC THENL
     [
       ASM_CASES_TAC `f (lift (&0)) dot (v1:real^3 cross v2) <= &0` THENL
         [
           EXISTS_TAC `v1 cross v2` THEN
             ASM_REWRITE_TAC[CROSS_EQ_0; DOT_CROSS_SELF];
           ALL_TAC
         ] THEN
         EXISTS_TAC `--(v1 cross v2)` THEN
         ASM_REWRITE_TAC[VECTOR_NEG_EQ_0; CROSS_EQ_0; DOT_RNEG; DOT_CROSS_SELF] THEN
         POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
       ALL_TAC
     ] THEN
     STRIP_TAC THEN

     (* Aux *)
     SUBGOAL_THEN `!p. p IN aff_ge {vec 0} {v1,v2:real^3} ==> p dot n = &0` ASSUME_TAC THENL
     [
       GEN_TAC THEN ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
         STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID];
       ALL_TAC
     ] THEN

     (* Need for the next two cases *)
     UNDISCH_TAC `~(segment [f (lift (&0)), w] INTER aff_ge {vec 0:real^3} {v1,v2} = {})` THEN DISCH_TAC THEN
     FIRST_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
     DISCH_THEN (X_CHOOSE_THEN `p:real^3` (LABEL_TAC "B")) THEN
     FIRST_ASSUM (MP_TAC o REWRITE_RULE [IN_INTER; IN_SEGMENT]) THEN
     DISCH_THEN (CONJUNCTS_THEN2 (X_CHOOSE_THEN `up:real` MP_TAC) ASSUME_TAC) THEN
     GEN_REWRITE_TAC LAND_CONV [CONJ_ASSOC] THEN
     DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "p1" o SYM)) THEN
     FIRST_ASSUM (MP_TAC o SPEC `p:real^3`) THEN
     FIRST_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[th])) THEN DISCH_TAC THEN

     (* w dot n < 0 *)
     DISJ_CASES_TAC (REAL_ARITH `w:real^3 dot n < &0 \/ w dot n = &0 \/ &0 < w dot n`) THENL
     [
       SUBGOAL_THEN `up = &0` ASSUME_TAC THENL
         [
           REMOVE_THEN "p1" (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
             ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
             ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
             DISCH_TAC THEN
             MATCH_MP_TAC (REAL_ARITH `&0 < --a ==> ~(a = &0)`) THEN
             REWRITE_TAC[REAL_ARITH `--(a * b + c * d) = a * (--b) + c * (--d)`] THEN
             MATCH_MP_TAC REAL_LET_ADD THEN
             CONJ_TAC THENL
             [
               MATCH_MP_TAC REAL_LE_MUL THEN
                 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - up <=> up <= &1`; REAL_NEG_GE0];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC REAL_LT_MUL THEN
             ASM_REWRITE_TAC[REAL_ARITH `&0 < up <=> &0 <= up /\ ~(up = &0)`; REAL_NEG_GT0];
           ALL_TAC
         ] THEN

         REMOVE_THEN "p1" MP_TAC THEN
         ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_LID] THEN
         DISCH_TAC THEN
         EXISTS_TAC `&0` THEN
         ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; INTERVAL_SING; IN_SING] THEN
         GEN_TAC THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     (* w dot n = 0 *)
     FIRST_X_ASSUM DISJ_CASES_TAC THENL
     [
       ASM_CASES_TAC `w:real^3 IN aff_ge {vec 0} {v1,v2}` THENL
         [
           SUBGOAL_THEN `~(segment [f (t1:real^1),w] INTER aff_ge {vec 0} {v1,v2:real^3} = {})` MP_TAC THENL
             [
               REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
                 EXISTS_TAC `w:real^3` THEN
                 REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT] THEN POP_ASSUM (fun th -> REWRITE_TAC[th]);
               ALL_TAC
             ] THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         EXISTS_TAC `&0` THEN
         ASM_REWRITE_TAC[REAL_LE_REFL; INTERVAL_SING; IN_SING] THEN
         CONJ_TAC THENL
         [
           GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
             EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         MATCH_MP_TAC segment_intersects_aff_ge_lemma THEN
         ASM_REWRITE_TAC[] THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `lift (&0)`) THEN
         ASM_REWRITE_TAC[] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN

         ASM_SIMP_TAC[affine_hull_3_plane] THEN
         ASM_REWRITE_TAC[IN_ELIM_THM] THEN
         SUBGOAL_THEN `~(up = &1)` ASSUME_TAC THENL
         [
           POP_ASSUM MP_TAC THEN REWRITE_TAC[CONTRAPOS_THM] THEN DISCH_TAC THEN
             REMOVE_THEN "p1" MP_TAC THEN ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
             ASM_SIMP_TAC[];
           ALL_TAC
         ] THEN

         REMOVE_THEN "p1" (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
         ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO] THEN
         POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD;
       ALL_TAC
     ] THEN

     (* Remove unnessary assumptions before considering the last case *)
     POP_ASSUM MP_TAC THEN REPLICATE_TAC 5 REMOVE_ASSUM THEN DISCH_TAC THEN

     (* w dot n > 0 *)

     (* Consider two major cases: f(t) intersects affine hull {vec 0,v1,v2} at some point or not *)
     SUBGOAL_THEN `?r. &0 <= r /\ r <= h /\
                       (!t. &0 <= t /\ t <= r ==> f (lift t) dot (n:real^3) <= &0) /\
                       (((!t. &0 <= t /\ t <= r ==> ~(segment [f (lift t), w] INTER aff_ge {vec 0} {v1,v2} = {})) /\ f (lift r) IN aff_ge {vec 0} {v1, v2}) \/
                          (?t1. &0 <= t1 /\ t1 <= r /\ segment [f (lift t1), w] INTER aff_ge {vec 0} {v1,v2} = {}))` MP_TAC THENL
     [
       ASM_CASES_TAC `!t. &0 <= t /\ t <= h ==> f (lift t) dot (n:real^3) <= &0` THENL
         [
           EXISTS_TAC `h:real` THEN
             ASM_REWRITE_TAC[REAL_LE_REFL] THEN
             DISJ2_TAC THEN
             EXISTS_TAC `drop (t1:real^1)` THEN
             ASM_REWRITE_TAC[LIFT_DROP] THEN
             FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t1:real^1)`; `h:real`]) THEN
             ASM_REWRITE_TAC[LIFT_DROP];
           ALL_TAC
         ] THEN

         POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN
         DISCH_THEN (X_CHOOSE_THEN `tt:real` MP_TAC) THEN
         REWRITE_TAC[TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
         DISCH_TAC THEN
         MP_TAC (SPECL [`\t:real. f (lift t) dot n:real^3`; `&0`; `tt:real`] continuous_lemma_inc) THEN
         ANTS_TAC THENL
         [
           ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
             REWRITE_TAC[REAL_CONTINUOUS_ON] THEN
             SUBGOAL_THEN `lift o (\t:real. f (lift t) dot n:real^3) o drop = (lift o (\y:real^3. n dot y)) o f` (fun th -> REWRITE_TAC[th]) THENL
             [
               REWRITE_TAC[FUN_EQ_THM; o_THM; LIFT_DROP; DOT_SYM];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
             REWRITE_TAC[IMAGE_LIFT_REAL_INTERVAL; CONTINUOUS_ON_LIFT_DOT] THEN
             MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
             EXISTS_TAC `interval [lift (&0), lift (h)]` THEN
             ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
           ALL_TAC
         ] THEN
         BETA_TAC THEN STRIP_TAC THEN
         EXISTS_TAC `x:real` THEN
         ASM_REWRITE_TAC[] THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `tt:real` THEN ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         CONJ_TAC THENL
         [
           REPEAT STRIP_TAC THEN
             ASM_CASES_TAC `t = x:real` THENL [ ASM_SIMP_TAC[REAL_ARITH `a = &0 ==> a <= &0`]; ALL_TAC ] THEN
             MATCH_MP_TAC REAL_LT_IMP_LE THEN
             FIRST_X_ASSUM MATCH_MP_TAC THEN
             ASM_REWRITE_TAC[REAL_LT_LE];
           ALL_TAC
         ] THEN

         ASM_CASES_TAC `?t1. &0 <= t1 /\ t1 <= x /\ segment [f (lift t1),w:real^3] INTER aff_ge {vec 0} {v1,v2} = {}` THEN ASM_REWRITE_TAC[] THEN
         POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_EXISTS_THM; DE_MORGAN_THM] THEN
         DISCH_TAC THEN
         SUBGOAL_THEN `!t. &0 <= t /\ t <= x ==> ~(segment [f (lift t),w:real^3] INTER aff_ge {vec 0} {v1,v2} = {})` ASSUME_TAC THENL
         [
           REPEAT STRIP_TAC THEN
             FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
             ASM_REWRITE_TAC[DE_MORGAN_THM];
           ALL_TAC
         ] THEN

         ASM_REWRITE_TAC[] THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
         ASM_REWRITE_TAC[REAL_LE_REFL; GSYM MEMBER_NOT_EMPTY] THEN
         DISCH_THEN (X_CHOOSE_THEN `p:real^3` MP_TAC) THEN
         REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
         STRIP_TAC THEN
         UNDISCH_TAC `p = (&1 - u) % f (lift x) + u % w:real^3` THEN DISCH_THEN (LABEL_TAC "p1" o SYM) THEN
         FIRST_ASSUM (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `p:real^3`) THEN
         ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         REWRITE_TAC[REAL_ENTIRE] THEN
         ASM_SIMP_TAC[REAL_ARITH `&0 < w dot n ==> ~(w:real^3 dot n = &0)`] THEN
         DISCH_TAC THEN
         REMOVE_THEN "p1" MP_TAC THEN
         ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID];
       ALL_TAC
     ] THEN


     (* Deal with two possible cases *)
     STRIP_TAC THENL
     [
       EXISTS_TAC `r:real` THEN
         ASM_REWRITE_TAC[] THEN
         REPEAT STRIP_TAC THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
         FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t:real^1)`; `r:real`]) THEN
         DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
         ASM_REWRITE_TAC[LIFT_DROP; MEMBER_NOT_EMPTY];
       ALL_TAC
     ] THEN

     (* The main case *)
     MP_TAC (SPECL [`v1:real^3`; `v2:real^3`; `n:real^3`; `f:real^1->real^3`; `w:real^3`; `r:real`] continuous_intersection_point) THEN
     ASM_REWRITE_TAC[] THEN
     ANTS_TAC THENL
     [
       MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
         EXISTS_TAC `interval [lift (&0), lift h]` THEN
         ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
       ALL_TAC
     ] THEN

     STRIP_TAC THEN

     (* Aux *)
     SUBGOAL_THEN `!t. &0 <= t /\ t <= r ==> a t % v1 + b t % v2:real^3 IN segment [f (lift t),w] INTER affine hull {vec 0,v1,v2}` (LABEL_TAC "a1") THENL
     [
       REPEAT STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
         ASM_REWRITE_TAC[EXTENSION; IN_SING; IN_INTER] THEN
         DISCH_THEN (MP_TAC o SPEC `a (t:real) % v1 + b t % v2:real^3`) THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     (* Aux *)
     SUBGOAL_THEN `!t. &0 <= t /\ t <= r ==> ?u. &0 <= u /\ u <= &1 /\ a t % v1 + b t % v2 = (&1 - u) % f (lift t) + u % w:real^3` (LABEL_TAC "a2") THENL
     [
       REPEAT STRIP_TAC THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
         ASM_REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
         STRIP_TAC THEN
         EXISTS_TAC `u:real` THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     (* Aux *)
     SUBGOAL_THEN `!t. &0 <= t /\ t <= r /\ &0 <= a t /\ &0 <= b t ==> (?x. x IN segment [f (lift t),w:real^3] INTER aff_ge {vec 0} {v1,v2})` (LABEL_TAC "a3") THENL
     [
       REPEAT STRIP_TAC THEN
         EXISTS_TAC `a (t:real) % (v1:real^3) + b t % v2` THEN
         REWRITE_TAC[IN_INTER] THEN
         REMOVE_THEN "a1" (MP_TAC o SPEC `t:real`) THEN
         ASM_SIMP_TAC[IN_INTER] THEN DISCH_TAC THEN
         ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
         MAP_EVERY EXISTS_TAC [`(a:real->real) t`; `(b:real->real) t`] THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     (* Aux *)
     SUBGOAL_THEN `!t. &0 <= t /\ t <= r /\ ~(segment [f (lift t),w] INTER aff_ge {vec 0:real^3} {v1,v2} = {}) ==> &0 <= a t /\ &0 <= b t` (LABEL_TAC "a4") THENL
     [
       GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
         POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
         STRIP_TAC THEN
         SUBGOAL_THEN `x:real^3 IN segment [f (lift t),w] INTER affine hull {vec 0,v1,v2}` MP_TAC THENL
         [
           ASM_REWRITE_TAC[IN_INTER] THEN
             MATCH_MP_TAC Hypermap.lemma_in_subset THEN
             EXISTS_TAC `aff_ge {vec 0:real^3} {v1,v2}` THEN
             ASM_REWRITE_TAC[] THEN
             REWRITE_TAC[SET_RULE `{vec 0:real^3,v1,v2} = {vec 0} UNION {v1,v2}`] THEN
             REWRITE_TAC[AFF_GE_SUBSET_AFFINE_HULL];
           ALL_TAC
         ] THEN
         DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN
         FIRST_ASSUM (ASSUME_TAC o REWRITE_RULE[IN_INTER]) THEN
         MP_TAC (ISPECL [`v1:real^3`; `v2:real^3`; `x:real^3`] in_affine_hull_lemma) THEN
         ASM_REWRITE_TAC[] THEN
         REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN

         MAP_EVERY (fun s -> REMOVE_THEN s (fun th -> ALL_TAC)) ["a1";
 "a2"; "a3"] THEN
         FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
         ASM_REWRITE_TAC[] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         REWRITE_TAC[IN_SING] THEN
         DISCH_THEN (LABEL_TAC "x1" o SYM) THEN
         STRIP_TAC THEN
         FIRST_X_ASSUM (LABEL_TAC "x2" o SYM o check (is_eq o concl)) THEN
         UNDISCH_TAC `x IN aff_ge {vec 0} {v1,v2:real^3}` THEN
         MP_TAC (ISPECL [`v1:real^3`; `v2:real^3`] aff_ge_0_2) THEN
         ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th; IN_ELIM_THM]) THEN
         STRIP_TAC THEN
         SUBGOAL_THEN `a (t:real) = t1'':real /\ b (t:real) = t2:real` MP_TAC THENL
         [
           FIRST_X_ASSUM MATCH_MP_TAC THEN
             REMOVE_THEN "x1" (fun th -> REWRITE_TAC[th]);
           ALL_TAC
         ] THEN
         SUBGOAL_THEN `t1''' = t1'':real /\ t2' = t2:real` MP_TAC THENL
         [
           FIRST_X_ASSUM MATCH_MP_TAC THEN
             POP_ASSUM (fun th -> REWRITE_TAC[th]);
           ALL_TAC
         ] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     (* Aux *)
     SUBGOAL_THEN `&0 <= a (&0) /\ &0 <= b (&0)` (LABEL_TAC "a5") THENL
     [
       FIRST_X_ASSUM MATCH_MP_TAC THEN
         ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01];
       ALL_TAC
     ] THEN


     (* Cases for a(t) and b(t) *)
     SUBGOAL_THEN `?x. &0 <= x /\ x <= r /\ (!t. &0 <= t /\ t <= x ==> &0 <= a t /\ &0 <= b t) /\ (a x = &0 \/ b x = &0)` MP_TAC THENL
     [
       (* 0 <= a(t) for all t *)
       ASM_CASES_TAC `!t. &0 <= t /\ t <= r ==> &0 <= a t` THENL
         [
           MP_TAC (SPECL [`b:real->real`; `&0`; `t1':real`] continuous_lemma_dec) THEN
             ASM_REWRITE_TAC[] THEN
             ANTS_TAC THENL
             [
               CONJ_TAC THENL
                 [
                   MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
                     EXISTS_TAC `real_interval [&0,r]` THEN
                     ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
                   ALL_TAC
                 ] THEN
                 FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
                 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
                 REWRITE_TAC[REAL_NOT_LE; GSYM MEMBER_NOT_EMPTY] THEN
                 DISCH_TAC THEN
                 FIRST_X_ASSUM MATCH_MP_TAC THEN
                 ASM_SIMP_TAC[REAL_LT_IMP_LE];
               ALL_TAC
             ] THEN
             STRIP_TAC THEN

             EXISTS_TAC `x:real` THEN
             SUBGOAL_THEN `x <= r` ASSUME_TAC THENL
             [
               MATCH_MP_TAC REAL_LE_TRANS THEN
                 EXISTS_TAC `t1':real` THEN
                 ASM_REWRITE_TAC[];
               ALL_TAC
             ] THEN
             ASM_REWRITE_TAC[] THEN
             GEN_TAC THEN DISCH_TAC THEN
             CONJ_TAC THENL
             [
               FIRST_X_ASSUM MATCH_MP_TAC THEN
                 ASM_REWRITE_TAC[] THEN
                 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
                 ASM_REWRITE_TAC[];
               ALL_TAC
             ] THEN
             ASM_CASES_TAC `t = x:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
             MATCH_MP_TAC REAL_LT_IMP_LE THEN
             FIRST_X_ASSUM MATCH_MP_TAC THEN
             ASM_REWRITE_TAC[REAL_ARITH `t < x <=> t <= x /\ ~(t = x)`];
           ALL_TAC
         ] THEN

         (* a(ta) < 0 *)
         POP_ASSUM MP_TAC THEN
         REWRITE_TAC[NOT_FORALL_THM; TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
         DISCH_THEN (X_CHOOSE_THEN `ta:real` ASSUME_TAC) THEN

         MP_TAC (SPECL [`a:real->real`; `&0`; `ta:real`] continuous_lemma_dec) THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
         ANTS_TAC THENL
         [
           MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
             EXISTS_TAC `real_interval [&0,r]` THEN
             ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
           ALL_TAC
         ] THEN
         DISCH_THEN (X_CHOOSE_THEN `xa:real` MP_TAC) THEN
         STRIP_TAC THEN
         SUBGOAL_THEN `!t. &0 <= t /\ t <= xa ==> &0 <= a t` MP_TAC THENL
         [
           GEN_TAC THEN DISCH_TAC THEN
             ASM_CASES_TAC `t = xa:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
             MATCH_MP_TAC REAL_LT_IMP_LE THEN
             FIRST_X_ASSUM MATCH_MP_TAC THEN
             ASM_REWRITE_TAC[REAL_ARITH `t < xa <=> t <= xa /\ ~(t = xa)`];
           ALL_TAC
         ] THEN
         REMOVE_ASSUM THEN DISCH_TAC THEN

         (* 0 <= b(t) for all t *)
         ASM_CASES_TAC `!t. &0 <= t /\ t <= r ==> &0 <= b t` THENL
         [
           EXISTS_TAC `xa:real` THEN
             SUBGOAL_THEN `xa <= r` ASSUME_TAC THENL
             [
               MATCH_MP_TAC REAL_LE_TRANS THEN
                 EXISTS_TAC `ta:real` THEN
                 ASM_REWRITE_TAC[];
               ALL_TAC
             ] THEN
             ASM_REWRITE_TAC[] THEN
             GEN_TAC THEN DISCH_TAC THEN
             CONJ_TAC THENL
             [
               FIRST_X_ASSUM MATCH_MP_TAC THEN
                 ASM_REWRITE_TAC[];
               ALL_TAC
             ] THEN
             FIRST_X_ASSUM MATCH_MP_TAC THEN
             ASM_REWRITE_TAC[] THEN
             MATCH_MP_TAC REAL_LE_TRANS THEN
             EXISTS_TAC `xa:real` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         (* b(tb) < 0 *)
         POP_ASSUM MP_TAC THEN
         REWRITE_TAC[NOT_FORALL_THM; TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
         DISCH_THEN (X_CHOOSE_THEN `tb:real` ASSUME_TAC) THEN

         MP_TAC (SPECL [`b:real->real`; `&0`; `tb:real`] continuous_lemma_dec) THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
         ANTS_TAC THENL
         [
           MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
             EXISTS_TAC `real_interval [&0,r]` THEN
             ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
           ALL_TAC
         ] THEN
         DISCH_THEN (X_CHOOSE_THEN `xb:real` MP_TAC) THEN
         STRIP_TAC THEN
         SUBGOAL_THEN `!t. &0 <= t /\ t <= xb ==> &0 <= b t` MP_TAC THENL
         [
           GEN_TAC THEN DISCH_TAC THEN
             ASM_CASES_TAC `t = xb:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
             MATCH_MP_TAC REAL_LT_IMP_LE THEN
             FIRST_X_ASSUM MATCH_MP_TAC THEN
             ASM_REWRITE_TAC[REAL_ARITH `t < xa <=> t <= xa /\ ~(t = xa)`];
           ALL_TAC
         ] THEN
         REMOVE_ASSUM THEN DISCH_TAC THEN

         EXISTS_TAC `min xa xb` THEN
         ASM_REWRITE_TAC[REAL_LE_MIN] THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC REAL_LE_TRANS THEN
             EXISTS_TAC `xa:real` THEN
             REWRITE_TAC[REAL_MIN_MIN] THEN
             MATCH_MP_TAC REAL_LE_TRANS THEN
             EXISTS_TAC `ta:real` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         CONJ_TAC THENL
         [
           GEN_TAC THEN DISCH_TAC THEN
             CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         REWRITE_TAC[real_min] THEN
         COND_CASES_TAC THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     (* The final stage *)
     DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
     ONCE_REWRITE_TAC[TAUT `A /\ B /\ C /\ D <=> (A /\ B) /\ C /\ D`] THEN
     DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
     DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN

     EXISTS_TAC `x:real` THEN
     ASM_REWRITE_TAC[] THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC REAL_LE_TRANS THEN
         EXISTS_TAC `r:real` THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     CONJ_TAC THENL
     [
       GEN_TAC THEN
         FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t:real^1)`; `x:real`]) THEN
         REWRITE_TAC[LIFT_DROP] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         DISCH_TAC THEN
         REMOVE_THEN "a3" (MP_TAC o SPEC `drop (t:real^1)`) THEN
         ANTS_TAC THENL
         [
           ASM_REWRITE_TAC[] THEN
             CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
             FIRST_X_ASSUM MATCH_MP_TAC THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         SIMP_TAC[LIFT_DROP];
       ALL_TAC
     ] THEN

     (* The final case split: a x = 0 or b x = 0 *)
     POP_ASSUM DISJ_CASES_TAC THENL
     [
       DISJ2_TAC THEN DISJ2_TAC THEN
         REMOVE_THEN "fw" (MP_TAC o SPEC `x:real`) THEN
         ANTS_TAC THENL
         [
           ASM_REWRITE_TAC[] THEN
             MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         STRIP_TAC THEN
         ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
         REMOVE_THEN "a2" (MP_TAC o SPEC `x:real`) THEN
         ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
         STRIP_TAC THEN
         POP_ASSUM MP_TAC THEN
         ASM_CASES_TAC `b (x:real) = &0` THENL [ ASM_SIMP_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
         DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv ((b:real->real) x) % v`) THEN
         REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB] THEN
         ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
         DISCH_TAC THEN
         MAP_EVERY EXISTS_TAC [`inv (b (x:real)) * (&1 - u)`; `inv (b (x:real)) * u`] THEN
         REWRITE_TAC[] THEN
         SUBGOAL_THEN `&0 <= inv (b (x:real))` ASSUME_TAC THENL
         [
           MATCH_MP_TAC REAL_LE_INV THEN
             REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `x:real`)) THEN
             ASM_SIMP_TAC[REAL_LE_REFL];
           ALL_TAC
         ] THEN
         CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
       ALL_TAC
     ] THEN

     DISJ2_TAC THEN DISJ1_TAC THEN
     REMOVE_THEN "fw" (MP_TAC o SPEC `x:real`) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN
         MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN
     ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
     REMOVE_THEN "a2" (MP_TAC o SPEC `x:real`) THEN
     ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
     STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     ASM_CASES_TAC `a (x:real) = &0` THENL [ ASM_SIMP_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
     DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv ((a:real->real) x) % v`) THEN
     REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB] THEN
     ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
     DISCH_TAC THEN
     MAP_EVERY EXISTS_TAC [`inv (a (x:real)) * (&1 - u)`; `inv (a (x:real)) * u`] THEN
     REWRITE_TAC[] THEN
     SUBGOAL_THEN `&0 <= inv (a (x:real))` ASSUME_TAC THENL
     [
       MATCH_MP_TAC REAL_LE_INV THEN
         REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `x:real`)) THEN
         ASM_SIMP_TAC[REAL_LE_REFL];
       ALL_TAC
     ] THEN
     CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`]
);;




(* v1 and v3 in a 4-point configuration are separated by the plane affine hull {0,v2,v4} *)

let separation_plane_4_points = 
prove(`!v1 v2 v3 v4:real^3. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
                                        dist (v2, v4) <= &2 * h0 /\ dist (v1, v3) <= &2 * h0 /\ &2 <= dist (v2, v4) /\
                                        &2 <= dist (v1, v2) /\ &2 <= dist (v1, v4) /\
                                        &2 <= dist (v2, v3) /\ &2 <= dist (v3, v4) /\
                                        ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {})
                                          ==> ?n. ~(n = vec 0) /\ v2 dot n = &0 /\ v4 dot n = &0 /\
                                              v1 dot n < &0 /\ &0 < v3 dot n`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
     [
       REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
         SIMP_TAC[in_ball_annulus];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3}` ASSUME_TAC THENL
     [
       ASM_SIMP_TAC[estd_non_collinear_lemma];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `~between (vec 0) (v1:real^3,v3)` ASSUME_TAC THENL
     [
       ASM_SIMP_TAC[zero_not_between_estd];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `?n:real^3. ~(n = vec 0) /\ v2 dot n = &0 /\ v4 dot n = &0 /\ v1 dot n <= &0` MP_TAC THENL
     [
       ASM_CASES_TAC `v1 dot (v2 cross v4) <= &0` THENL
         [
           EXISTS_TAC `v2 cross v4` THEN
             ASM_REWRITE_TAC[CROSS_EQ_0; DOT_CROSS_SELF];
           ALL_TAC
         ] THEN
         EXISTS_TAC `--(v2 cross v4)` THEN
         ASM_REWRITE_TAC[VECTOR_NEG_EQ_0; CROSS_EQ_0; DOT_RNEG; DOT_CROSS_SELF] THEN
         POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
       ALL_TAC
     ] THEN
     STRIP_TAC THEN

     EXISTS_TAC `n:real^3` THEN
     SUBGOAL_THEN `~(v1 IN aff_ge {vec 0:real^3} {v2, v4}) /\ ~(v3 IN aff_ge {vec 0} {v2, v4})` ASSUME_TAC THENL
     [
       CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
         [
           MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `v1:real^3`];
           MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `v3:real^3`]
         ] THEN
         ASM_REWRITE_TAC[DIST_SYM];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `~(v2 IN aff_ge {vec 0:real^3} {v1, v3}) /\ ~(v4 IN aff_ge {vec 0:real^3} {v1, v3})` ASSUME_TAC THENL
     [
       CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
         [
           MAP_EVERY EXISTS_TAC [`v1:real^3`; `v3:real^3`; `v2:real^3`];
           MAP_EVERY EXISTS_TAC [`v1:real^3`; `v3:real^3`; `v4:real^3`]
         ] THEN
         ASM_REWRITE_TAC[DIST_SYM];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN
     ASM_CASES_TAC `v1 dot n:real^3 = &0` THENL
     [
       ASM_CASES_TAC `v3 dot n:real^3 = &0` THENL
         [
           MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v1:real^3`; `v3:real^3`] segment_intersects_aff_ge_lemma) THEN
             ANTS_TAC THENL
             [
               ASM_REWRITE_TAC[] THEN
                 ASM_SIMP_TAC[affine_hull_3_plane; IN_ELIM_THM];
               ALL_TAC
             ] THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN
         MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v1:real^3`; `v3:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     CONJ_TAC THENL [ ASM_REWRITE_TAC[REAL_LT_LE]; ALL_TAC ] THEN
     DISJ_CASES_TAC (REAL_ARITH `v3 dot n:real^3 < &0 \/ v3 dot n = &0 \/ &0 < v3 dot n`) THENL
     [
       UNDISCH_TAC `~(segment [v1:real^3,v3] INTER aff_ge {vec 0} {v2,v4} = {})` THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
         REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
         ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
         STRIP_TAC THEN
         POP_ASSUM (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
         ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
         ASM_CASES_TAC `u = &0` THEN ASM_REWRITE_TAC[] THENL
         [
           ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_MUL_LZERO; REAL_MUL_LID; REAL_ADD_RID];
           ALL_TAC
         ] THEN
         SUBGOAL_THEN `(&1 - u) * (v1 dot n:real^3) + u * (v3 dot n) < &0` MP_TAC THENL
         [
           REWRITE_TAC[REAL_ARITH `(&1 - u) * a + u * b < &0 <=> &0 < u * --b + (&1 - u) * --a`] THEN
             MATCH_MP_TAC REAL_LTE_ADD THEN
             CONJ_TAC THENL
             [
               MATCH_MP_TAC REAL_LT_MUL THEN
                 ASM_REWRITE_TAC[REAL_NEG_GT0; REAL_LT_LE];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC REAL_LE_MUL THEN
             ASM_REWRITE_TAC[REAL_NEG_GE0; REAL_LT_LE] THEN
             ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
           ALL_TAC
         ] THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     POP_ASSUM DISJ_CASES_TAC THENL
     [
       MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v3:real^3`; `v1:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
         ASM_REWRITE_TAC[SEGMENT_SYM];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[]);;




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



(* The first rotation lemma for a 4-point configuration *)
let lemma_4_points_rotation1 = 
prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
                                       dist (v1, v3) <= &2 * h0 /\ dist (v2, v4) <= &2 * h0 /\
                                       &2 <= dist (v1, v2) /\ &2 <= dist (v1, v4) /\
                                       &2 <= dist (v2, v3) /\ &2 <= dist (v3, v4) /\
                                       &2 <= dist (v2, v4) /\
                                       ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {})
                                       ==> (?v1'. v1' IN ball_annulus /\ norm v1' = norm v1 /\
                                              dist (v1', v3) <= &2 * h0 /\
                                              dist (v1', v2) = dist (v1, v2) /\ dist (v1', v4) = &2 /\
                                              ~(segment [v1',v3] INTER aff_ge {vec 0} {v2,v4} = {}))`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3}` ASSUME_TAC THENL
     [
       MATCH_MP_TAC estd_non_collinear_lemma THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
     [
       REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
         SIMP_TAC[in_ball_annulus];
       ALL_TAC
     ] THEN

     MP_TAC (SPEC_ALL separation_plane_4_points) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN

     MP_TAC (ISPECL [`v2:real^3`; `v1:real^3`; `v3:real^3`] rotation_about_axis) THEN
     ASM_REWRITE_TAC[DIMINDEX_3; LE_REFL; projection] THEN
     ANTS_TAC THENL
     [
       CONJ_TAC THEN DISCH_THEN (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN ASM_REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_LZERO; REAL_MUL_RZERO; REAL_SUB_RZERO] THENL
         [
           ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`];
           ASM_SIMP_TAC[REAL_LT_IMP_NE]
         ];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN

     SUBGOAL_THEN `!t. (f:real^1->real^3) t IN ball_annulus` ASSUME_TAC THENL
     [
       GEN_TAC THEN REWRITE_TAC[in_ball_annulus] THEN
         REWRITE_TAC[GSYM NORM_EQ_0] THEN
         SUBGOAL_THEN `norm ((f:real^1->real^3) t) = norm (v1:real^3)` (fun th -> REWRITE_TAC[th]) THENL
         [
           FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&0`]) THEN
             SIMP_TAC[VECTOR_MUL_LZERO; DIST_0];
           ALL_TAC
         ] THEN
         REWRITE_TAC[NORM_EQ_0] THEN
         REWRITE_TAC[GSYM in_ball_annulus] THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `&1`] continuous_lemma_aff_ge) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[REAL_LE_01] THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
             EXISTS_TAC `(:real^1)` THEN
             ASM_REWRITE_TAC[SUBSET_UNIV];
           ALL_TAC
         ] THEN
         GEN_TAC THEN DISCH_TAC THEN
         MATCH_MP_TAC zero_not_between_estd THEN
         ASM_REWRITE_TAC[] THEN
         MATCH_MP_TAC REAL_LE_TRANS THEN
         EXISTS_TAC `dist (v1:real^3,v3)` THEN
         ASM_REWRITE_TAC[] THEN
          FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
         ANTS_TAC THENL
         [
           POP_ASSUM MP_TAC THEN
             SUBGOAL_THEN `t = lift (drop (t:real^1))` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL
             [
               REWRITE_TAC[LIFT_DROP];
               ALL_TAC
             ] THEN
             REWRITE_TAC[IN_INTERVAL_1];
           ALL_TAC
         ] THEN
         REWRITE_TAC[LIFT_DROP];
       ALL_TAC
     ] THEN

     DISCH_THEN DISJ_CASES_TAC THENL
     [
       MATCH_MP_TAC (TAUT `F ==> A`) THEN
         POP_ASSUM (MP_TAC o SPEC `lift (&1)`) THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
         REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL; REAL_LE_01] THEN
         REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
         ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
         STRIP_TAC THEN
         POP_ASSUM (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN
         ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
         MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
         REWRITE_TAC[REAL_ARITH `(&1 - u) * a * b + u * b = b * (a * (&1 - u) + u)`] THEN
         MATCH_MP_TAC REAL_LT_MUL THEN
         ASM_REWRITE_TAC[] THEN
         ASM_CASES_TAC `u = &0` THENL
         [
           ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_MUL_RID; REAL_ADD_RID];
           ALL_TAC
         ] THEN
         MATCH_MP_TAC REAL_LET_ADD THEN
         ASM_REWRITE_TAC[REAL_LT_LE] THEN
         MATCH_MP_TAC REAL_LE_MUL THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN
     DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
     REWRITE_TAC[CONJ_ASSOC] THEN
     DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN

     SUBGOAL_THEN `!t. &2 <= dist (f (t:real^1), v2:real^3)` ASSUME_TAC THENL
     [
       GEN_TAC THEN
         FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&1`]) THEN
         ASM_SIMP_TAC[VECTOR_MUL_LID];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> dist (f (lift t),v3:real^3) <= &2 * h0` ASSUME_TAC THENL
     [
       REPEAT STRIP_TAC THEN
         MATCH_MP_TAC REAL_LE_TRANS THEN
         EXISTS_TAC `dist (v1:real^3, v3)` THEN
         ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `dist (f (lift x), v4:real^3) < &2` ASSUME_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o check (is_disj o concl)) THEN
         ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
         REWRITE_TAC[REAL_NOT_LT; DE_MORGAN_THM] THEN
         DISCH_TAC THEN

         REPEAT CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
         [
           MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
             ASM_REWRITE_TAC[DIST_SYM];
           MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
             ASM_SIMP_TAC[DIST_SYM];
           MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
             ASM_SIMP_TAC[];
         ];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL [`f:real^1->real^3`; `v4:real^3`; `x:real`; `&2`] dist_decreasing_ivt_lemma) THEN
     ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
     STRIP_TAC THEN
     EXISTS_TAC `(f:real^1->real^3) t` THEN

     SUBGOAL_THEN `!t:real^1. dist ((f t):real^3,v2) = dist (v1,v2)` ASSUME_TAC THENL
     [
       GEN_TAC THEN
         FIRST_X_ASSUM (MP_TAC o SPECL [`t':real^1`; `&1`]) THEN
         SIMP_TAC[VECTOR_MUL_LID];
       ALL_TAC
     ] THEN

     ASM_SIMP_TAC[] THEN
     CONJ_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&0`]) THEN
         SIMP_TAC[VECTOR_MUL_LZERO; DIST_0];
       ALL_TAC
     ] THEN

     FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
     ANTS_TAC THENL
     [
       REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP] THEN
         MATCH_MP_TAC Hypermap.lemma_in_subset THEN
         EXISTS_TAC `interval [lift (&0), lift x]` THEN
         ASM_REWRITE_TAC[SUBSET_INTERVAL] THEN
         REWRITE_TAC[DIMINDEX_1; ARITH_RULE `1 <= i /\ i <= 1 <=> i = 1`] THEN
         SIMP_TAC[] THEN
         ASM_REWRITE_TAC[GSYM drop; LIFT_DROP; REAL_LE_REFL];
       ALL_TAC
     ] THEN

     REWRITE_TAC[LIFT_DROP]);;



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


let lemma_4_points_rotation1_full = 
prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
                                            dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
                                            &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
                                            &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
                                            &2 <= dist (v2,v4) /\
                                            ~(segment [v1,v3] INTER aff_ge {vec 0} {v2, v4} = {})
                                            ==> (?v1' v3'. v1' IN ball_annulus /\ v3' IN ball_annulus /\
                                                   norm v1' = norm v1 /\ norm v3' = norm v3 /\
                                                   dist (v1',v3') <= &2 * h0 /\
                                                   dist (v1',v2) = &2 /\ dist (v1',v4) = &2 /\
                                                   dist (v2,v3') = &2 /\ dist (v3',v4) = &2 /\
                                                   ~(segment [v1',v3'] INTER aff_ge {vec 0} {v2, v4} = {}))`,

   REPEAT STRIP_TAC THEN
     (* v1 about v2 *)
     MP_TAC (SPEC_ALL lemma_4_points_rotation1) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     SUBGOAL_THEN `&2 <= dist (v1':real^3,v2)` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     UNDISCH_TAC `norm (v1':real^3) = norm (v1:real^3)` THEN
     REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v1:real^3` o concl))) THEN
     DISCH_TAC THEN

     (* v1 about v4 *)
     MP_TAC (SPECL [`v1':real^3`; `v4:real^3`; `v3:real^3`; `v2:real^3`] lemma_4_points_rotation1) THEN
     ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; Collect_geom.PER_SET2] THEN
     REMOVE_ASSUM THEN
     REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v1':real^3` o concl))) THEN
     DISCH_THEN (X_CHOOSE_THEN `v1':real^3` MP_TAC) THEN STRIP_TAC THEN

     (* v3 about v2 *)
     MP_TAC (SPECL [`v3:real^3`; `v2:real^3`; `v1':real^3`; `v4:real^3`] lemma_4_points_rotation1) THEN
     ASM_REWRITE_TAC[DIST_SYM; REAL_LE_REFL; SEGMENT_SYM] THEN
     DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN
     REWRITE_TAC[DIST_SYM] THEN STRIP_TAC THEN
     UNDISCH_TAC `norm (v3':real^3) = norm (v3:real^3)` THEN
     SUBGOAL_THEN `&2 <= dist (v2:real^3,v3')` ASSUME_TAC THENL
     [
       ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v3:real^3` o concl))) THEN
     DISCH_TAC THEN

     (* v3 about v4 *)
     MP_TAC (SPECL [`v3':real^3`; `v4:real^3`; `v1':real^3`; `v2:real^3`] lemma_4_points_rotation1) THEN
     ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; Collect_geom.PER_SET2; SEGMENT_SYM] THEN
     REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v3':real^3` o concl))) THEN
     DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN STRIP_TAC THEN

     MAP_EVERY EXISTS_TAC [`v1':real^3`; `v3':real^3`] THEN
     ASM_REWRITE_TAC[DIST_SYM; SEGMENT_SYM]);;


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


(* Auxiliary result for the second rotation lemma *)

let segment_inter_conv = 
prove(`!v1 v2 v3 v4 n:real^N. ~(v2 = vec 0) /\ ~(v4 = vec 0) /\ ~(v2 = v4) /\
                                 ~(projection (v4 - v2) (--v2) = vec 0) /\
                                 ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {}) /\
                                 v1 dot n < &0 /\ &0 < v3 dot n /\ v2 dot n = &0 /\ v4 dot n = &0 /\
                                 ~(segment [projection (v4 - v2) (v1 - v2), projection (v4 - v2) (v3 - v2)] INTER
                                     aff_ge {vec 0} {projection (v4 - v2) (--v2)} = {})
                                 ==> ~(segment [v1, v3] INTER convex hull {vec 0, v2, v4} = {})`,

    REPEAT STRIP_TAC THEN
      POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
      REWRITE_TAC[IN_SEGMENT; CONVEX_HULL_3_ALT; IN_INTER; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN

      UNDISCH_TAC `~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4:real^N} = {})` THEN
      REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_SEGMENT; IN_INTER] THEN
      ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
      REPEAT STRIP_TAC THEN
      EXISTS_TAC `x:real^N` THEN
      CONJ_TAC THENL
      [
        EXISTS_TAC `u:real` THEN
          ASM_REWRITE_TAC[];
        ALL_TAC
      ] THEN

      MAP_EVERY EXISTS_TAC [`t1:real`; `t2:real`] THEN
      FIRST_ASSUM (fun th -> REWRITE_TAC[th]) THEN
      ASM_REWRITE_TAC[] THEN

      ABBREV_TAC `d = v4 - v2:real^N` THEN
      ABBREV_TAC `v = v1 - v2:real^N` THEN
      ABBREV_TAC `w = v3 - v2:real^N` THEN

      FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
      REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
      DISCH_THEN (X_CHOOSE_THEN `px:real^N` MP_TAC) THEN
      DISCH_THEN (CONJUNCTS_THEN2 (X_CHOOSE_THEN `up:real` MP_TAC) (X_CHOOSE_THEN `tp:real` MP_TAC)) THEN
      REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
      STRIP_TAC THEN POP_ASSUM (LABEL_TAC "px1") THEN
      ONCE_REWRITE_TAC[CONJ_ASSOC] THEN
      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "px2")) THEN

      SUBGOAL_THEN `(&1 - u) % v + u % w = t2 % d + (&1 - t1 - t2) % (--v2:real^N)` MP_TAC THENL
      [
        REPLICATE_TAC 4 REMOVE_ASSUM THEN
          REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
          REWRITE_TAC [VECTOR_ARITH `(&1 - u) % (v1 - v2) + u % (v3 - v2) = ((&1 - u) % v1 + u % v3) - v2:real^N`] THEN
          FIRST_X_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[SYM th])) THEN
          ASM_REWRITE_TAC[] THEN
          VECTOR_ARITH_TAC;
        ALL_TAC
      ] THEN

      SUBGOAL_THEN `~(d = vec 0:real^N)` ASSUME_TAC THENL
      [
        EXPAND_TAC "d" THEN
          ASM_REWRITE_TAC[VECTOR_SUB_EQ];
        ALL_TAC
      ] THEN

      DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. projection d v`) THEN
      REWRITE_TAC[PROJECTION_LINEAR] THEN
      ASM_SIMP_TAC[PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN

      SUBGOAL_THEN `projection d (--v2) dot n = &0 /\ projection d v dot n = v1 dot n /\ projection d w dot n = v3 dot n:real^N` ASSUME_TAC THENL
      [
        MAP_EVERY EXPAND_TAC ["d";
 "v"; "w"] THEN
          REWRITE_TAC[projection] THEN
          ASM_REWRITE_TAC[DOT_LSUB; DOT_LNEG; DOT_LMUL; REAL_SUB_REFL; REAL_MUL_RZERO] THEN
          REAL_ARITH_TAC;
        ALL_TAC
      ] THEN

      DISCH_TAC THEN
      FIRST_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
      USE_THEN "px2" MP_TAC THEN USE_THEN "px1" (fun th -> REWRITE_TAC[th]) THEN
      DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
      ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO] THEN
      DISCH_THEN (LABEL_TAC "A" o SYM) THEN DISCH_THEN (LABEL_TAC "B") THEN

      SUBGOAL_THEN `u = up:real` ASSUME_TAC THENL
      [
        MATCH_MP_TAC EQ_TRANS THEN
          ABBREV_TAC `a = v1 dot n:real^N` THEN
          ABBREV_TAC `b = v3 dot n:real^N` THEN
          EXISTS_TAC `a / (a - b)` THEN
          SUBGOAL_THEN `~(a - b = &0)` ASSUME_TAC THENL
          [
            MATCH_MP_TAC (REAL_ARITH `&0 < b + --a ==> ~(a - b = &0)`) THEN
              MATCH_MP_TAC REAL_LT_ADD THEN
              ASM_REWRITE_TAC[REAL_NEG_GT0];
            ALL_TAC
          ] THEN

          CONJ_TAC THEN MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `a - b:real` THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN ASM_SIMP_TAC[REAL_MUL_LINV] THENL
          [
            REMOVE_THEN "B" MP_TAC THEN REAL_ARITH_TAC;
            ALL_TAC
          ] THEN
          REMOVE_THEN "A" MP_TAC THEN
          REAL_ARITH_TAC;
        ALL_TAC
      ] THEN

      REMOVE_THEN "px2" MP_TAC THEN
      POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]) THEN
      ASM_REWRITE_TAC[VECTOR_MUL_RCANCEL] THEN
      UNDISCH_TAC `&0 <= tp` THEN
      REAL_ARITH_TAC);;




(* The second rotation lemma for a 4-point configuration *)

let lemma_4_points_rotation2 = 
prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
                                       dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
                                       &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
                                       &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
                                       &2 <= dist (v2,v4) /\
                                       ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4} = {})
                                       ==> (?v1'. v1' IN ball_annulus /\ norm v1' = &2 /\
                                                  dist (v1',v3) <= &2 * h0 /\
                                                  dist (v1',v2) = dist (v1,v2) /\
                                                  dist (v1',v4) = dist (v1,v4) /\
                                                  ~(segment [v1',v3] INTER convex hull {vec 0,v2,v4} = {}))`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `?u t2 t4. (&0 <= u /\ u <= &1 /\ &0 <= t2 /\ &0 <= t4 /\ t2 + t4 <= &1) /\ (&1 - u) % (v1 - v2) + u % (v3 - v2) = t4 % (v4 - v2) + (&1 - t2 - t4) % (--v2:real^3)` MP_TAC THENL
     [
       POP_ASSUM MP_TAC THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; CONVEX_HULL_3_ALT; IN_ELIM_THM] THEN
         REWRITE_TAC[VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
         REPEAT STRIP_TAC THEN
         MAP_EVERY EXISTS_TAC [`u:real`; `u':real`; `v:real`] THEN
         ASM_REWRITE_TAC[] THEN
         REWRITE_TAC[VECTOR_ARITH `(&1 - u) % (v1 - v2) + u % (v3 - v2) = ((&1 - u) % v1 + u % v3) - v2:real^3`] THEN
         POP_ASSUM MP_TAC THEN
         FIRST_X_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[SYM th])) THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3} /\ ~(v2 = vec 0) /\ ~(v4 = vec 0)` ASSUME_TAC THENL
     [
       REPLICATE_TAC 3 (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
         SIMP_TAC[in_ball_annulus] THEN
         REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN
         MATCH_MP_TAC estd_non_collinear_lemma THEN
         ASM_REWRITE_TAC[in_ball_annulus];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4:real^3} = {})` MP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
         STRIP_TAC THEN EXISTS_TAC `x:real^3` THEN ASM_REWRITE_TAC[] THEN
         MATCH_MP_TAC Hypermap.lemma_in_subset THEN
         EXISTS_TAC `convex hull {vec 0,v2,v4:real^3}` THEN
         ASM_REWRITE_TAC[] THEN
         ASM_SIMP_TAC[CONVEX_HULL_3_ALT; aff_ge_0_2; SUBSET; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
         REPEAT STRIP_TAC THEN
         MAP_EVERY EXISTS_TAC [`u:real`; `v:real`] THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_neg o concl)) THEN
     DISCH_TAC THEN

     MAP_EVERY (fun tm -> DISCH_THEN (X_CHOOSE_THEN tm MP_TAC)) [`u:real`; `t2:real`; `t4:real`] THEN
     DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "A")) THEN

     MP_TAC (SPEC_ALL separation_plane_4_points) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN

     ABBREV_TAC `v:real^3 = v1 - v2` THEN
     ABBREV_TAC `w:real^3 = v3 - v2` THEN
     ABBREV_TAC `d:real^3 = v4 - v2` THEN

     SUBGOAL_THEN `~(d = vec 0:real^3)` ASSUME_TAC THENL
     [
       EXPAND_TAC "d" THEN
         REWRITE_TAC[GSYM NORM_EQ_0; GSYM dist; DIST_SYM] THEN
         ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> ~(a = &0)`];
       ALL_TAC
     ] THEN

     (* Rotation *)
     MP_TAC (ISPECL [`projection d v:real^3`; `projection d w:real^3`; `projection d (--v2):real^3`; `d:real^3`] rotation_lemma_segments) THEN
     SUBGOAL_THEN `~(projection d (--v2) = vec 0:real^3)` ASSUME_TAC THENL
     [
       EXPAND_TAC "d" THEN
         REWRITE_TAC[projection] THEN
         ABBREV_TAC `k = (--v2 dot (v4 - v2:real^3)) / ((v4 - v2) dot (v4 - v2))` THEN
         ASM_CASES_TAC `k = &0` THENL
         [
           ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_SUB_RZERO; VECTOR_NEG_EQ_0];
           ALL_TAC
         ] THEN

         DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv (k) % v`) THEN
         ASM_SIMP_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_LINV] THEN
         REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_RZERO] THEN
         REWRITE_TAC[VECTOR_ARITH `a % (--v2) - (v4 - v2) = vec 0 <=> v4 = (&1 - a) % v2:real^3`] THEN
         UNDISCH_TAC `~collinear {vec 0,v2,v4} /\ ~(v2 = vec 0) /\ ~(v4 = vec 0:real^3)` THEN
         SIMP_TAC[COLLINEAR_LEMMA_ALT; DE_MORGAN_THM; NOT_EXISTS_THM];
       ALL_TAC
     ] THEN

     ANTS_TAC THENL
     [
       SUBGOAL_THEN `v dot n = v1 dot n /\ w dot n = v3 dot n /\ d dot n:real^3 = &0` ASSUME_TAC THENL
         [
           MAP_EVERY EXPAND_TAC ["v";
 "w"; "d"] THEN
             ASM_REWRITE_TAC[DOT_LSUB; REAL_SUB_RZERO];
           ALL_TAC
         ] THEN
         ASM_REWRITE_TAC[DIMINDEX_3; LE_REFL; PROJECTION_ORTHOGONAL] THEN

         CONJ_TAC THENL
         [
           DISCH_THEN (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN
             REWRITE_TAC[projection] THEN
             ASM_REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_LZERO; REAL_MUL_RZERO; REAL_SUB_RZERO] THEN
             ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> ~(a = &0)`];
           ALL_TAC
         ] THEN

         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
         REWRITE_TAC[IN_INTER; IN_SEGMENT; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
         EXISTS_TAC `(&1 - t2 - t4) % projection d (--v2:real^3)` THEN
         CONJ_TAC THENL
         [
           EXISTS_TAC `&1 - t2 - t4` THEN
             ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - t2 - t4 <=> t2 + t4 <= &1`] THEN
             MATCH_MP_TAC (REAL_ARITH `&0 <= t2 /\ &0 <= t4 ==> &1 - t2 - t4 <= &1`) THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         EXISTS_TAC `u:real` THEN
         ASM_REWRITE_TAC[] THEN
         REMOVE_THEN "A" (MP_TAC o AP_TERM `\v:real^3. projection d v`) THEN
         REWRITE_TAC[PROJECTION_LINEAR] THEN
         ASM_SIMP_TAC[PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
       ALL_TAC
     ] THEN

     DISCH_THEN (X_CHOOSE_THEN `g:real^1->real^3` STRIP_ASSUME_TAC) THEN

     (* f(t) *)
     ABBREV_TAC `f = (\t:real^1. (g t + v - projection d v) + v2:real^3)` THEN

     (* f(0) = v1 and (f(1) dot n) = 0 *)
     SUBGOAL_THEN `f (lift (&0)) = v1:real^3 /\ f (lift (&1)) dot n = &0` ASSUME_TAC THENL
     [
       EXPAND_TAC "f" THEN
         ASM_REWRITE_TAC[VECTOR_ARITH `pv + v - pv = v:real^3`] THEN
         CONJ_TAC THENL
         [
           EXPAND_TAC "v" THEN VECTOR_ARITH_TAC;
           ALL_TAC
         ] THEN

         REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
         SUBGOAL_THEN `d dot n:real^3 = &0` ASSUME_TAC THENL [ EXPAND_TAC "d" THEN ASM_REWRITE_TAC[DOT_LSUB; REAL_SUB_RZERO]; ALL_TAC ] THEN
         SUBGOAL_THEN `(v - projection d v) dot n:real^3 = &0` (fun th -> REWRITE_TAC[th]) THENL
         [
           GEN_REWRITE_TAC (PAT_CONV `\x:real^3. (x - y) dot z = &0`) [VECTOR_PROJECTION] THEN
             REWRITE_TAC[VECTOR_ARITH `(a + b) - a = b:real^3`] THEN
             ASM_REWRITE_TAC[DOT_LMUL; REAL_MUL_RZERO];
           ALL_TAC
         ] THEN

         ASM_REWRITE_TAC[projection; DOT_LSUB; DOT_LMUL; DOT_LNEG; REAL_MUL_RZERO; REAL_SUB_LZERO; REAL_NEG_0; REAL_ADD_LID];
       ALL_TAC
     ] THEN

     (* d(f(t), v2) = d(v1, v2) *)
     SUBGOAL_THEN `!t. dist (f (t:real^1), v2:real^3) = dist (v1, v2) /\ dist (f t, v4) = dist (v1, v4)` ASSUME_TAC THENL
     [
       GEN_TAC THEN EXPAND_TAC "f" THEN
         REWRITE_TAC[dist; VECTOR_ARITH `(a + b) - b = a:real^3 - vec 0`] THEN
         REWRITE_TAC[VECTOR_ARITH `((a + b - c) + v2) - v4 = (a + b - c) - (v4 - v2:real^3)`] THEN
         REWRITE_TAC[GSYM dist; DIST_EQ] THEN
         ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ; PROJECTION_ZERO] THEN
         ASM_REWRITE_TAC[PROJECTION_0; DIST_0] THEN
         EXPAND_TAC "v" THEN EXPAND_TAC "d" THEN REWRITE_TAC[dist] THEN
         REWRITE_TAC[VECTOR_ARITH `v1 - v2 - (v4 - v2) = v1 - v4:real^3`] THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     (* d(f(t), v3) <= d(v1,v3) <= 2 h0 *)
     SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), v3:real^3) <= &2 * h0` MP_TAC THENL
     [
       REPEAT STRIP_TAC THEN
         MATCH_MP_TAC REAL_LE_TRANS THEN
         EXISTS_TAC `dist (v1,v3:real^3)` THEN
         ASM_REWRITE_TAC[] THEN
         EXPAND_TAC "f" THEN
         REWRITE_TAC[dist] THEN
         ASM_REWRITE_TAC[VECTOR_ARITH `((g + v - pv) + v2) - v3:real^3 = (g + v - pv) - (v3 - v2)`] THEN
         GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ARITH `v1 - v3 = (v1 - v2) - (v3 - v2:real^3)`] THEN
         ASM_REWRITE_TAC[] THEN
         REWRITE_TAC[GSYM dist] THEN
         MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
         ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     (* |f(t)| <= |v1| *)
     SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> norm (f (lift t):real^3) <= norm (v1:real^3)` MP_TAC THENL
     [
       REPEAT STRIP_TAC THEN
         EXPAND_TAC "f" THEN
         ASM_REWRITE_TAC[VECTOR_ARITH `(g + v - pv) + v2:real^3 = (g + v - pv) - (--v2)`] THEN
         GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ARITH `v1 = (v1 - v2) - (--v2:real^3)`] THEN
         ASM_REWRITE_TAC[] THEN
         REWRITE_TAC[GSYM dist] THEN
         MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
         ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     REPEAT DISCH_TAC THEN

     (* If 2 <= |f(t)|, then f IN ball_annulus *)
     SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 /\ &2 <= norm (f (lift t):real^3) ==> f (lift t) IN ball_annulus` ASSUME_TAC THENL
     [
       REPEAT STRIP_TAC THEN
         ASM_SIMP_TAC[in_ball_annulus; GSYM NORM_EQ_0; REAL_ARITH `&2 <= a ==> ~(a = &0)`] THEN
         MATCH_MP_TAC REAL_LE_TRANS THEN
         EXISTS_TAC `norm (v1:real^3)` THEN
         ASM_SIMP_TAC[] THEN
         UNDISCH_TAC `v1 IN ball_annulus` THEN
         SIMP_TAC[in_ball_annulus];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `f:real^1->real^3 continuous_on interval [lift (&0), lift (&1)]` ASSUME_TAC THENL
     [
       EXPAND_TAC "f" THEN
         REPEAT (MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST]) THEN
         MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
         EXISTS_TAC `UNIV:real^1->bool` THEN
         ASM_REWRITE_TAC[SUBSET_UNIV];
       ALL_TAC
     ] THEN

     REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o check (free_in `g:real^1->real^3` o concl))) THEN
     SUBGOAL_THEN `!t:real^1. projection d (g t) = (g t):real^3` MP_TAC THENL
     [
       GEN_TAC THEN REWRITE_TAC[projection] THEN
         ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO; VECTOR_MUL_LZERO; VECTOR_SUB_RZERO];
       ALL_TAC
     ] THEN

     REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `g:real^1->real^3` o concl))) THEN
     REPEAT DISCH_TAC THEN

     ASM_CASES_TAC `!h. &0 <= h /\ h <= &1 ==> &2 <= norm (f (lift h):real^3)` THENL
     [
       MATCH_MP_TAC (TAUT `F ==> A`) THEN
         MP_TAC (SPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `&1`] continuous_lemma_aff_ge) THEN
         ANTS_TAC THENL
         [
           ASM_REWRITE_TAC[REAL_LE_01] THEN
             GEN_TAC THEN DISCH_TAC THEN
             SUBGOAL_THEN `t:real^1 = lift (drop t)` (fun th -> ONCE_REWRITE_TAC[th]) THENL [ REWRITE_TAC[LIFT_DROP]; ALL_TAC ] THEN
             SUBGOAL_THEN `&0 <= drop (t:real^1) /\ drop t <= &1` ASSUME_TAC THENL
             [
               ASM_REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC zero_not_between_estd THEN
             ASM_SIMP_TAC[];
           ALL_TAC
         ] THEN

         DISCH_THEN DISJ_CASES_TAC THENL
         [
           MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `f (lift (&1)):real^3`; `v3:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
             ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`; IN_INTERVAL_1; REAL_LE_REFL; REAL_LE_01] THEN
             DISCH_TAC THEN
             MATCH_MP_TAC LEMMA_3_POINTS_FINAL THEN
             MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift (&1)):real^3`] THEN
             ASM_SIMP_TAC[DIST_SYM; REAL_LE_REFL; REAL_LE_01];
           ALL_TAC
         ] THEN

         POP_ASSUM MP_TAC THEN STRIP_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
         [
           MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
             ASM_SIMP_TAC[DIST_SYM];
           MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
             ASM_SIMP_TAC[DIST_SYM];
           MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
             ASM_SIMP_TAC[DIST_SYM]
         ];
       ALL_TAC
     ] THEN

     (* ?h. f(h) <= 2 *)
     POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; REAL_NOT_LE] THEN
     DISCH_THEN (CHOOSE_THEN ASSUME_TAC) THEN

     SUBGOAL_THEN `?s. &0 <= s /\ s <= &1 /\ norm (f (lift s):real^3) = &2 /\ (!t. &0 <= t /\ t <= s ==> &2 <= norm (f (lift t)))` MP_TAC THENL
     [
       MP_TAC (SPECL [`\t:real. norm (f (lift t):real^3)`; `&2`; `h:real`] continuous_lemma_dec) THEN
         ANTS_TAC THENL
         [
           ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
             UNDISCH_TAC `v1 IN ball_annulus` THEN
             SIMP_TAC[in_ball_annulus] THEN DISCH_TAC THEN
             REWRITE_TAC[REAL_CONTINUOUS_ON; IMAGE_LIFT_REAL_INTERVAL] THEN
             SUBGOAL_THEN `lift o (\t. norm (f (lift t):real^3)) o drop = (lift o norm) o f` (fun th -> REWRITE_TAC[th]) THENL
             [
               REWRITE_TAC[FUN_EQ_THM; o_THM; LIFT_DROP];
               ALL_TAC
             ] THEN
             MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
             REWRITE_TAC[CONTINUOUS_ON_LIFT_NORM] THEN
             MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
             EXISTS_TAC `interval [lift (&0), lift (&1)]` THEN
             ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
           ALL_TAC
         ] THEN

         BETA_TAC THEN STRIP_TAC THEN
         EXISTS_TAC `x:real` THEN
         ASM_REWRITE_TAC[] THEN
         CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `h:real` THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
         REPEAT STRIP_TAC THEN
         ASM_CASES_TAC `t = x:real` THENL [ ASM_REWRITE_TAC[REAL_LE_REFL]; ALL_TAC ] THEN
         MATCH_MP_TAC REAL_LT_IMP_LE THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         ASM_REWRITE_TAC[REAL_LT_LE];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN
     SUBGOAL_THEN `!t. t <= s ==> t <= &1` ASSUME_TAC THENL
     [
       REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
         EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     (* The main step *)
     MP_TAC (SPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `s:real`] continuous_lemma_aff_ge) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN
         CONJ_TAC THENL
         [
           MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
             EXISTS_TAC `interval [lift (&0), lift (&1)]` THEN
             ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
           ALL_TAC
         ] THEN

         GEN_TAC THEN DISCH_TAC THEN
         SUBGOAL_THEN `t:real^1 = lift (drop t)` (fun th -> ONCE_REWRITE_TAC[th]) THENL [ REWRITE_TAC[LIFT_DROP]; ALL_TAC ] THEN
         SUBGOAL_THEN `&0 <= drop (t:real^1) /\ drop t <= s` ASSUME_TAC THENL
         [
           ASM_REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP];
           ALL_TAC
         ] THEN
         MATCH_MP_TAC zero_not_between_estd THEN
         ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     ONCE_REWRITE_TAC[DISJ_SYM] THEN
     DISCH_THEN DISJ_CASES_TAC THENL
     [
       MATCH_MP_TAC (TAUT `F ==> A`) THEN
         POP_ASSUM MP_TAC THEN STRIP_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
         [
           MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
             ASM_SIMP_TAC[DIST_SYM];
           MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
             ASM_SIMP_TAC[DIST_SYM];
           MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
             ASM_SIMP_TAC[DIST_SYM]
         ];
       ALL_TAC
     ] THEN

     EXISTS_TAC `f (lift s):real^3` THEN
     ASM_SIMP_TAC[REAL_LE_REFL] THEN

     (* [f(s), v3] INTER convex hull {0,v2,v4} *)
     MATCH_MP_TAC segment_inter_conv THEN
     ASM_REWRITE_TAC[] THEN

     MP_TAC (SPECL [`f (lift s):real^3`; `v2:real^3`; `v3:real^3`; `v4:real^3`] separation_plane_4_points) THEN
     ANTS_TAC THENL
     [
       ASM_SIMP_TAC[REAL_LE_REFL] THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
       ALL_TAC
     ] THEN

     REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `n:real^3` o concl))) THEN
     STRIP_TAC THEN
     EXISTS_TAC `n:real^3` THEN
     ASM_REWRITE_TAC[] THEN
     CONJ_TAC THENL
     [
       ONCE_REWRITE_TAC[VECTOR_ARITH `v2 = v4:real^3 <=> v4 - v2 = vec 0`] THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     CONJ_TAC THENL
     [
       FIRST_X_ASSUM MATCH_MP_TAC THEN
         ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `projection d (f (lift s) - v2:real^3) = projection d (g (lift s))` (fun th -> REWRITE_TAC[th]) THENL
     [
       EXPAND_TAC "f" THEN
         REWRITE_TAC[VECTOR_ARITH `(a + v2) - v2 = a:real^3`] THEN
         REWRITE_TAC[PROJECTION_LINEAR] THEN
         SUBGOAL_THEN `?a. v - projection d v = a % d:real^3` MP_TAC THENL
         [
           EXISTS_TAC `(v dot d:real^3) / (d dot d)` THEN
             REWRITE_TAC[projection] THEN
             VECTOR_ARITH_TAC;
           ALL_TAC
         ] THEN
         STRIP_TAC THEN
         ASM_SIMP_TAC[PROJECTION_LINEAR; PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_RID];
       ALL_TAC
     ] THEN

     ASM_SIMP_TAC[]);;



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


let lemma_4_points_rotation2_full = 
prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
                                            dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
                                            &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
                                            &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
                                            &2 <= dist (v2,v4) /\
                                            ~(segment [v1,v3] INTER convex hull {vec 0, v2, v4} = {})
                                            ==> (?v1' v3'. v1' IN ball_annulus /\ v3' IN ball_annulus /\
                                                   norm v1' = &2 /\ norm v3' = &2 /\
                                                   dist (v1',v3') <= &2 * h0 /\
                                                   dist (v1',v2) = dist (v1,v2) /\ dist (v1',v4) = dist (v1,v4) /\
                                                   dist (v2,v3') = dist (v2,v3) /\ dist (v3',v4) = dist (v3,v4) /\
                                                   ~(segment [v1',v3'] INTER aff_ge {vec 0} {v2, v4} = {}))`,

   REPEAT STRIP_TAC THEN
     (* v1 about v2-v4 *)
     MP_TAC (SPEC_ALL lemma_4_points_rotation2) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     EXISTS_TAC `v1':real^3` THEN
     ASM_REWRITE_TAC[] THEN

     (* v3 about v2-v4 *)
     MP_TAC (SPECL [`v3:real^3`; `v2:real^3`; `v1':real^3`; `v4:real^3`] lemma_4_points_rotation2) THEN
     ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; SEGMENT_SYM] THEN
     DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN REWRITE_TAC[DIST_SYM] THEN
     STRIP_TAC THEN
     EXISTS_TAC `v3':real^3` THEN
     ASM_REWRITE_TAC[DIST_SYM] THEN

     POP_ASSUM MP_TAC THEN
     REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
     STRIP_TAC THEN
     EXISTS_TAC `x:real^3` THEN ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC Hypermap.lemma_in_subset THEN
     EXISTS_TAC `convex hull {vec 0, v2, v4:real^3}` THEN
     ASM_REWRITE_TAC[] THEN
     UNDISCH_TAC `v2 IN ball_annulus` THEN
     UNDISCH_TAC `v4 IN ball_annulus` THEN
     SIMP_TAC[in_ball_annulus; aff_ge_0_2] THEN
     REPEAT DISCH_TAC THEN
     REWRITE_TAC[SUBSET; CONVEX_HULL_3_ALT; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
     REPEAT STRIP_TAC THEN
     MAP_EVERY EXISTS_TAC [`u:real`; `v:real`] THEN
     ASM_REWRITE_TAC[]);;



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


(* Prove that a certain configuration of 4 points is impossible *)

let lemma_4_points_circumcenter = 
prove(`!v1 v2 v3 v4. ~(collinear {vec 0,v2,v4}) /\
                                          v2 IN ball_annulus /\ v4 IN ball_annulus /\
                                          ~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4} = {}) /\
                                          norm v1 = &2 /\ norm v3 = &2 /\
                                          dist (v1,v2) = &2 /\ dist (v1,v4) = &2 /\
                                          dist (v3,v2) = &2 /\ dist (v3,v4) = &2
                                              ==> norm(v1 + v3) = &2 * eta_y (norm v2) (norm v4) (dist (v2,v4))`,

  REWRITE_TAC[in_ball_annulus] THEN
    REPEAT STRIP_TAC THEN
    SUBGOAL_THEN `!v w:real^3. norm v = &2 /\ dist (v,w) = &2 ==> v dot w = norm w pow 2 / &2` ASSUME_TAC THENL
    [
      REWRITE_TAC[DIST_SQR; REAL_ARITH `&0 <= &2`] THEN
        REWRITE_TAC[dist; NORM_POW_2] THEN
        REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_SQUARE_NORM; DOT_SYM] THEN
        REPEAT GEN_TAC THEN
        STRIP_TAC THEN POP_ASSUM MP_TAC THEN
        ASM_REWRITE_TAC[] THEN
        REAL_ARITH_TAC;
      ALL_TAC
    ] THEN
    FIRST_ASSUM (MP_TAC o SPECL [`v1:real^3`; `v2:real^3`]) THEN
    FIRST_ASSUM (MP_TAC o SPECL [`v1:real^3`; `v4:real^3`]) THEN
    FIRST_ASSUM (MP_TAC o SPECL [`v3:real^3`; `v2:real^3`]) THEN
    FIRST_X_ASSUM (MP_TAC o SPECL [`v3:real^3`; `v4:real^3`]) THEN
    ASM_REWRITE_TAC[DOT_SYM] THEN
    REPEAT STRIP_TAC THEN

    ABBREV_TAC `v = inv(&2) % (v1 + v3:real^3)` THEN

    SUBGOAL_THEN `v:real^3 IN affine hull {vec 0,v2,v4}` ASSUME_TAC THENL
    [
      FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
        REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
        REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
        ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
        STRIP_TAC THEN
        SUBGOAL_THEN `x:real^3 dot v1 = x dot v3` MP_TAC THENL
        [
          POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
            ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; DOT_SYM];
          ALL_TAC
        ] THEN
        POP_ASSUM (LABEL_TAC "A" o SYM) THEN
        ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
        ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM; REAL_ARITH `&2 pow 2 = &4`] THEN
        ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`] THEN
        REWRITE_TAC[REAL_ARITH `((&1 - u) * &4 + u * a13) - ((&1 - u) * a13 + u * &4) = &2 * u * (a13 - &4) - (a13 - &4)`] THEN

        ASM_CASES_TAC `v1:real^3 dot v3 = &4` THENL
        [
          DISCH_THEN (fun th -> ALL_TAC) THEN
            SUBGOAL_THEN `norm (v3) % v1:real^3 = norm (v1) % v3` MP_TAC THENL
            [
              REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQ] THEN
                ASM_REWRITE_TAC[DOT_SYM] THEN
                REAL_ARITH_TAC;
              ALL_TAC
            ] THEN
            ASM_REWRITE_TAC[VECTOR_ARITH `&2 % v1 = &2 % v3 <=> v1 = v3`] THEN
            DISCH_TAC THEN UNDISCH_TAC `x = (&1 - u) % v1 + u % v3:real^3` THEN
            EXPAND_TAC "v" THEN
            POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
            REWRITE_TAC[VECTOR_ARITH `(&1 - u) % v1 + u % v1 = v1:real^3`] THEN
            EXPAND_TAC "x" THEN
            REWRITE_TAC[VECTOR_ARITH `inv(&2) % (v1 + v1) = v1:real^3`] THEN
            DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
            REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
            MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
            CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
            VECTOR_ARITH_TAC;
          ALL_TAC
        ] THEN

        DISCH_TAC THEN
        SUBGOAL_THEN `u = inv(&2)` ASSUME_TAC THENL
        [
          POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
            CONV_TAC REAL_FIELD;
          ALL_TAC
        ] THEN

        SUBGOAL_THEN `v = x:real^3` (fun th -> REWRITE_TAC[th]) THENL
        [
          ASM_REWRITE_TAC[] THEN
            EXPAND_TAC "v" THEN
            VECTOR_ARITH_TAC;
          ALL_TAC
        ] THEN

        EXPAND_TAC "x" THEN
        REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
        MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
        CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
        VECTOR_ARITH_TAC;
      ALL_TAC
    ] THEN

    SUBGOAL_THEN `dist (v:real^3,v2) = norm v /\ dist (v,v4) = norm v` ASSUME_TAC THENL
    [
      REWRITE_TAC[DIST_SQR] THEN
        REWRITE_TAC[dist; NORM_POS_LE; NORM_POW_2] THEN
        REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN
        REWRITE_TAC[REAL_ARITH `a - b - c = a <=> b + c = &0`] THEN
        EXPAND_TAC "v" THEN
        REWRITE_TAC[DOT_LMUL; DOT_RMUL; DOT_LADD; DOT_RADD] THEN
        ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
        REAL_ARITH_TAC;
      ALL_TAC
    ] THEN

    SUBGOAL_THEN `v:real^3 = circumcenter {vec 0,v2,v4}` ASSUME_TAC THENL
    [
      MATCH_MP_TAC (GEN_ALL Collect_geom.DIST_EQ_IS_UNIQUE) THEN
        MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `vec 0:real^3`] THEN
        ASM_REWRITE_TAC[DIST_0] THEN
        MP_TAC (SPECL [`vec 0:real^3`; `v2:real^3`; `v4:real^3`] Collect_geom.CIRCUMCENTER_PROPTIES) THEN
        ASM_REWRITE_TAC[] THEN
        STRIP_TAC THEN
        FIRST_ASSUM (MP_TAC o SPEC `vec 0:real^3`) THEN
        SIMP_TAC[IN_INSERT; DIST_0] THEN
        DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
        FIRST_ASSUM (MP_TAC o SPEC `v2:real^3`) THEN
        FIRST_ASSUM (MP_TAC o SPEC `v4:real^3`) THEN
        SIMP_TAC[IN_INSERT] THEN
        REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN
        REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY] THEN
        GEN_TAC THEN
        STRIP_TAC THEN ASM_REWRITE_TAC[];
      ALL_TAC
    ] THEN

    SUBGOAL_THEN `norm (v:real^3) = radV {vec 0,v2,v4:real^3}` ASSUME_TAC THENL
    [
      ASM_REWRITE_TAC[GSYM DIST_0; DIST_SYM] THEN
        MP_TAC (GEN_ALL Collect_geom.NOT_COL_IMP_RADV_PROPERTIY) THEN
        DISCH_THEN (MP_TAC o SPECL [`vec 0:real^3`; `v2:real^3`; `v4:real^3`]) THEN
        ASM_REWRITE_TAC[] THEN
        DISCH_THEN (MATCH_MP_TAC o GSYM) THEN
        ONCE_REWRITE_TAC[GSYM IN] THEN
        REWRITE_TAC[IN_INSERT];
      ALL_TAC
    ] THEN

    POP_ASSUM MP_TAC THEN
    MP_TAC (SPECL [`v4:real^3`; `v2:real^3`; `vec 0:real^3`; `norm (v2:real^3)`; `norm (v4:real^3)`; `dist (v2:real^3,v4:real^3)`] Collect_geom.CDEUSDF) THEN
    REWRITE_TAC[Collect_geom.dist3; DIST_0; DIST_SYM] THEN
    SUBGOAL_THEN `{v4,v2,vec 0:real^3} = {vec 0,v2,v4}` (fun th -> ONCE_REWRITE_TAC[th]) THENL
    [
      SET_TAC[];
      ALL_TAC
    ] THEN
    REMOVE_ASSUM THEN
    ASM_REWRITE_TAC[] THEN
    REPLICATE_TAC 2 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN
    DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
    DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
    EXPAND_TAC "v" THEN
    REWRITE_TAC[NORM_MUL] THEN
    REAL_ARITH_TAC);;


let PARALLELOGRAM_LAW = 
prove(`!v1 v2:real^N. &2 * (norm v1 pow 2 + norm v2 pow 2) = norm (v1 + v2) pow 2 + norm (v1 - v2) pow 2`,

   REPEAT GEN_TAC THEN
     REWRITE_TAC[NORM_POW_2] THEN
     VECTOR_ARITH_TAC);;


let lemma_4_points_contradiction = 
prove(`!v1 v2 v3 v4.
                                           v2 IN ball_annulus /\ v4 IN ball_annulus /\
                                           &2 <= dist (v2,v4) /\ dist (v2,v4) <= &2 * h0 /\
                                           ~(segment [v1,v3] INTER aff_ge {vec 0} {v2, v4} = {}) /\
                                           norm v1 = &2 /\ norm v3 = &2 /\
                                           dist (v1,v2) = &2 /\ dist (v1,v4) = &2 /\
                                           dist (v3,v2) = &2 /\ dist (v3,v4) = &2 /\
                                           dist (v1,v3) <= &2 * h0
                                             ==> F`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `~collinear {vec 0:real^3,v2,v4}` ASSUME_TAC THENL
     [
       MATCH_MP_TAC estd_non_collinear_lemma THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     MP_TAC (SPEC_ALL lemma_4_points_circumcenter) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_TAC THEN
     MP_TAC (ISPECL [`v1:real^3`; `v3:real^3`] PARALLELOGRAM_LAW) THEN
     ASM_REWRITE_TAC[GSYM dist] THEN
     MATCH_MP_TAC (REAL_ARITH `a < b ==> ~(b = a)`) THEN
     CONV_TAC REAL_RAT_REDUCE_CONV THEN
     ONCE_REWRITE_TAC[REAL_ARITH `&16 = (&16 - (&2 * h0) pow 2) + (&2 * h0) pow 2`] THEN
     MATCH_MP_TAC REAL_LTE_ADD2 THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC REAL_LET_TRANS THEN
         EXISTS_TAC `&4 * #2.2` THEN
         CONJ_TAC THENL
         [
           REWRITE_TAC[REAL_POW_MUL] THEN
             MATCH_MP_TAC REAL_LE_MUL2 THEN
             ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2; REAL_ARITH `&2 pow 2 <= &4`] THEN

             MP_TAC Tame_inequalities.ETA_Y_4_POINTS_INEQ THEN

             REWRITE_TAC[Tame_inequalities.INEQ_ALT; ALL] THEN
             DISCH_THEN MATCH_MP_TAC THEN
             REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
             ASM_SIMP_TAC[in_ball_annulus];
           ALL_TAC
         ] THEN
         REWRITE_TAC[Sphere.h0] THEN
         REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
     REWRITE_TAC[dist; REAL_ABS_NORM] THEN
     REWRITE_TAC[GSYM dist] THEN
     UNDISCH_TAC `dist(v1,v3:real^3) <= &2 * h0` THEN
     REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);;


(* The final result *)

let LEMMA_4_POINTS_FINAL = 
prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
                                   dist (v1, v3) <= &2 * h0 /\ dist (v2, v4) <= &2 * h0 /\
                                   &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
                                   &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
                                   &2 <= dist (v1,v3) /\ &2 <= dist (v2,v4)
                                   ==> aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4} = {vec 0}`,

   REPEAT STRIP_TAC THEN
     ASM_CASES_TAC `aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4} = {vec 0:real^3}` THEN ASM_REWRITE_TAC[] THEN
     SUBGOAL_THEN `?p. ~(p = vec 0:real^3) /\ p IN aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4}` MP_TAC THENL
     [
       POP_ASSUM MP_TAC THEN
         REWRITE_TAC[EXTENSION; IN_SING; NOT_FORALL_THM] THEN
         DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
         ASM_CASES_TAC `x = vec 0:real^3` THENL
         [
           ASM_REWRITE_TAC[IN_INTER; points_in_aff_ge_0_2];
           ALL_TAC
         ] THEN
         ASM_REWRITE_TAC[] THEN
         DISCH_TAC THEN
         EXISTS_TAC `x:real^3` THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
     [
       REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
         SIMP_TAC[in_ball_annulus];
       ALL_TAC
     ] THEN

     ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; IN_INTER] THEN
     STRIP_TAC THEN
     UNDISCH_TAC `p = t1 % v1 + t2 % v3:real^3` THEN
     POP_ASSUM (LABEL_TAC "p2" o SYM) THEN
     DISCH_THEN (LABEL_TAC "p1" o SYM) THEN

     SUBGOAL_THEN `!v v1 v2 v3 v4 t1 t2 t1' t2'. &0 <= t1 /\ &0 <= t2 /\ &0 <= t1' /\ &0 <= t2' /\ ~(v = vec 0) /\
                               t1 % v1 + t2 % v3 = v /\  t1' % v2 + t2' % v4 = v /\
                               t1' + t2' <= t1 + t2
                                 ==> ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4:real^3} = {})` ASSUME_TAC THENL
     [
       REPEAT REMOVE_ASSUM THEN
         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
         REPEAT STRIP_TAC THEN
         SUBGOAL_THEN `&0 < t1 + t2` ASSUME_TAC THENL
         [
           ASM_CASES_TAC `t1 = &0` THENL
             [
               UNDISCH_TAC `t1 % v1 + t2 % v3:real^3 = v` THEN
                 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
                 REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
                 ASM_CASES_TAC `t2 = &0` THENL
                 [
                   POP_ASSUM (fun th -> REWRITE_TAC[th; VECTOR_MUL_LZERO; VECTOR_ADD_LID]) THEN
                     ASM_REWRITE_TAC[];
                   ALL_TAC
                 ] THEN
                 DISCH_TAC THEN
                 ASM_REWRITE_TAC[REAL_ADD_LID; REAL_LT_LE];
               ALL_TAC
             ] THEN

             MATCH_MP_TAC REAL_LTE_ADD THEN
             ASM_REWRITE_TAC[REAL_LT_LE];
           ALL_TAC
         ] THEN

         REWRITE_TAC[IN_INTER; IN_SEGMENT; CONVEX_HULL_3_ALT; IN_ELIM_THM] THEN
         EXISTS_TAC `inv (t1 + t2) % v:real^3` THEN
         CONJ_TAC THENL
         [
           EXISTS_TAC `t2 * inv (t1 + t2)` THEN
             CONJ_TAC THENL
             [
               MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
                 MATCH_MP_TAC REAL_LE_INV THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
               ALL_TAC
             ] THEN

             CONJ_TAC THENL
             [
               REWRITE_TAC[GSYM real_div] THEN
                 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
                 ASM_REWRITE_TAC[REAL_ARITH `t2 <= t1 + t2 <=> &0 <= t1`];
               ALL_TAC
             ] THEN

             UNDISCH_TAC `t1 % v1 + t2 % v3:real^3 = v` THEN
             DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
             SUBGOAL_THEN `&1 - t2 * inv(t1 + t2) = t1 * inv (t1 + t2)` (fun th -> REWRITE_TAC[th]) THENL
             [
               MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
                 EXISTS_TAC `t1 + t2:real` THEN
                 REWRITE_TAC[REAL_SUB_RDISTRIB] THEN
                 ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
                 ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`; REAL_MUL_LINV] THEN
                 REAL_ARITH_TAC;
               ALL_TAC
             ] THEN

             VECTOR_ARITH_TAC;
           ALL_TAC
         ] THEN

         REWRITE_TAC[VECTOR_ADD_LID; VECTOR_SUB_RZERO] THEN
         MAP_EVERY EXISTS_TAC [`inv (t1 + t2) * t1'`; `inv (t1 + t2) * t2'`] THEN
         REWRITE_TAC[CONJ_ASSOC] THEN
         CONJ_TAC THENL
         [
           CONJ_TAC THENL
             [
               CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
               ALL_TAC
             ] THEN

             REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; REAL_MUL_AC; GSYM real_div] THEN
             MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         UNDISCH_TAC `t1' % v2 + t2' % v4:real^3 = v` THEN
         DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
         VECTOR_ARITH_TAC;
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `?v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
                                 dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
                                 &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
                                 &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
                                 &2 <= dist (v2,v4) /\
                                 ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4} = {})` MP_TAC THENL
     [
       ASM_CASES_TAC `t1' + t2' <= t1 + t2:real` THENL
         [
           MAP_EVERY EXISTS_TAC [`v1:real^3`; `v2:real^3`; `v3:real^3`; `v4:real^3`] THEN
             ASM_REWRITE_TAC[] THEN
             FIRST_X_ASSUM MATCH_MP_TAC THEN
             MAP_EVERY EXISTS_TAC [`p:real^3`; `t1:real`; `t2:real`; `t1':real`; `t2':real`] THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN
         DISCH_TAC THEN
         MAP_EVERY EXISTS_TAC [`v2:real^3`; `v1:real^3`; `v4:real^3`; `v3:real^3`] THEN
         ASM_REWRITE_TAC[DIST_SYM] THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         MAP_EVERY EXISTS_TAC [`p:real^3`; `t1':real`; `t2':real`; `t1:real`; `t2:real`] THEN
         ASM_SIMP_TAC[REAL_LT_IMP_LE];
       ALL_TAC
     ] THEN

     REPEAT REMOVE_ASSUM THEN
     STRIP_TAC THEN

     (* First rotation *)
     MP_TAC (SPEC_ALL lemma_4_points_rotation2_full) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN

     (* Second rotation *)
     MP_TAC (SPECL [`v1':real^3`; `v2:real^3`; `v3':real^3`; `v4:real^3`] lemma_4_points_rotation1_full) THEN
     ASM_REWRITE_TAC[] THEN
     MAP_EVERY (fun tm -> REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in tm o concl)))) [`v1:real^3`; `v3:real^3`; `v1':real^3`; `v3':real^3`] THEN

     STRIP_TAC THEN
     MATCH_MP_TAC lemma_4_points_contradiction THEN
     MAP_EVERY EXISTS_TAC [`v1'':real^3`; `v2:real^3`; `v3'':real^3`; `v4:real^3`] THEN
     ASM_REWRITE_TAC[DIST_SYM]);;



end;;