(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Eyypqdw = struct



open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Appendix;;

let SGIN_POW_EQ=
prove(`a IN {-- &1, &1} ==> a pow 2= &1`,

REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`]
THEN RESA_TAC
THEN REAL_ARITH_TAC);;

let EYYPQDW_COPLANAR=
prove_by_refinement(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
/\ a IN {-- &1, &1}
/\ &0< ups_x x1 x3 x5
/\ (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))=v3
==>
 coplanar{vec 0, v1, v2, v3}`,

[STRIP_TAC;

REWRITE_TAC[coplanar]
THEN EXISTS_TAC`vec 0:real^3`
THEN EXISTS_TAC`v1:real^3`
THEN EXISTS_TAC`v2:real^3`
THEN ASM_REWRITE_TAC[SET_RULE`{A,B,C,D} SUBSET E<=> A IN E/\ B IN E/\ C IN E/\ D IN E`;Collect_geom2.AFFINE_HULL_3;IN_ELIM_THM]
THEN REPEAT STRIP_TAC;

EXISTS_TAC`&1`
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&0`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1+ &0+ &0= &1`]
THEN VECTOR_ARITH_TAC;

EXISTS_TAC`&0`
THEN EXISTS_TAC`&1`
THEN EXISTS_TAC`&0`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0+ &1+ &0= &1`]
THEN VECTOR_ARITH_TAC;

EXISTS_TAC`&0`
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0+ &0+ &1= &1`]
THEN VECTOR_ARITH_TAC;

EXPAND_TAC"v3"
THEN REWRITE_TAC[CROSS_LAGRANGE;VECTOR_ARITH`a%v+b%(c%v-d%w)=(a+ b*c)%v+(--b*d)%w`]
THEN EXISTS_TAC`&1- (inv (&2 * x1) * (x1 + x3 - x5) +
      (inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) *
      (v1 dot (v2:real^3))) - (--(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) *
      (v1 dot v1))`
THEN EXISTS_TAC`(inv (&2 * x1) * (x1 + x3 - x5) +
      (inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) *
      (v1 dot (v2:real^3)))`
THEN EXISTS_TAC`(--(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) *
      (v1 dot (v1:real^3)))`
THEN ASM_REWRITE_TAC[REAL_ARITH`(&1-A-B)+A+B= &1`]
THEN VECTOR_ARITH_TAC]);;


let EYYPQDW_NORMV3=
prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
/\ a IN {-- &1, &1}
/\ &0< ups_x x1 x3 x5
/\ (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))=v3
==>
 norm(v3)  pow 2= x3`,

STRIP_TAC
THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM]
THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`]
THEN MRESAL_TAC (GEN_ALL Trigonometry1.DIST_UPS_X_POS)[`vec 0:real^3`;`v1:real^3`;`v2:real^3`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG]
THEN MRESAL_TAC Collect_geom.FHFMKIY[`vec 0:real^3`;`v1:real^3`;`v2:real^3`;`x1:real`;`x2:real`;`x6:real`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG]
THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`)
THEN RESA_TAC
THEN EXPAND_TAC"v3"
THEN REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_RSUB;DOT_LSUB]
THEN REPEAT RESA_TAC
THEN MRESA_TAC DOT_SYM[`v2:real^3`;`v1:real^3`]
THEN REPLICATE_TAC (23-9)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[REAL_ARITH`x1 - v1 dot v2 - (v1 dot v2 - x2) = x6
<=>  v1 dot v2  = (x1 + x2 - x6)/ &2`;REAL_ARITH`a*a *b=a pow 2 *b/\ A- &0=A/\ (a*b) pow 2=a pow 2 * b pow 2`;REAL_INV_MUL]
THEN RESA_TAC
THEN ASM_SIMP_TAC[SGIN_POW_EQ]
THEN MRESA_TAC REAL_MUL_LINV[`x1:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`((inv (&2) pow 2 * inv x1 pow 2) * (x1 + x3 - x5) pow 2) * x1 = ((inv (&2) pow 2 * inv x1 ) * (x1 + x3 - x5) pow 2) * (inv x1 *x1)
/\ A * &1 =A `]
THEN ASM_SIMP_TAC[SGIN_POW_EQ]
THEN MP_TAC(REAL_ARITH`&0< ups_x x1 x3 x5==> &0<=ups_x x1 x3 x5/\ ~(ups_x x1 x3 x5 = &0)`)
THEN RESA_TAC
THEN MRESA_TAC REAL_LE_INV[`ups_x x1 x2 x6`]
THEN MRESA_TAC REAL_LE_MUL[`inv(ups_x x1 x2 x6)`;`ups_x x1 x3 x5`]
THEN MRESA_TAC SQRT_POW2[`inv (ups_x x1 x2 x6) * ups_x x1 x3 x5`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(inv x1 pow 2 * &1 * inv (ups_x x1 x2 x6) * ups_x x1 x3 x5) *
 x1 *
 (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)
= (inv x1 *x1) * inv x1  * inv (ups_x x1 x2 x6) * ups_x x1 x3 x5 *
 (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)`]
THEN MRESA_TAC REAL_EQ_MUL_LCANCEL[`ups_x x1 x2 x6`;`(inv (&2) pow 2 * inv x1) * (x1 + x3 - x5) pow 2 +
 &1 *
 inv x1 *
 inv (ups_x x1 x2 x6) *
 ups_x x1 x3 x5 *
 (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)`;`x3:real`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC REAL_MUL_LINV[`ups_x x1 x2 x6`]
THEN ASM_REWRITE_TAC[REAL_ARITH`ups_x x1 x2 x6 *
 ((inv (&2) pow 2 * inv x1) * (x1 + x3 - x5) pow 2 +
  &1 *
  inv x1 *
  inv (ups_x x1 x2 x6) *
  ups_x x1 x3 x5 *
  (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))
= inv x1 *( ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2/ &4 +
    (inv (ups_x x1 x2 x6) * ups_x x1 x2 x6 ) *
  ups_x x1 x3 x5 *
  (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))`] 
THEN MRESA_TAC REAL_EQ_MUL_LCANCEL[`x1:real`;`inv x1 *
 (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 +
  &1 * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))`;`ups_x x1 x2 x6 * x3`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_REWRITE_TAC[REAL_ARITH`x1 *
 inv x1 *
 (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 +
  &1 * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))
= (inv x1 *x1) *
 (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 +
   ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))/\ a pow 2=a*a`;ups_x]
THEN REAL_ARITH_TAC);;

let EYYPQDW_NORM_V3_V1=
prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
/\ a IN {-- &1, &1}
/\ &0< ups_x x1 x3 x5
/\ (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))=v3
==>
 norm (v3-v1)  pow 2= x5`,

STRIP_TAC
THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_LSUB;DOT_RSUB]
THEN MP_TAC EYYPQDW_NORMV3
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[GSYM DOT_SQUARE_NORM;]
THEN REPEAT RESA_TAC
THEN MRESA_TAC DOT_SYM[`v3:real^3`;`v1:real^3`]
THEN REWRITE_TAC[REAL_ARITH`x3 - v1 dot v3 - (v1 dot v3 - x1) = x5
<=> v1 dot v3 = (x1+x3-x5)/ &2`]
THEN EXPAND_TAC"v3"
THEN REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS;REAL_INV_MUL]
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`)
THEN RESA_TAC
THEN MRESA_TAC REAL_MUL_LINV[`x1:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`((inv (&2) * inv x1) * (x1 + x3 - x5)) * x1
= (inv x1 * x1) * (x1 + x3 - x5)/ &2 `]
THEN REAL_ARITH_TAC);;

let EYYPQDW_SCALAR_POS=
prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
/\ a IN {-- &1, &1}
/\ &0< ups_x x1 x3 x5
/\ (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))=v3
==>
 (?t. &0<t/\ v3 cross v1= (a*t)%(v1 cross v2))`,

STRIP_TAC
THEN EXPAND_TAC"v3"
THEN REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS;REAL_INV_MUL;CROSS_LAGRANGE;CROSS_LADD;VECTOR_ARITH`A-B=A+(--B):real^3/\ a % vec 0= vec 0 /\ vec 0 +A=A`;CROSS_LMUL;CROSS_REFL;CROSS_LADD;CROSS_LNEG;DOT_SQUARE_NORM]
THEN MRESA_TAC CROSS_SKEW[`v2:real^3`;`v1:real^3`]
THEN REWRITE_TAC[VECTOR_ARITH`(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) %
     --(x1 % --(v1 cross v2))
= ((inv x1 *x1) * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) %
     (v1 cross v2)`]
THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_MUL_LINV[`x1:real`][REAL_ARITH`&1*a=a`]
THEN EXISTS_TAC`sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC SQRT_POS_LT
THEN MATCH_MP_TAC REAL_LT_MUL
THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ]
THEN MATCH_MP_TAC (REAL_ARITH`&0<=a /\ ~(a= &0)==> &0< a`)
THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`]
THEN MRESAL_TAC (GEN_ALL Trigonometry1.DIST_UPS_X_POS)[`vec 0:real^3`;`v1:real^3`;`v2:real^3`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG]
THEN MRESAL_TAC Collect_geom.FHFMKIY[`vec 0:real^3`;`v1:real^3`;`v2:real^3`;`x1:real`;`x2:real`;`x6:real`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG]);;




let v3_defor_v1=new_definition`v3_defor_v1 a v1 v2 x1 x2 x5 x6 x3= (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))`;;
let v3_defor_v2=new_definition`v3_defor_v2 a  x1 x2 x3 x5 x6 v1 v2= (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))`;;

let LIFT_CONTINUOUS_ATREAL=
prove(`!x. lift continuous atreal x`,

REWRITE_TAC[continuous_atreal;DIST_LIFT]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`e:real`
THEN ASM_REWRITE_TAC[]);;


let LIFT_CONTINUOUS_ATREAL_I=
prove(`!x. lift o(\x. x) continuous atreal x`,

REWRITE_TAC[continuous_atreal;DIST_LIFT;o_DEF]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`e:real`
THEN ASM_REWRITE_TAC[]);;


let EYYPQDW_CONTINUOUS_AT_X=
prove_by_refinement(`&0< x1 /\ &0<x2 /\ &0< x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
/\ a IN {-- &1, &1}
 /\ &0< ups_x x1 x3 x5
==> 
 (\x3. v3_defor_v1 a v1 v2 x1 x2 x5 x6 x3)  continuous atreal (x3)`,

[
STRIP_TAC
THEN REWRITE_TAC[v3_defor_v1;CROSS_LAGRANGE]
THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS;REAL_INV_MUL;CROSS_LAGRANGE;CROSS_LADD;VECTOR_ARITH`A-B=A+(--B):real^3/\ a % vec 0= vec 0 /\ vec 0 +A=A`;CROSS_LMUL;CROSS_REFL;CROSS_LADD;CROSS_LNEG;DOT_SQUARE_NORM;o_DEF]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN STRIP_TAC;

MATCH_MP_TAC CONTINUOUS_VMUL
THEN REWRITE_TAC[o_DEF;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN REWRITE_TAC[o_DEF;LIFT_ADD]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN REWRITE_TAC[LIFT_SUB]
THEN MATCH_MP_TAC CONTINUOUS_SUB
THEN ASM_SIMP_TAC[CONTINUOUS_CONST;CONTINUOUS_LIFT_NORM_COMPOSE;LIFT_CONTINUOUS_ATREAL];

MATCH_MP_TAC CONTINUOUS_VMUL
THEN REWRITE_TAC[o_DEF;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN MRESAL_TAC CONTINUOUS_ATREAL_COMPOSE[`(\x. lift (inv (ups_x x1 x2 x6) * ups_x x1 x x5))`;`lift o sqrt o drop`;`x3:real`][o_DEF;LIFT_DROP]
THEN POP_ASSUM MATCH_MP_TAC
THEN STRIP_TAC;

REWRITE_TAC[LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN REWRITE_TAC[ups_x;LIFT_ADD;]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN STRIP_TAC;

REWRITE_TAC[LIFT_SUB]
THEN MATCH_MP_TAC CONTINUOUS_SUB
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN MATCH_MP_TAC CONTINUOUS_SUB
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN ONCE_REWRITE_TAC[GSYM o_DEF;]
THEN REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1;]
THEN MATCH_MP_TAC REAL_CONTINUOUS_MUL
THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL_I];

MATCH_MP_TAC CONTINUOUS_ADD
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN STRIP_TAC;

REWRITE_TAC[o_DEF;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL];

ONCE_REWRITE_TAC[REAL_ARITH`&2 * x * x5= &2 * x5 * x`]
THEN REWRITE_TAC[o_DEF;LIFT_CMUL;]
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL];

ONCE_REWRITE_TAC[GSYM o_DEF]
THEN ONCE_REWRITE_TAC[GSYM o_DEF]
THEN MATCH_MP_TAC CONTINUOUS_AT_WITHIN
THEN MATCH_MP_TAC CONTINUOUS_AT_SQRT
THEN REWRITE_TAC[LIFT_DROP]
THEN MATCH_MP_TAC REAL_LT_MUL
THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ]
THEN MATCH_MP_TAC (REAL_ARITH`&0<=a /\ ~(a= &0)==> &0< a`)
THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`]
THEN MRESAL_TAC (GEN_ALL Trigonometry1.DIST_UPS_X_POS)[`vec 0:real^3`;`v1:real^3`;`v2:real^3`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG]
THEN MRESAL_TAC Collect_geom.FHFMKIY[`vec 0:real^3`;`v1:real^3`;`v2:real^3`;`x1:real`;`x2:real`;`x6:real`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG]]);;

let EYYPQDW_CONTINUOUS_AT_V=
prove(`&0< x1 /\ &0<x2 /\ &0< x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
/\ a IN {-- &1, &1}
 /\ &0< ups_x x1 x3 x5
==> (\v2. v3_defor_v2 a x1 x2 x3 x5 x6 v1 v2)  continuous at (v2)`,

STRIP_TAC
THEN REWRITE_TAC[v3_defor_v2;CROSS_LAGRANGE]
THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS;REAL_INV_MUL;CROSS_LAGRANGE;CROSS_LADD;VECTOR_ARITH` a % vec 0= vec 0 /\ vec 0 +A=A`;CROSS_LMUL;CROSS_REFL;CROSS_LADD;CROSS_LNEG;DOT_SQUARE_NORM;o_DEF]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN ASM_SIMP_TAC[CONTINUOUS_CONST;VECTOR_ARITH`a%(v-w)=a%v- a%w`]
THEN MATCH_MP_TAC CONTINUOUS_SUB
THEN STRIP_TAC
THENL[

MATCH_MP_TAC CONTINUOUS_CMUL
THEN MATCH_MP_TAC CONTINUOUS_VMUL
THEN ASM_SIMP_TAC[CONTINUOUS_AT_LIFT_DOT];

MATCH_MP_TAC CONTINUOUS_CMUL
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN ASM_SIMP_TAC[CONTINUOUS_AT_ID]]);;

let V3_DEFOR_V1_EQV3_DEFOR_V2=
prove(`v3_defor_v1 a v1 v2 x1 x2 x5 x6 x3=v3_defor_v2 a x1 x2 x3 x5 x6 v1 v2`,

REWRITE_TAC[v3_defor_v1;v3_defor_v2]);;

let LIFT_UPS_CONTINUOUS=
prove_by_refinement(`~(collinear{vec 0,v1,v2:real^3}) /\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
==> lift o(\x2. ups_x x1 x2 x6) continuous atreal (x2)`,

[STRIP_TAC
THEN REWRITE_TAC[ups_x;LIFT_ADD;o_DEF]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN STRIP_TAC;

REWRITE_TAC[LIFT_SUB]
THEN MATCH_MP_TAC CONTINUOUS_SUB
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN MATCH_MP_TAC CONTINUOUS_SUB
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN ONCE_REWRITE_TAC[GSYM o_DEF;]
THEN REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1;]
THEN MATCH_MP_TAC REAL_CONTINUOUS_MUL
THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL_I];

MATCH_MP_TAC CONTINUOUS_ADD
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
THEN STRIP_TAC;

REWRITE_TAC[o_DEF;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL];

ONCE_REWRITE_TAC[REAL_ARITH`&2 * x * x5= &2 * x5 * x`]
THEN REWRITE_TAC[o_DEF;LIFT_CMUL;]
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN MATCH_MP_TAC CONTINUOUS_CMUL
THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL]]);;


let MK_PLANAR_REP=
prove(`mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 a  - v0= (inv(&2 * x1) *(x1 + x3 - x5))% (v1-v0) + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%((v1-v0) cross ((v1-v0) cross (v2-v0:real^3)))`,

REWRITE_TAC[mk_planar2;LET_DEF;LET_END_DEF;real_div;VECTOR_ARITH`(a+b)-a=b:real^3`;]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`a*b=b*a`]
THEN MATCH_MP_TAC(VECTOR_ARITH`a=b==> c+a=c+b:real^3`)
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`a*b=b*a`]
THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> a%v=b %v:real^3`)
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`(a*b)*c=b*a*c`]
THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> c*a=c*b:real`)
THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> c*a=c*b:real`)
THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> sqrt(a)=sqrt(b:real)`)
THEN REAL_ARITH_TAC);;




let EYYPQDW = 
prove_by_refinement(`!v0 v1 v2 v3 x1 x2 x3 x5 x6 s.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
  x1 = dist(v1,v0) pow 2 /\
  x2 = dist(v2,v0) pow 2 /\
  x6 = dist(v1,v2) pow 2 /\
  &0 < ups_x x1 x3 x5 /\
  (s = &1 \/ s = -- &1) /\
  v3 = mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 s ==>
    (coplanar {v0,v1,v2,v3} /\
       x3 = dist(v3,v0) pow 2 /\
	x5 = dist(v3,v1) pow 2 /\
	?t. &0 < t /\
	 t % ((v3- v0) cross (v1- v0)) = ( s % ((v1 - v0) cross (v2 - v0))))`,

[
REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`]
THEN REPEAT STRIP_TAC;

MRESAL_TAC(GEN_ALL EYYPQDW_COPLANAR)[`x3:real`;`s:real`;`x2:real`;`x6:real` ;`x1:real`;`x3:real`;`x5:real`;`v1-v0:real^3`;`v2-v0:real^3`;`v3-v0:real^3`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT]
THEN REDUCE_VECTOR_TAC;

MRESAL_TAC(GEN_ALL EYYPQDW_NORMV3)[`x3:real`;`s:real`;`x2:real`;`x6:real` ;`x1:real`;`x5:real`;`v1-v0:real^3`;`v2-v0:real^3`;`v3-v0:real^3`;`x3:real`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE];

MRESAL_TAC(GEN_ALL EYYPQDW_NORM_V3_V1)[`x3:real`;`s:real`;`x2:real`;`x6:real` ;`x1:real`;`x3:real`;`v2-v0:real^3`;`v3-v0:real^3`;`v1-v0:real^3`;`x5:real`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE];

MRESAL_TAC(GEN_ALL EYYPQDW_SCALAR_POS)[`x3:real`;`x2:real`;`x6:real` ;`x1:real`;`x3:real`;`x5:real`;`v3-v0:real^3`;`s:real`;`v1-v0:real^3`;`v2-v0:real^3`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE]
THEN EXISTS_TAC`inv t`
THEN STRIP_TAC;

MATCH_MP_TAC REAL_LT_INV
THEN ASM_REWRITE_TAC[];

MP_TAC(REAL_ARITH`&0< t==> ~(t= &0)`)
THEN RESA_TAC 
THEN MRESA_TAC REAL_MUL_LINV[`t:real`]
THEN ASM_REWRITE_TAC[VECTOR_ARITH`a%b%v=(a*b)%v`;REAL_ARITH`inv t * s * t= (inv t * t)*s`]
THEN VECTOR_ARITH_TAC]);;



let MK_PLANAR_V3_DEFOR_V1=
prove(`mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 a  - v0
= v3_defor_v1 a (v1-v0) (v2-v0) x1 x2 x5 x6 x3`,

REWRITE_TAC[v3_defor_v1;MK_PLANAR_REP]);;
let MK_PLANAR_V3_DEFOR_V1_FUN=
prove(`(\q. mk_planar2 v0 v1 v2 x1 x2 q x5 x6 s)= (\x3. v3_defor_v1 s (v1-v0) (v2-v0) x1 x2 x5 x6 x3+ v0)`,

REWRITE_TAC[FUN_EQ_THM;]
THEN GEN_TAC
THEN REWRITE_TAC[GSYM MK_PLANAR_V3_DEFOR_V1]
THEN VECTOR_ARITH_TAC);;


let EYYPQDW2 = 
prove(`!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
  x1 = dist(v1,v0) pow 2 /\
  x2 = dist(v2,v0) pow 2 /\
  x6 = dist(v1,v2) pow 2 /\
  (s = &1 \/ s = -- &1)/\
  &0 < ups_x x1 x3 x5 ==>
   (\q. mk_planar2 v0 v1 v2 x1 x2 q x5 x6 s) continuous atreal x3`,

REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`]
THEN REPEAT STRIP_TAC
THEN ASM_SIMP_TAC[MK_PLANAR_V3_DEFOR_V1_FUN]
THEN MRESAL_TAC(GEN_ALL EYYPQDW_CONTINUOUS_AT_X)[`x3:real`;`s:real`;`v1-v0:real^3`;`v2-v0:real^3`;`x1:real`;`x2:real` ;`x5:real`;`x6:real`;`x3:real`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN ASM_SIMP_TAC[CONTINUOUS_CONST]);;

let MK_PLANAR_V3_DEFOR_V2_FUN=
prove(`(\q. mk_planar2 v0 v1 q x1 x2 x3 x5 x6 s)= (\v2. v3_defor_v2 s x1 x2 x3 x5 x6 (v1-v0) (v2-v0) + v0)`,

REWRITE_TAC[FUN_EQ_THM;]
THEN GEN_TAC
THEN REWRITE_TAC[v3_defor_v2;GSYM MK_PLANAR_REP]
THEN VECTOR_ARITH_TAC);;
let lemma30000=
prove(`(\v2'. v3_defor_v2 s (norm (v1 - v0) pow 2) (norm (v2 - v0) pow 2) x3 x5
        (norm (v1 - v2) pow 2)
        (v1 - v0)
        (v2' - v0))
= (\v2'. v3_defor_v2 s (norm (v1 - v0) pow 2) (norm (v2 - v0) pow 2) x3 x5
        (norm (v1 - v2) pow 2)
        (v1 - v0)
        (v2'))o(\v2. v2- v0)`,

REWRITE_TAC[o_DEF])
;;

let EYYPQDW3 =
prove(`!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
  x1 = dist(v1,v0) pow 2 /\
  x2 = dist(v2,v0) pow 2 /\
  x6 = dist(v1,v2) pow 2 /\
  (s = &1 \/ s = -- &1)/\
  &0 < ups_x x1 x3 x5 ==>
   (\q. mk_planar2 v0 v1 q x1 x2 x3 x5 x6 s) continuous at v2`,

REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`]
THEN REPEAT STRIP_TAC
THEN ASM_SIMP_TAC[MK_PLANAR_V3_DEFOR_V2_FUN]
THEN MRESAL_TAC(GEN_ALL EYYPQDW_CONTINUOUS_AT_V)[`x3:real`;`s:real`;`x1:real`;`x2:real` ;`x3:real`;`x5:real`;`x6:real`;`v1-v0:real^3`;`v2-v0:real^3`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE]
THEN MATCH_MP_TAC CONTINUOUS_ADD
THEN ASM_SIMP_TAC[CONTINUOUS_CONST;lemma30000]
THEN MATCH_MP_TAC CONTINUOUS_AT_COMPOSE
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC CONTINUOUS_SUB
THEN ASM_SIMP_TAC[CONTINUOUS_CONST;CONTINUOUS_AT_ID]);;
 end;;


(*
let check_completeness_claimA_concl = 
  Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) 
*)