(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: leg                                                               *)
(* Author: Nguyen Quang Truong                                               *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================== *)



flyspeck_needs "general/sphere.hl";;
flyspeck_needs "leg/geomdetail.hl";;
flyspeck_needs "leg/affprops.hl";;
flyspeck_needs "leg/cayleyR_def.hl";;

module Collect_geom  = struct

(*

thales:
global replace rho->rho_x

This file gives an alternative def of rho_ij, delta, chi.  
These should be reconciled with main flyspeck library


*)

  let packing = Sphere.packing;;
  let eta_x = Sphere.eta_x;;
  let eta_y = Sphere.eta_y;;
  let aff = Sphere.aff;;  (* also appears in Geomdetail *)
  let line = Sphere.line;;
  let circumcenter = Sphere.circumcenter;;
  let radV = Sphere.radV;;

  let conv = Geomdetail.conv;;
  let CONV0_SET2 = Geomdetail.CONV0_SET2;;
  let OR_IMP_EX = Geomdetail.OR_IMP_EX;;
  let CONV_SET3 = Geomdetail.CONV_SET3;;
  let INTERS_SUBSET = Geomdetail.INTERS_SUBSET;;
  let DOT_SUB_ADD = Geomdetail.DOT_SUB_ADD;;
  let trg_dist3_sym = Geomdetail.trg_dist3_sym;;
  let DIST_LT_HALF_PLANE = Geomdetail.DIST_LT_HALF_PLANE;;

  let simp_def2 = Affprops.affprops;;

  let cayleyR = Cayleyr.cayleyR;;

  let BY = Hales_tactic.BY;;

prioritize_real();;

(* dist3 is deprecated *) 

let dist3 = new_definition `dist3 (v:real^3) w = dist(v,w)`;;
 


let ups_x = new_definition ` ups_x x1 x2 x6 =
         --x1 * x1 - x2 * x2 - x6 * x6 +
         &2 * x1 * x6 +
         &2 * x1 * x2 +
         &2 * x2 * x6 `;;

(*
let rho_ij = new_definition ` rho_ij (x12 :real) x13 x14 x23 x24 x34 =
         --(x14 * x14 * x23 * x23) -
         x13 * x13 * x24 * x24 -
         x12 * x12 * x34 * x34 +
         &2 *
         (x12 * x14 * x23 * x34 +
          x12 * x13 * x24 * x34 +
          x13 * x14 * x23 * x24) `;;
*)


let rho_ij'_rho_x = new_definition `rho_ij' x1 x2 x3 x6 x5 x4 = rho_x x1 x2 x3 x4 x5 x6`;;


let rho_ij' = 
prove_by_refinement(
  `!x12 x34 x13 x14 x23 x24. rho_ij' (x12 :real) x13 x14 x23 x24 x34 =
         --(x14 * x14 * x23 * x23) -
         x13 * x13 * x24 * x24 -
         x12 * x12 * x34 * x34 +
         &2 *
         (x12 * x14 * x23 * x34 +
          x12 * x13 * x24 * x34 +
          x13 * x14 * x23 * x24)`,

  (* {{{ proof *)
  [
  (REWRITE_TAC[rho_ij'_rho_x;Sphere.rho_x]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)


let chi = new_definition ` chi x12 x13 x14 x23 x24 x34 =
         x13 * x23 * x24 +
         x14 * x23 * x24 +
         x12 * x23 * x34 +
         x14 * x23 * x34 +
         x12 * x24 * x34 +
         x13 * x24 * x34 -
         &2 * x23 * x24 * x34 -
         x12 * x34 * x34 -
         x14 * x23 * x23 -
         x13 * x24 * x24 `;;


let delta = new_definition ` delta x12 x13 x14 x23 x24 x34 =
   --(x12 * x13 * x23) -
         x12 * x14 * x24 -
         x13 * x14 * x34 -
         x23 * x24 * x34 +
         x12 * x34 * (--x12 + x13 + x14 + x23 + x24 - x34) + 
         x13 * x24 * (x12 - x13 + x14 + x23 - x24 + x34 ) +
         x14 * x23 * ( x12 + x13 - x14 - x23 + x24 + x34 ) `;;


let eta_v = new_definition ` eta_v v1 v2 (v3: real^N) =
        let e1 = dist (v2, v3) in
  	  let e2 = dist (v1, v3) in
  	  let e3 = dist (v2, v1) in
  	  e1 * e2 * e3 / sqrt ( ups_x (e1 pow 2 ) ( e2 pow 2) ( e3 pow 2 ) ) `;;


let max_real = new_definition(`max_real x y =
        if (y < x) then x else y`);;


let max_real3 = new_definition ` max_real3 x y z = max_real (max_real x y ) z `;;


let ups_x_pow2 = new_definition` ups_x_pow2 x y z = ups_x ( x*x ) ( y * y) ( z * z)`;;


let plane_norm = new_definition `
  plane_norm p <=>
         (?n v0. ~(n = vec 0) /\ p = {v | n dot (v - v0) = &0}) `;;



let delta_x34 = new_definition ` delta_x34 x12 x13 x14 x23 x24 x34  = 
-- &2 * x12 * x34 + 
(--x13 * x14 +
      --x23 * x24 +
      x13 * x24 +
      x14 * x23 +
      --x12 * x12 +
      x12 * x14 +
      x12 * x24 +
      x12 * x13 +
      x12 * x23) `;;


(*
let plane_3p = new_definition `plane_3p (a:real^3) b c =
         {x | ~collinear {a, b, c} /\
              (?ta tb tc. ta + tb + tc = &1 /\ x = ta % a + tb % b + tc % c)}`;;
*)

(* end new_definition *)

(* NGUYEN DUC PHUONG *)
(* Definition of Cayley – Menger square cm3 *)



let cm3_ups_x = new_definition `!(v1:real^3) (v2:real^3) (v3:real^3).
   cm3_ups_x v1 v2 v3 = 
  (((v2 - v1)$2 * (v3 - v1)$3 ) - ((v2 - v1)$3 * (v3 - v1)$2)) pow 2 +
  (((v2 - v1)$3 * (v3 - v1)$1 ) - ((v2 - v1)$1 * (v3 - v1)$3)) pow 2 +
  (((v2 - v1)$1 * (v3 - v1)$2 ) - ((v2 - v1)$2 * (v3 - v1)$1)) pow 2 `;;


(* Nguyen Tuyen Hoang, Nguyen Duc Phuong *)

(* The polynomial ups can be expressed as a Cayley- Menger square *)  


let lemma_cm3 = 
prove (`!(x:real^3) y. 
(x-y)$1 = x$1 - y$1 /\ (x-y)$2 = x$2 - y$2 /\ (x-y)$3 = x$3 - y$3`,
 

(REPEAT GEN_TAC) THEN (REPEAT CONJ_TAC) THENL 
[(MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 1 /\ 1 <= 3`]);
(MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 2 /\ 2 <= 3`]);
(MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 3 /\ 3 <= 3`])]);;


let lemma7 = 
prove ( `! (v1 : real ^3)(v2: real^3)(v3:real^3).
  cm3_ups_x v1 v2 v3 = 
  ups_x (norm (v1 -v2) pow 2) (norm (v2 -v3) pow 2) (norm (v3 -v1) pow 2) / &4`,


 (REPEAT GEN_TAC) THEN
 (REWRITE_TAC[cm3_ups_x; ups_x]) THEN
 (REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_3;REAL_POW_2]) THEN
 (REWRITE_TAC[lemma_cm3]) THEN
  REAL_ARITH_TAC );;


let pow_g = 
prove ( `! (x:real). &0 <= x pow 2`,

  GEN_TAC THEN REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;


let lemma8 = 
prove ( `! (v1:real^3)(v2:real^3)(v3:real^3). 
&0 <= ups_x (norm (v1 - v2) pow 2)(norm (v2 - v3) pow 2)(norm (v3 - v1) pow 2)`,

 (REPEAT GEN_TAC)
THEN (MATCH_MP_TAC (REAL_ARITH `&0 <= a/ &4 ==> &0 <= a `))
THEN (REWRITE_TAC[GSYM lemma7])
THEN (REWRITE_TAC[cm3_ups_x])

THEN (ABBREV_TAC `(a:real) = (((v2:real^3) - v1)$2 * (v3 - v1)$3 - (v2 - v1)$3 * (v3 - v1)$2) pow 2`)
THEN (FIRST_X_ASSUM ((LABEL_TAC "1") o GSYM))
THEN (ABBREV_TAC `(b:real) = (((v2:real^3) - v1)$3 * (v3 - v1)$1 - (v2 - v1)$1 * (v3 - v1)$3) pow 2`)
THEN (FIRST_X_ASSUM((LABEL_TAC "2") o GSYM))
THEN (ABBREV_TAC `(c:real) = (((v2:real^3) - v1)$1 * (v3 - v1)$2 - (v2 - v1)$2 * (v3 - v1)$1) pow 2`)
THEN (FIRST_X_ASSUM((LABEL_TAC "3") o GSYM))

THEN (MATCH_MP_TAC (SPEC_ALL REAL_LE_ADD))
THEN CONJ_TAC
THEN (ASM_REWRITE_TAC[pow_g])
THEN (MATCH_MP_TAC (SPEC_ALL REAL_LE_ADD))
THEN CONJ_TAC
THEN (ASM_REWRITE_TAC[pow_g]));;

(* ========== *)
(* QUANG TRUONG *)
(* ============ *)
let GONTONG = REAL_RING ` ((a + b) + c = a + b + c ) `;;

let SUB_SUM_SUB = REAL_RING ` (a - ( b + c ) = a - b - c )/\( a - (b- c) = a - b + c )` ;;

(* lemma 4, p 7 *)

let JVUNDLC = 
prove(`!a b c s.
     s = (a + b + c) / &2
     ==> &16 * s * (s - a) * (s - b) * (s - c) =
         ups_x (a pow 2) (b pow 2) (c pow 2)`,
 SIMP_TAC [ ups_x] THEN 
REWRITE_TAC[REAL_FIELD` a / &2 - b = ( a - &2 * b ) / &2 `] THEN 
REWRITE_TAC[REAL_FIELD ` &16 * ( a / &2 ) * ( b / &2 ) * (c / &2 ) *
( d / &2 ) = a * b * c * d `] THEN REAL_ARITH_TAC);;

let SET_TAC =
   let basicthms =
    [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
     IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in
   let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @
                 [IN_ELIM_THM; IN] in
   let PRESET_TAC =
     TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN
     REPEAT COND_CASES_TAC THEN
     REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
     REWRITE_TAC allthms in
   fun ths ->
     PRESET_TAC THEN
     (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
     MESON_TAC[];;

 let SET_RULE tm = prove(tm,SET_TAC[]);;

(* some TRUONG TACTICS *)

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

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

let DAO = NGOAC THEN REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a`];;

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

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

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

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

let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (tm)];;
let STRIP_TR = REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC)
      THEN REWRITE_TAC[IMP_IMP] THEN PHA;;


let elimin = REWRITE_RULE[IN];;


let CONV_EM = 
prove(`conv {} = {}:real^A->bool`,

  REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin
NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]
  THEN REAL_ARITH_TAC);;


let CONV_SING = 
prove(`!u. conv {u:real^A} = {u}`,

 REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;
 elimin IN_SING] THEN REPEAT GEN_TAC THEN
 REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN
 REPEAT STRIP_TAC THENL [ASM_MESON_TAC[VECTOR_MUL_LID];
 ASM_REWRITE_TAC[]] THEN EXISTS_TAC `\ (v:real^A). &1` THEN
 MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`] );;

let IN_ACT_SING = SET_RULE `! a x. ({a} x <=> a = x ) /\ ( x IN {a} <=> x = a) /\ {a} a`;;

let IN_SET2 = SET_RULE `!a b x.
         (x IN {a, b} <=> x = a \/ x = b) /\ ({a, b} x <=> x = a \/ x = b)`;;


let SUM_DIS2 = 
prove(`! x y f. ~(x=y) ==> sum {x,y} f = f x + f y `,
REWRITE_TAC[
   SET_RULE ` ~( x = y)
 <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; SUM_CLAUSES; SUM_SING]);;



let VSUM_DIS2 = 
prove(` ! x y f. ~(x=y) ==>  vsum {x,y} f = f x + f y`,
 REWRITE_TAC[
   SET_RULE ` ~( x = y)
 <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; VSUM_CLAUSES; VSUM_SING]);;


let NOV10 = 
prove(` ! x y. (x = y
      ==> (!x. y = x <=>
               (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x = a % y + b % y))) `,

REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN 
REWRITE_TAC[ MESON[VECTOR_MUL_LID]` a + b = &1 /\ x = (a + b) % y <=> a + b = &1 /\ 
x = y`]THEN REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN NGOAC THEN 
REWRITE_TAC[LEFT_EXISTS_AND_THM] THEN MATCH_MP_TAC (MESON[]` a ==> ( x = y <=> a /\
 y = x )`)THEN EXISTS_TAC `&0` THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;



let TRUONG_LEMMA = 
prove
  (  `!x y x':real^N.
       (?f. x' = f x % x + f y % y /\ (&0 <= f x /\ &0 <= f y) /\
            f x + f y = &1) <=>
       (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % x + b % y)`   ,

   REPEAT GEN_TAC THEN EQ_TAC 
THENL [MESON_TAC[]; STRIP_TAC] THEN
   ASM_CASES_TAC `y:real^N = x` THENL
    [EXISTS_TAC `\x:real^N. &1 / &2`;
     EXISTS_TAC `\u:real^N. if u = x then (a:real) else b`] THEN
   ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
   CONV_TAC REAL_RAT_REDUCE_CONV);;


let CONV_SET2 = 
prove(` ! x y:real^A. conv {x,y} = {w | ? a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
  w = a%x + b%y}`,

ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
  ==> P a b )`] THEN 
REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN 
SIMP_TAC[] THEN REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV_SING; FUN_EQ_THM;
 IN_ELIM_THM] THEN REWRITE_TAC[ IN_ACT_SING] THEN REWRITE_TAC[NOV10] THEN 
REWRITE_TAC[conv; sgn_ge; affsign; lin_combo] THEN 
REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN 
ONCE_REWRITE_TAC[ MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
  ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN 
REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\x' = vsum {x, y} ff /\ l /\ 
sum {x, y} f = &1 <=> ~(x = y) /\ x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN 
REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 <= f w) <=> &0 <= f x /\ &0 <= f y`] 
THEN ONCE_REWRITE_TAC[ GSYM (MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
  ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN 
REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN REWRITE_TAC[ TRUONG_LEMMA]);;


let LE_OF_ZPGPXNN = 
prove(` ! a b v v1 v2 . &0 <= a /\ &0 <= b /\ a + b = &1 /\
 v = a % v1 + b % v2  ==> dist ( v,v1) + dist (v,v2) = dist(v1,v2)`,
 
SIMP_TAC[dist; REAL_ARITH ` a + b = &1 <=> b = &1 - a `] THEN 
REWRITE_TAC[VECTOR_ARITH ` (a % v1 + (&1 - a) % v2) - v1 = ( a - &1 )%( v1 - v2)`] THEN 
REWRITE_TAC[VECTOR_ARITH` (a % v1 + (&1 - a) % v2) - v2 = a % ( v1 - v2) `] THEN 
SIMP_TAC[NORM_MUL; GSYM REAL_ABS_REFL] THEN REWRITE_TAC[ REAL_ARITH ` abs ( a - &1 )
 = abs ( &1 - a ) `] THEN REAL_ARITH_TAC);;


let LENGTH_EQUA = 
prove(` ! v v1 v2. v IN conv {v1,v2} ==> dist (v,v1) + 
 dist (v,v2) = dist (v1,v2) `,
REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN 
MESON_TAC[LE_OF_ZPGPXNN]);;

(* lemma 10. p 14 *)

let ZPGPXNN = 
prove(`!v1 v2 v. dist (v1,v2) < dist (v,v1) + dist (v,v2) ==> 
 ~(v IN conv {v1, v2})`,

REWRITE_TAC[MESON[] `a ==> ~ b <=> ~(a /\ b )`] THEN REWRITE_TAC[CONV_SET2; IN_ELIM_THM]
THEN MESON_TAC[LE_OF_ZPGPXNN; REAL_ARITH ` a < b ==> ~ ( a = b ) `]);;

let REDUCE_T2 = MESON[]` !P Q.
     (!v1 v2 v3 t1 t2 t3. P v1 t1 v2 t2 v3 t3 <=> P v2 t2 v1 t1 v3 t3) /\
     (!v1 v2 v3. Q v1 v2 v3 <=> Q v2 v1 v3) /\
     (!v1 v2 v3 t1 t2 t3.
          ~(t1 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)
     ==> (!v1 v2 v3 t1 t2 t3.
              ~(t1 = &0 /\ t2 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3
              ==> Q v1 v2 v3)`;;


let VEC_PER2_3 = VECTOR_ARITH `((a:real^N ) + b + c = b + a + c)/\
   ( (a:real^N ) + b + c = c + b + a )`;;
let PER2_IN3 = SET_RULE `  {a,b,c} = {b,a,c} /\ {a,b,c} = {c,b,a}`;;

let REDUCE_T3 = MESON[]`!P Q.
     (!v1 v2 v3 t1 t2 t3. P v1 t1 v2 t2 v3 t3 <=> P v3 t3 v2 t2 v1 t1) /\
     (!v1 v2 v3. Q v1 v2 v3 <=> Q v3 v2 v1) /\
     (!v1 v2 v3 t1 t2 t3. ~(t1 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)
     ==> (!v1 v2 v3 t1 t2 t3.
              ~(t1 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)`;;


let SUB_PACKING = 
prove(`!sub s.
     packing s /\ sub SUBSET s
     ==> (!x y. x IN sub /\ y IN sub /\ ~(x = y) ==> &2 <= dist3 x y)`,

REWRITE_TAC[ packing; GSYM dist3] THEN SET_TAC[]);;


let PAIR_EQ_EXPAND =
 SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`;;

let IN_SET3 = SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `;;
let IN_SET4 = SET_RULE ` x IN {a,b,c,d} <=> x = a \/ x = b \/ x = c \/ x = d `;;

(* le 8. p 13 *)

let SGFCDZO = 
prove(`! (v1:real^3) v2 v3 t1 t2 t3.
     t1 % v1 + t2 % v2 + t3 % v3 = vec 0 /\
     t1 + t2 + t3 = &0 /\
     ~(t1 = &0 /\ t2 = &0 /\ t3 = &0)
     ==> collinear {v1, v2, v3}`,
 
ONCE_REWRITE_TAC[MESON[]` a /\ b/\c <=> c /\ a /\ b `] THEN 
MATCH_MP_TAC REDUCE_T2 THEN 
CONJ_TAC THENL [SIMP_TAC[VEC_PER2_3; REAL_ADD_AC]; CONJ_TAC THENL 
  [SIMP_TAC[PER2_IN3]; MATCH_MP_TAC REDUCE_T3]] THEN 
CONJ_TAC THENL [SIMP_TAC[REAL_ADD_AC; VEC_PER2_3]; 
CONJ_TAC THENL [SIMP_TAC[PER2_IN3];  REWRITE_TAC[]]] THEN 
REPEAT GEN_TAC THEN REWRITE_TAC[collinear] THEN 
STRIP_TAC THEN EXISTS_TAC `v2 - (v3:real^3)` THEN 
ONCE_REWRITE_TAC[MESON[]` x IN s /\ y IN s <=> 
  ( x = y \/ ~ ( x = y))/\ x IN s /\ y IN s `] THEN 
REWRITE_TAC[IN_SET3] THEN REPEAT GEN_TAC THEN 
REWRITE_TAC[MESON[]` (a \/ b) /\ c ==> d <=> (a /\ c ==> d) /\ (b /\ c ==> d)`] 
THEN CONJ_TAC THENL [DISCH_TAC THEN EXISTS_TAC `&0` THEN 
FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[]` (a ==> c) ==> a /\ b ==> c `) THEN 
MESON_TAC[VECTOR_MUL_LZERO; VECTOR_SUB_EQ]; STRIP_TAC] THENL [

ASM_MESON_TAC[] ;

EXISTS_TAC ` t3  / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN 
ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
  ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN 
REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN 
ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN 
REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
  a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN 
SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN 
MESON_TAC[VECTOR_ARITH ` --(t2 % v2 + t3 % v3) - --(t2 + t3) % v2 - 
  (t3 % v2 - t3 % v3) = vec 0`]; 

EXISTS_TAC ` ( -- t2 ) / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN 
ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
  ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN 
REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN 
ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN 
REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
  a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN 
SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN 
MESON_TAC[VECTOR_ARITH ` --(t2 % v2 + t3 % v3) - --(t2 + t3) % v3 - 
 (--t2 % v2 - --t2 % v3) =  vec 0`];


EXISTS_TAC ` ( -- t3) / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN 
ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
  ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN 
REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN 
ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN 
REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
  a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN 
SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN MESON_TAC[VECTOR_ARITH ` --(t2 + t3) % v2 
- --(t2 % v2 + t3 % v3) - (--t3 % v2 - --t3 % v3) = vec 0`];


ASM_MESON_TAC[];


EXISTS_TAC ` &1 ` THEN ASM_SIMP_TAC[VECTOR_MUL_LID];


EXISTS_TAC ` t2 / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN 
ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
  ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN 
REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN 
ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN 
REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
  a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN 
SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN 
MESON_TAC[VECTOR_ARITH ` --(t2 + t3) % v3 - --(t2 % v2 + t3 % v3) -
   (t2 % v2 - t2 % v3) = vec 0`];

EXISTS_TAC ` -- &1 ` THEN ASM_MESON_TAC[VECTOR_ARITH ` v3 - v2 = -- &1 % (v2 - v3)`];


ASM_MESON_TAC[]]);;


(* le 2. p 6 *)

let RHUFIIB = 
prove( ` !x12 x13 x14 x23 x24 x34.
         rho_ij' x12 x13 x14 x23 x24 x34 * ups_x x34 x24 x23 =
         chi x12 x13 x14 x23 x24 x34 pow 2 +
         &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `,

REWRITE_TAC[rho_ij';
 chi; delta; ups_x] THEN REAL_ARITH_TAC);;



let RIGHT_END_POINT = 
prove( `!x aa bb.
     (?a b. &0 < a /\ b = &0 /\ a + b = &1 /\ x = a % aa + b % bb) <=> x = aa`,

REPEAT GEN_TAC THEN EQ_TAC THENL [STRIP_TR THEN 
REWRITE_TAC[ MESON[REAL_ARITH `b = &0 /\ a + b = &1 <=> b= &0 /\ a = &1 `]`
   b = &0 /\ a + b = &1 /\ P a b  <=>  b = &0 /\ a = &1 /\ P (&1 ) ( &0 ) `] THEN 
MESON_TAC[VECTOR_ARITH ` &1 % aa + &0 % bb = aa `];
DISCH_TAC  THEN EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &0 ` THEN 
REWRITE_TAC[REAL_ARITH ` &0 < &1 /\ &1 + &0 = &1 `] THEN 
ASM_MESON_TAC[VECTOR_ARITH ` &1 % aa + &0 % bb = aa `]]);;


let LEFT_END_POINT = 
prove(` !x aa bb.
     (?a b. a = &0 /\ &0 < b /\ a + b = &1 /\ x = &0 % aa + &1 % bb)
  <=> x = bb `,

REWRITE_TAC[VECTOR_ARITH ` &0 % aa + &1 % bb = bb `] THEN 
MESON_TAC[REAL_ARITH ` &0 = &0 /\ &0 < &1 /\ &0 + &1 = &1 `]);;



let CONV_CONV0 = 
prove(`! x a b. x IN conv {a,b} <=> x = a \/ x = b \/ x IN conv0 {a,b} `,

REWRITE_TAC[CONV_SET2; CONV0_SET2; IN_ELIM_THM] THEN 
REWRITE_TAC[REAL_ARITH ` &0 <= a <=> a = &0 \/ &0 < a `] THEN 
KHANANG THEN REWRITE_TAC[EXISTS_OR_THM] THEN 
SIMP_TAC[MESON[REAL_ARITH ` ~(a = &0 /\ b = &0 /\ a + b = &1)`]`
  ~(a = &0 /\ b = &0 /\ a + b = &1 /\ las )` ] THEN 
REWRITE_TAC[MESON[REAL_ARITH ` a = &0 /\ a + b = &1 <=> a = &0 /\ b = &1 `]`
  a = &0 /\ &0 < b /\ a + b = &1 /\ x = a % aa + b % ba <=>
     a = &0 /\ &0 < b /\ a + b = &1 /\ x = &0 % aa + &1 % ba`] THEN 
MESON_TAC[ RIGHT_END_POINT; LEFT_END_POINT]);;


let GONTONG = REWRITE_TAC[REAL_ARITH ` ( a + b ) + c = a + b + c `];;

(* le 27. p 20 *)

let MAEWNPU = 
prove(` ?b c.
         !x12 x13 x14 x23 x24 x34.
             delta x12 x13 x14 x23 x24 x34 =
             --x12 * x34 pow 2 +
             b x12 x13 x14 x23 x24 * x34 +
             c x12 x13 x14 x23 x24 `,

REWRITE_TAC[delta; REAL_ARITH ` a - b = a + -- b `; 
  REAL_ARITH ` a * (b + c )= a * b + a * c ` ] THEN 
REWRITE_TAC[REAL_ARITH ` a * b * -- c = -- a * b * c /\ -- ( a * b ) = -- a * b `] THEN 
REWRITE_TAC[REAL_ARITH` x12 * x34 * x23 + x12 * x34 * x24 +
   --x12 * x34 * x34 = x12 * x34 * x23 + x12 * x34 * x24 +
   -- x12 * ( x34 pow 2 )  `] THEN 
REWRITE_TAC[REAL_ARITH ` ( a + b ) + c = a + b + c `] THEN 
REWRITE_TAC[REAL_ARITH ` a + b * c pow 2 + d = b * c pow 2 + a + d `] THEN 
ONCE_REWRITE_TAC[REAL_ARITH `a + b + c + d + e = a + d + b + c + e `] THEN 
REWRITE_TAC[REAL_ARITH ` a * b * c = ( a * b ) * c `] THEN 
REPLICATE_TAC 30 ( ONCE_REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x + d + e
  = a * x pow 2 + b * x + e + d `] THEN GONTONG THEN REWRITE_TAC[ REAL_ARITH 
 ` a * x pow 2 + b * x + d * x  + e = a * x pow 2 + ( b  +  d)  * x  + e`]) THEN 
REPLICATE_TAC 50 ( ONCE_REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x + d + e
  = a * x pow 2 + b * x + e + d `] THEN GONTONG THEN ONCE_REWRITE_TAC[ REAL_ARITH ` a * x pow 2 + b * x + (d * x) * h  + e
 = a * x pow 2 + ( b  +  d * h )  * x  + e`]) THEN 
EXISTS_TAC ` (\ x12 x13 x14 x23 x24. --x13 * x14 +
          --x23 * x24 +
          x13 * x24 +
          x14 * x23 +
          --x12 * x12 +
          x12 * x14 +
          x12 * x24 +
          x12 * x13 +
          x12 * x23 ) ` THEN 
EXISTS_TAC ` (\ x12 x13 x14 x23 x24. (x14 * x23) * x12 +
         (x14 * x23) * x13 +
         (--x14 * x23) * x14 +
         (--x14 * x23) * x23 +
         (x14 * x23) * x24 +
         (--x12 * x13) * x23 +
         (--x12 * x14) * x24 +
         (x13 * x24) * x12 +
         (--x13 * x24) * x13 +
         (x13 * x24) * x14 +
         (x13 * x24) * x23 +
         (--x13 * x24) * x24 ) ` THEN 
SIMP_TAC[]);;

(* ----new ------- *)


let DELTA_COEFS = new_specification ["b_coef";
 "c_coef"] MAEWNPU;;



let DELTA_X34 = 
prove(` !x12 x13 x14 x23 x24 x34.
     delta x12 x13 x14 x23 x24 x34 =
     --x12 * x34 pow 2 +
     (--x13 * x14 +
      --x23 * x24 +
      x13 * x24 +
      x14 * x23 +
      --x12 * x12 +
      x12 * x14 +
      x12 * x24 +
      x12 * x13 +
      x12 * x23) *
     x34 +
     (x14 * x23) * x12 +
     (x14 * x23) * x13 +
     (--x14 * x23) * x14 +
     (--x14 * x23) * x23 +
     (x14 * x23) * x24 +
     (--x12 * x13) * x23 +
     (--x12 * x14) * x24 +
     (x13 * x24) * x12 +
     (--x13 * x24) * x13 +
     (x13 * x24) * x14 +
     (x13 * x24) * x23 +
     (--x13 * x24) * x24`,
 REWRITE_TAC[delta] THEN REAL_ARITH_TAC);;


let C_COEF_FORMULA = 
prove(`! x12 x13 x14 x23 x24. c_coef x12 x13 x14 x23 x24
  = (x14 * x23) * x12 +
         (x14 * x23) * x13 +
         (--x14 * x23) * x14 +
         (--x14 * x23) * x23 +
         (x14 * x23) * x24 +
         (--x12 * x13) * x23 +
         (--x12 * x14) * x24 +
         (x13 * x24) * x12 +
         (--x13 * x24) * x13 +
         (x13 * x24) * x14 +
         (x13 * x24) * x23 +
         (--x13 * x24) * x24`,
 MP_TAC DELTA_COEFS THEN 
NHANH (MESON[]` (!x12 x13 x14 x23 x24 x34. p x12 x13 x14 x23 x24 x34)
  ==> (! x12 x13 x14 x23 x24. p x12 x13 x14 x23 x24 (&0) ) `) THEN 
REWRITE_TAC[DELTA_X34] THEN 
REWRITE_TAC[REAL_ARITH ` &0 pow 2 = &0 `; REAL_MUL_RZERO; REAL_ADD_LID] THEN 
SIMP_TAC[]);;


let BC_DEL_FOR = 
prove(` ! x12 x13 x14 x23 x24. b_coef x12 x13 x14 x23 x24 =
  --x13 * x14 +
          --x23 * x24 +
          x13 * x24 +
          x14 * x23 +
          --x12 * x12 +
          x12 * x14 +
          x12 * x24 +
          x12 * x13 +
          x12 * x23 /\ 
  c_coef x12 x13 x14 x23 x24 =
         (x14 * x23) * x12 +
         (x14 * x23) * x13 +
         (--x14 * x23) * x14 +
         (--x14 * x23) * x23 +
         (x14 * x23) * x24 +
         (--x12 * x13) * x23 +
         (--x12 * x14) * x24 +
         (x13 * x24) * x12 +
         (--x13 * x24) * x13 +
         (x13 * x24) * x14 +
         (x13 * x24) * x23 +
         (--x13 * x24) * x24 `,
 REWRITE_TAC[C_COEF_FORMULA] THEN 
MP_TAC DELTA_COEFS THEN NHANH (MESON[]` (!x12 x13 x14 x23 x24 x34. 
p x12 x13 x14 x23 x24 x34)
  ==> (! x12 x13 x14 x23 x24. p x12 x13 x14 x23 x24 (&1) ) `) THEN 
REWRITE_TAC[DELTA_X34; C_COEF_FORMULA] THEN 
REWRITE_TAC[REAL_ARITH ` a + b + c = a + b' + c <=> b = b' `] THEN 
SIMP_TAC[REAL_RING` a * &1 = a `]);;

(*
let AGBWHRD = prove(` !x12 x13 x14 x23 x24 x12 x13 x14 x23 x24.
         b_coef x12 x13 x14 x23 x24 pow 2 +
         &4 * x12 * c_coef x12 x13 x14 x23 x24 =
         ups_x x12 x23 x13 * ups_x x12 x24 x14`, REWRITE_TAC[BC_DEL_FOR; ups_x] THEN 
REAL_ARITH_TAC);;
*)


let COLLINEAR_EX = 
prove(` ! x y (z:real^3) . collinear {x,y,z} <=> ( ? a b c. a + b + c = &0 /\ ~ ( a = &0 /\
b = &0 /\ c = &0 ) /\ a % x + b % y + c % z = vec 0 ) `,

REWRITE_TAC[collinear] THEN 
REPEAT GEN_TAC THEN 
STRIP_TR THEN 
EQ_TAC THENL [
NHANH (SET_RULE` (!x' y'. x' IN {x, y, z} /\ y' IN {x, y, z} ==> P x' y' )
    ==> P x y /\ P x z `) THEN 
STRIP_TR THEN 
DISJ_CASES_TAC (MESON[]` c = &0 /\ c' = &0 \/ ~( c = &0 /\ c' = &0  ) `) THENL [
ASM_SIMP_TAC[VECTOR_ARITH ` x - y = &0 % t <=> y = x`] THEN 
DISCH_TAC THEN 
EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &1 ` THEN 
EXISTS_TAC ` -- &2 ` THEN 
REWRITE_TAC[REAL_ARITH ` &1 + &1 + -- &2 = &0 /\
 ~(&1 = &0 /\ &1 = &0 /\ -- &2 = &0)`; VECTOR_ARITH` &1 % x + &1 % x + 
  -- &2 % x = vec 0`];



NHANH (MESON[VECTOR_MUL_LCANCEL]` x = c % u /\
  y  = c' % u ==> c' % x = c' % (c % u) /\ c % y = c % c' % u `) THEN 
REWRITE_TAC[VECTOR_ARITH ` x = c' % c % u /\ y = c % c' % u <=>
   x = y /\ y = c % c' % u`] THEN 
REWRITE_TAC[VECTOR_ARITH ` c' % (x - y) = c % (x - z) <=> (c - c' ) % x + c' % y +
  -- c % z = vec 0 `] THEN 
ASM_MESON_TAC[REAL_ARITH ` (( c - b ) + b + -- c = &0 ) /\ (~( c = &0 ) 
   <=> ~( -- c = &0 ))`]];REWRITE_TAC[GSYM collinear] THEN MESON_TAC[SGFCDZO]]);;



let MAX_REAL_LESS_EX = 
prove(`!x y a. max_real x y <= a <=> x <= a /\ y <= a`,

REWRITE_TAC[max_real; COND_EXPAND; COND_ELIM_THM;COND_RAND; COND_RATOR] THEN 
REPEAT GEN_TAC THEN 
MESON_TAC[REAL_ARITH ` (~ ( b < a ) /\ b <= c ==> a <= c)`;  REAL_ARITH ` a < b /\ b <= c ==> a <= c `]);;



let MAX_REAL3_LESS_EX = 
prove(`! x y z a. max_real3 x y z <= a <=> x <= a /\ 
y <= a /\ z <= a `,
 REWRITE_TAC[max_real3; MAX_REAL_LESS_EX] THEN MESON_TAC[]);;


MESON[]` (!x y z.
          (P x y z <=> P y x z) /\
          (P x y z <=> P x z y) /\
          (Q x y z <=> Q y x z) /\
          (Q x y z <=> Q x z y)) /\
     (!x y z. P x y z ==> Q x y z)
     ==> (!x y z. P x y z ==> Q x y z /\ Q y x z /\ Q z x y)`;;
(* ========== *)


let UPS_X_SYM = 
prove(` ! x y z. ups_x x y z = ups_x y x z /\
  ups_x x y z = ups_x x z y `,
 REWRITE_TAC[ups_x] THEN REAL_ARITH_TAC);;

let PER_MUL3 = REAL_ARITH ` a*b*c = b * a * c /\ a *b *c = a * c * b `;;


let ETA_X_SYM = 
prove(` ! x y z. &0 <= x /\ &0 <= y /\ &0 <= z /\ &0 <= ups_x x y z ==>
  eta_x x y z = eta_x y x z /\ eta_x x y z = eta_x x z y `,

REWRITE_TAC[eta_x] THEN 
NHANH (MESON[UPS_X_SYM]` &0 <= ups_x x y z ==> &0 <= ups_x y x z 
  /\ &0 <= ups_x x z y `) THEN 
NHANH (MESON[REAL_LE_MUL]`&0 <= x /\ &0 <= y /\ &0 <= z /\ las ==> 
  &0 <= x * y * z`) THEN 
PHA THEN NHANH (MESON[REAL_LE_DIV; REAL_ARITH ` a * b * c = b * a * c 
  /\ a * b * c = a * c * b `]`
  &0 <= ups_x x y z /\ &0 <= aa /\ &0 <= bb /\ &0 <= x * y * z
     ==> &0 <= (x * y * z) / ups_x x y z /\
         &0 <= (y * x * z) / aa /\
         &0 <= (x * z * y) / bb`) THEN 
SIMP_TAC[SQRT_INJ] THEN 
MESON_TAC[UPS_X_SYM; PER_MUL3]);;


let ETA_Y_SYM = 
prove(` ! x y z. &0 <= ups_x (x * x) (y * y) (z * z) ==>
  eta_y x y z = eta_y y x z /\ eta_y x y z = eta_y x z y `,

REWRITE_TAC[eta_y] THEN REPEAT LET_TAC THEN MESON_TAC[ETA_X_SYM; REAL_LE_SQUARE]);;



let ETA_Y_SYMM = MESON[UPS_X_SYM; ETA_Y_SYM]` ! x y z. &0 <= ups_x (x * x) (y * y) (z * z)
   ==> eta_y x y z = eta_y x z y /\
         eta_y x y z = eta_y y x z /\
         eta_y x y z = eta_y z x y /\
         eta_y x y z = eta_y y z x /\
         eta_y x y z = eta_y z y x`;;



let IMPLY_POS = 
prove(`! x y z . &0 <= ups_x (x * x) (y * y) (z * z) ==>
  &0 <= ((z * z) * (x * x) * y * y) / ups_x (z * z) (x * x) (y * y) /\ 
  &0 <= ((x * x) * (y * y) * z * z) / ups_x (x * x) (y * y) (z * z) /\
  &0 <= ((y * y) * (z * z) * x * x) / ups_x (y * y) (z * z) (x * x) `,
 MP_TAC
 REAL_LE_SQUARE THEN MP_TAC REAL_LE_MUL THEN MESON_TAC[UPS_X_SYM; REAL_LE_DIV]);;

let POW2_COND = MESON[REAL_ABS_REFL; REAL_LE_SQUARE_ABS]` ! a b. &0 <= a /\ &0 <= b ==> 
( a <= b <=> a pow 2 <= b pow 2 ) `;;



let TRUONGG = 
prove(`! x y z. &0 < ups_x_pow2 z x y ==> 
 ((z * z) * (x * x) * y * y) / ups_x (z * z) (x * x) (y * y) -
    z pow 2 / &4 = ( z pow 2 * (( z pow 2 - x pow 2 - y pow 2 ) pow 2 )) 
   / (&4 * ups_x_pow2 z x y )`,

REWRITE_TAC[ups_x; ups_x_pow2] THEN CONV_TAC REAL_FIELD);;

let RE_TRUONGG = REWRITE_RULE[GSYM ups_x_pow2] TRUONGG;;


let HVXIKHW = 
prove(` !x y z.
         &0 <= x /\ &0 <= y /\ &0 <= z /\ &0 < ups_x_pow2 x y z
         ==> max_real3 x y z / &2 <= eta_y x y z`,

REWRITE_TAC[REAL_ARITH` a / &2 <= b <=> a <= &2 * b `; MAX_REAL3_LESS_EX] THEN 
REWRITE_TAC[eta_x; ups_x_pow2] THEN 
NHANH (REAL_ARITH` &0 < a ==> &0 <= a `) THEN 
DAO THEN REPEAT GEN_TAC THEN 
REWRITE_TAC[MESON[ETA_Y_SYMM]` &0 <= ups_x (x * x) (y * y) (z * z) /\ las
 ==> z <= &2 * eta_y x y z /\ x <= &2 * eta_y x y z /\ y <= &2 * eta_y x y z 
  <=> &0 <= ups_x (x * x) (y * y) (z * z) /\ las
 ==> z <= &2 * eta_y z x y /\ x <= &2 * eta_y x y z /\ y <= &2 * eta_y y z x`] THEN 
REWRITE_TAC[eta_y] THEN CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[eta_x] 
THEN NHANH (SPEC_ALL IMPLY_POS) THEN 
NHANH (SPEC_ALL (prove(` ! a b x y. &0 <= a / b /\ &0 <= x /\ &0 <= y ==>
   &0 <=  &2 * sqrt ( a/b) /\ &0 <= &2 * sqrt x /\ &0 <= &2 * sqrt y `,
REWRITE_TAC[REAL_ARITH ` &0 <= &2 * a <=> &0 <= a `] THEN 
SIMP_TAC[SQRT_WORKS]))) THEN SIMP_TAC[POW2_COND] THEN 
REWRITE_TAC[REAL_ARITH ` x <= ( &2 * y ) pow 2 <=> x / &4 <= y pow 2 `] THEN 
SIMP_TAC[ SQRT_POW_2] THEN REWRITE_TAC[ GSYM ups_x_pow2] THEN 
REWRITE_TAC[REAL_FIELD` a / b <= c <=> &0 <= c - a / b `] THEN 
SIMP_TAC[ups_x_pow2; UPS_X_SYM; RE_TRUONGG] THEN DAO THEN 
MATCH_MP_TAC (MESON[]` (a4 ==> l) ==> (a1/\a2/\a3/\a4/\a5) ==> l `) THEN 
MP_TAC REAL_LE_SQUARE THEN MP_TAC REAL_LE_MUL THEN MP_TAC REAL_LE_DIV THEN 
REWRITE_TAC[GSYM REAL_POW_2] THEN MESON_TAC[REAL_ARITH ` &0 < a ==> &0 <= &4 * a `]);;


let EXISTS_INV = REAL_FIELD` ~( a = &0 ) <=> a * &1 / a = &1 /\ &1 / a * a = &1 `;;



let REAL_LT_RDIV_0 = 
prove( `!y z. &0 < z ==> (&0 < (y / z) <=> &0 < y)`,

  MESON_TAC[REAL_LT_DIV;REAL_LT_MUL;REAL_DIV_RMUL;REAL_ARITH `&0 < x==> ~(x= &0)`]);;


let POS_EQ_INV_POS = 
prove(`!x. &0 < x <=> &0 < &1 / x`,
 GEN_TAC THEN EQ_TAC
THENL [REWRITE_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]`! b.  &0 < b 
   ==> &0 < &1 / b `];REWRITE_TAC[] THEN 
MESON_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]` &0 < b
    ==> &0 < &1 / b `; REAL_FIELD ` &1 / ( &1 / x ) = x ` ]]);;



let MIDDLE_POINT = 
prove(` ! x y (z:real^3) . collinear {x,y,z} ==> x IN conv {y,z} \/ 
y IN conv {x,z} \/  z IN conv {x,y} `,
 REWRITE_TAC[COLLINEAR_EX] THEN REPEAT 
GEN_TAC THEN 
MATCH_MP_TAC (prove(`(!(a:real) (b:real) (c:real). P a b c <=> P (--a) (--b) (--c)) /\
   ((?a b c. &0 <= a /\ P a b c) ==> l) ==>  ( ? a b c. P a b c ) ==> l `,
 DISCH_TAC THEN ASM_MESON_TAC[REAL_ARITH ` ! a. a <= &0 \/ &0 <= a`;
   REAL_ARITH ` a <= &0 <=> &0 <= -- a `])) THEN 
CONJ_TAC THENL [MESON_TAC[REAL_ARITH` a = &0 <=> -- a = &0 `; REAL_ARITH ` a + b + c = &0
  <=> --a + --b + --c = &0`; VECTOR_ARITH ` a % x + b % y + c % z = vec 0
  <=> --a % x + --b % y + --c % z = vec 0 `]; STRIP_TAC] THEN 
DISJ_CASES_TAC (REAL_ARITH ` &0 < b \/ b <= &0`) THENL
[STRIP_TR THEN REWRITE_TAC[VECTOR_ARITH ` a + b + c % z = vec 0 <=>
  --c % z = a + b `] THEN 
NHANH (MESON[VECTOR_MUL_LCANCEL]` a % x = y ==> (&1 / a) % a % x = &1 / a % y `) THEN 
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN 
REWRITE_TAC[MESON[]` a1/\a2/\a3/\a4/\a5 ==> l <=> a1 /\ a5 /\ a2 ==>
  a3/\a4 ==> l `] THEN 
NHANH (REAL_FIELD ` &0 <= a /\ &0 < b /\ a + b + c = &0 ==> 
  a / ( -- c ) + b /( -- c ) = &1 /\ ~ ( -- c = &0 )/\ &0 < -- c `) THEN 
SIMP_TAC[EXISTS_INV] THEN 
ONCE_REWRITE_TAC[MESON[POS_EQ_INV_POS]` a /\ &0 < c <=> a /\ &0 < &1 / c `] THEN 
REWRITE_TAC[VECTOR_MUL_LID; CONV_SET2; IN_ELIM_THM; GSYM (REAL_ARITH` a / b =
   &1 / b * a `)] THEN 
ONCE_REWRITE_TAC[REAL_ARITH` a / b = &1 / b * a `] THEN 
MP_TAC (GEN_ALL (MESON[REAL_ARITH`( a * &1 = a ) /\ ( &0 < a ==> &0 <= a )`; 
 REAL_LE_MUL]` &0 < &1 / c * &1 /\ ( &0 <= a \/ &0 < a ) ==> &0 <= &1 / c * a `)) THEN 
MESON_TAC[]; STRIP_TR THEN 
NHANH (MESON[REAL_ARITH` &0 <= c \/ c <= &0`]` a + b + v = &0 ==>
  &0 <= v \/ v <= &0 `) THEN 
REWRITE_TAC[MESON[]` a1/\(a2 /\ (aa\/ bb))/\ dd <=>
  (aa\/bb) /\ a1/\a2/\dd`] THEN SPEC_TAC (`a:real`, `a:real`) THEN 
SPEC_TAC (`b:real`, `b:real`) THEN SPEC_TAC (`c:real`, `c:real`) THEN 
KHANANG THEN REWRITE_TAC[(prove( `&0 <= c /\ &0 <= a /\ a + b + c = &0 /\
 ~(a = &0 /\ b = &0 /\ c = &0) /\ a % x + b % y + c % z = vec 0 /\
 b <= &0 <=> --a <= &0 /\ &0 <= --b /\ --b + --c + --a = &0 /\
 ~(--b = &0 /\ --c = &0 /\ --a = &0) /\ --b % y + --c % z + -- a % x = vec 0 /\
 --c <= &0`, MESON_TAC[
REAL_ARITH ` (a = &0 <=> --a = &0) /\ ( b <= &0 <=> &0 <= -- b ) /\
     (&0 <= a <=> --a <= &0) /\
     (a + b + c = &0 <=> --b + --c + -- a = &0)`;
VECTOR_ARITH` a % x + b % y + c % z = vec 0 <=> 
 --b % y + --c % z + --a % x = vec 0 `]))] THEN 
REWRITE_TAC[MESON[]` a \/ b ==> c <=> (a ==> c) /\(b==>c)`] THEN 
REWRITE_TAC[MESON[REAL_ARITH `&0 <= a <=> a = &0 \/ &0 < a `]`
  c <= &0 /\ &0 <= a /\ l <=> ( a = &0 \/ &0 < a ) /\ c <= &0 /\ l`] THEN 
KHANANG THEN 
REWRITE_TAC[MESON[REAL_ARITH `a = &0 /\ c <= &0 /\ a + b + c = &0 /\ b <= &0
     ==> a = &0 /\ b = &0 /\ c = &0`]`a = &0 /\      c <= &0 /\
      a + b + c = &0 /\ ~(a = &0 /\ b = &0 /\ c = &0) /\a2/\ b <= &0 <=> F `] THEN 
NHANH (MESON[REAL_FIELD ` &0 < a /\
         a + b + c = &0 ==> -- b / a + -- c / a = &1 `]`&0 < a /\      c <= &0 /\
      a + b + c = &0 /\ l ==> --b / a + --c / a = &1 `) THEN 
REWRITE_TAC[VECTOR_ARITH `  a % x + b % y + c % z = vec 0 <=>
  a % x = -- b % y + -- c % z `] THEN 
NHANH (MESON[VECTOR_MUL_LCANCEL]` a % x = y ==> &1 / a % a % x = &1 / a % y `) THEN 
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH ` &1 / a * b 
  = b / a `;VECTOR_MUL_LID ] THEN PHA THEN 
PURE_ONCE_REWRITE_TAC[MESON[REAL_FIELD ` &0 < a ==> a / a = &1`]`
   &0 < a /\ P ( a / a) <=> &0 < a /\ P ( &1 ) `] THEN 
REWRITE_TAC[VECTOR_MUL_LID ] THEN 
REWRITE_TAC[MESON[SET_RULE ` {a,b} = {b,a}`]` y IN conv {x, z} \/ z IN conv {x, y}
  <=> y IN conv {z,x} \/ z IN conv {x,y} `] THEN 
REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN 
REWRITE_TAC[ REAL_ARITH ` a <= &0 <=> &0 <= -- a `] THEN 
MESON_TAC[REAL_LE_DIV; REAL_ARITH ` &0 < a ==> &0 <= a `]]);;


let IN_CONV_COLLINEAR = 
prove(` ! (v:real^3) v1 v2. v IN conv {v1,v2} ==> 
collinear {v,v1,v2} `,
 REWRITE_TAC[COLLINEAR_EX] THEN 
REWRITE_TAC[COLLINEAR_EX; CONV_SET2; IN_ELIM_THM] THEN 
REWRITE_TAC[VECTOR_ARITH ` v = a % v1 + b % v2 <=> 
   &1 % v + -- a % v1 + -- b % v2 = vec 0 `] THEN 
MESON_TAC[REAL_ARITH `~ ( &1 = &0 ) /\ (a + b = &1 <=> &1 + --a + --b = &0 )`]);;

let PER_SET3 = SET_RULE ` {a,b,c} = {a,c,b} /\ {a,b,c} = {b,a,c} /\
  {a,b,c} = {c,a,b} /\ {a,b,c} = {b,c,a} /\ {a,b,c} = {c,b,a} `;;


let COLLINERA_AS_IN_CONV2 = 
prove(` ! x y (z:real^3) . collinear {x,y,z} <=> 
x IN conv {y,z} \/ 
y IN conv {x,z} \/  z IN conv {x,y}`,
 
MESON_TAC[PER_SET3; IN_CONV_COLLINEAR; MIDDLE_POINT]);;


let LENGTH_EQ_EX = 
prove(`!v v1 v2.
     dist (v1,v) + dist (v,v2) = dist (v1,v2) <=>
     ~(dist (v1,v2) < dist (v1,v) + dist (v,v2))`,

REPEAT GEN_TAC THEN 
REWRITE_TAC[REAL_ARITH ` ~( a < b) <=> b <= a `] THEN 
EQ_TAC THENL [REAL_ARITH_TAC; 
NHANH (MESON[DIST_TRIANGLE]` dist (v1,v) + dist (v,v2) <= dist (v1,v2)
  ==> dist(v1,v2) <= dist (v1,v) + dist (v,v2)`) THEN 
REAL_ARITH_TAC]);;


(* HARRISON have proved this lemma as following, but it must be loaded after convex.ml *)


let BETWEEN_IFF_IN_CONVEX_HULL = 
prove
  (`!v v1 v2:real^N.
         dist(v1,v) + dist(v,v2) = dist(v1,v2) <=> v IN convex hull {v1,v2}`,

   REPEAT GEN_TAC THEN ASM_CASES_TAC  `v1:real^N = v2` THENL
    [ASM_REWRITE_TAC[INSERT_AC; CONVEX_HULL_SING; IN_SING] THEN NORM_ARITH_TAC;
     REWRITE_TAC[CONVEX_HULL_2_ALT; IN_ELIM_THM] THEN EQ_TAC THENL
      [DISCH_TAC THEN EXISTS_TAC `dist(v1:real^N,v) / dist(v1,v2)` THEN
       ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; DIST_POS_LT] THEN CONJ_TAC
       THENL [FIRST_ASSUM(SUBST1_TAC o SYM) THEN NORM_ARITH_TAC; ALL_TAC] THEN
       MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
       EXISTS_TAC `dist(v1:real^N,v2)` THEN
       ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; REAL_SUB_LDISTRIB;
                    REAL_DIV_LMUL; DIST_EQ_0] THEN
       FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [DIST_TRIANGLE_EQ] o SYM) THEN
       FIRST_ASSUM(SUBST1_TAC o SYM) THEN
       REWRITE_TAC[dist; REAL_ARITH `(a + b) * &1 - a = b`] THEN
       VECTOR_ARITH_TAC;
       STRIP_TAC THEN ASM_REWRITE_TAC[dist] THEN
       REWRITE_TAC[VECTOR_ARITH `a - (a + b:real^N) = --b`;
                   VECTOR_ARITH `(a + u % (b - a)) - b = (&1 - u) % (a - b)`;
                   NORM_NEG; NORM_MUL; GSYM REAL_ADD_LDISTRIB] THEN
       REWRITE_TAC[NORM_SUB] THEN REPEAT(POP_ASSUM MP_TAC) THEN
       CONV_TAC REAL_FIELD]]);;

(* From this, your version follows easily: *)

 
let BETWEEN_IMP_IN_CONVEX_HULL = 
prove
  (`!v v1 v2. dist(v1,v) + dist(v,v2) = dist(v1,v2)
              ==> (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
                         v = a % v1 + b % v2)`,

   REWRITE_TAC[BETWEEN_IFF_IN_CONVEX_HULL; CONVEX_HULL_2; IN_ELIM_THM] THEN
   REWRITE_TAC[CONJ_ASSOC]);;




let PRE_HE = 
prove(` ! x y z. let p = ( x + y + z ) / &2 in
  ups_x_pow2 x y z = &16 * p * ( p - x ) * ( p - y ) * ( p - z ) `,

CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN 
REWRITE_TAC[ups_x_pow2; ups_x] THEN REAL_ARITH_TAC);;


let PRE_HER = 
prove(`!x y z.
     ups_x_pow2 x y z =
     &16 *
     (x + y + z) / &2 *
     ((x + y + z) / &2 - x) *
     ((x + y + z) / &2 - y) *
     ((x + y + z) / &2 - z)`,
 
REWRITE_TAC[ups_x_pow2; ups_x] THEN REAL_ARITH_TAC);;



let TRIVIVAL_LE = 
prove(`!v1 v2 v3.
     ~(v2 = v3 /\ v1 = v2)
     ==> ~(dist (v1,v2) + dist (v1,v3) + dist (v2,v3) = &0)`,

SIMP_TAC[DE_MORGAN_THM; DIST_NZ] THEN 
NHANH (MESON[DIST_POS_LE]`&0 < dist (v2,v3) \/ &0 < dist (v1,v2) ==>
  &0 <= dist(v1,v3) `) THEN MP_TAC DIST_POS_LE THEN KHANANG THEN 
REWRITE_TAC[OR_IMP_EX] THEN 
NHANH (MESON[DIST_POS_LE]`&0 < dist (v2,v3) /\ &0 <= dist (v1,v3)
  ==> &0 <= dist(v1,v2) `) THEN 
SIMP_TAC[REAL_ARITH`( &0 < a /\ &0 <= b ) /\ &0 <= c ==> ~(c + b + a = &0 ) `] THEN 
NHANH (MESON[DIST_POS_LE]`&0 < dist (v1,v2) /\ &0 <= dist (v1,v3) ==>
  &0 <= dist(v2,v3) `) THEN 
MESON_TAC[REAL_ARITH ` &0 < a /\ &0 <= b /\ &0 <= c ==> ~( a + b + c = &0 ) `]);;




let MID_COND = 
prove(` ! v v1 v2. v IN conv {v1,v2} <=> dist(v1,v) + dist(v,v2)
 = dist(v1,v2) `,
 REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[LENGTH_EQUA; DIST_SYM];
REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN 
MESON_TAC[DIST_SYM; BETWEEN_IMP_IN_CONVEX_HULL]]);;


(* lemma 9. p 13 *)

let FHFMKIY = 
prove(`!(v1:real^3) v2 v3 x12 x13 x23.
         x12 = dist (v1,v2) pow 2 /\
         x13 = dist (v1,v3) pow 2 /\
         x23 = dist (v2,v3) pow 2
         ==> (collinear {v1, v2, v3} <=> ups_x x12 x13 x23 = &0)`,

REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[COLLINERA_AS_IN_CONV2]
 THEN REWRITE_TAC[REAL_ARITH ` x pow 2 = x * x `; GSYM ups_x_pow2] THEN 
REWRITE_TAC[PRE_HER] THEN REWRITE_TAC[REAL_ENTIRE] THEN 
ONCE_REWRITE_TAC[MESON[]`( v1 IN conv {v2, v3} \/ a \/ b <=> l ) <=> 
(v1 = v2 /\ v1 = v3 ) \/  ~(v1 = v2 /\ v1 = v3) ==> ( v1 IN conv {v2, v3} 
\/ a \/ b <=> l )`] THEN REWRITE_TAC[OR_IMP_EX] THEN 
SIMP_TAC[DIST_SYM; DIST_REFL; MESON[]` a= b/\ a= c <=> b = c /\ a= b`] THEN 
SIMP_TAC[SET_RULE ` {a,a} = {a} /\ a IN {a} `; CONV_SING;
   REAL_ARITH ` (&0 + &0 + &0)/ &2 = &0 `] THEN SIMP_TAC[ TRIVIVAL_LE; 
REAL_ARITH `~( &16 = &0) /\(~( a = &0) ==> ~( a / &2 = &0))`] THEN 
REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - a = &0 <=> b + c = a `] THEN 
REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - b = &0 <=> c + a = b  `] THEN 
REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - c = &0 <=> a + b = c `] THEN 
REWRITE_TAC[MESON[SET_RULE `{a,b} = {b,a} `]`v2 IN conv {v1, v3} \/ v3 IN 
conv {v1, v2}  <=> v2 IN conv {v3,v1} \/ v3 IN conv {v1, v2}`] THEN 
REWRITE_TAC[MID_COND] THEN MESON_TAC[DIST_SYM]);;

(* le 11. p 14 *)
(* NGUYEN QUANG TRUONG *)


(* These following lemma are Multivariate/convex.ml *)



let affine_dependent = new_definition
 `affine_dependent (s:real^N -> bool) <=>
        ?x. x IN s /\ x IN (affine hull (s DELETE x))`;;

 
let AFFINE_HULL_FINITE = 
prove
  (`!s:real^N->bool.
       FINITE s
       ==> affine hull s = {y | ?u. sum s u = &1 /\ vsum s (\v. u v % v) = y}`,

   GEN_TAC THEN DISCH_TAC THEN
   REWRITE_TAC[EXTENSION; AFFINE_HULL_EXPLICIT; IN_ELIM_THM] THEN
   X_GEN_TAC `x:real^N` THEN EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
    [MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `f:real^N->real`] THEN
     STRIP_TAC THEN
     EXISTS_TAC `\x:real^N. if x IN t then f x else &0` THEN
     REWRITE_TAC[] THEN ONCE_REWRITE_TAC[COND_RAND] THEN
     ONCE_REWRITE_TAC[COND_RATOR] THEN REWRITE_TAC[VECTOR_MUL_LZERO] THEN
     ASM_SIMP_TAC[GSYM VSUM_RESTRICT_SET; GSYM SUM_RESTRICT_SET] THEN
     ASM_SIMP_TAC[SET_RULE `t SUBSET s ==> {x | x IN s /\ x IN t} = t`];
     X_GEN_TAC `f:real^N->real` THEN
     ASM_CASES_TAC `s:real^N->bool = {}` THEN
     ASM_REWRITE_TAC[SUM_CLAUSES; REAL_OF_NUM_EQ; ARITH] THEN STRIP_TAC THEN
     MAP_EVERY EXISTS_TAC [`s:real^N->bool`; `f:real^N->real`] THEN
     ASM_REWRITE_TAC[GSYM EXTENSION; SUBSET_REFL]]);;

 
let IN_AFFINE_HULL_IMP_COLLINEAR = 
prove
  (`!a b c:real^N. a IN (affine hull {b,c}) ==> collinear {a,b,c}`,

   REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
    [`a:real^N = b`; `a:real^N = c`; `b:real^N = c`] THEN
   TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
   SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_SING] THEN
   SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; FINITE_RULES; REAL_ADD_RID] THEN
   ASM_REWRITE_TAC[IN_INSERT; IN_ELIM_THM; NOT_IN_EMPTY; VECTOR_ADD_RID] THEN
   DISCH_THEN(X_CHOOSE_THEN `f:real^N->real` STRIP_ASSUME_TAC) THEN
   ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`] THEN
   ASM_REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA; VECTOR_SUB_EQ] THEN
   EXISTS_TAC `(f:real^N->real) c` THEN EXPAND_TAC "a" THEN
   FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (REAL_ARITH
    `b + c = &1 ==> b = &1 - c`)) THEN VECTOR_ARITH_TAC);;


 
let AFFINE_DEPENDENT_3_IMP_COLLINEAR = 
prove
  (`!a b c:real^N. affine_dependent{a,b,c} ==> collinear{a,b,c}`,

   REPEAT GEN_TAC THEN
   MAP_EVERY ASM_CASES_TAC
    [`a:real^N = b`; `a:real^N = c`; `b:real^N = c`] THEN
   TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
   REWRITE_TAC[affine_dependent; IN_INSERT; NOT_IN_EMPTY] THEN STRIP_TAC THEN
   FIRST_X_ASSUM SUBST_ALL_TAC THENL
    [ALL_TAC;
     ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`];
     ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`]] THEN
   MATCH_MP_TAC IN_AFFINE_HULL_IMP_COLLINEAR THEN
   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (MESON[]
    `x IN s ==> s = t ==> x IN t`)) THEN
   AP_TERM_TAC THEN ASM SET_TAC[]);;

(* LEMMA 11 *)

let FAFKVLR = 
prove
 (`!v1 v2 v3 v:real^N.
       ~collinear{v1,v2,v3} /\ v IN (affine hull {v1,v2,v3})

       ==> ?t1 t2 t3. v = t1 % v1 + t2 % v2 + t3 % v3 /\
                      t1 + t2 + t3 = &1 /\
                      !ta tb tc. v = ta % v1 + tb % v2 + tc % v3 /\

                                 ta + tb + tc = &1
                                 ==> ta = t1 /\ tb = t2 /\ tc = t3`,

 REPEAT GEN_TAC THEN
 MAP_EVERY ASM_CASES_TAC
  [`v1:real^N = v2`; `v2:real^N = v3`; `v1:real^N = v3`] THEN
 TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
 SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_SING; IN_ELIM_THM] THEN
 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; FINITE_INSERT; FINITE_SING;
          SUM_SING; VSUM_SING] THEN
 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; LEFT_IMP_EXISTS_THM] THEN
 X_GEN_TAC `f:real^N->real` THEN STRIP_TAC THEN
 MAP_EVERY EXISTS_TAC
  [`(f:real^N->real) v1`; `(f:real^N->real) v2`; `(f:real^N->real) v3`] THEN
 ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN EXPAND_TAC "v" THEN
 DISCH_TAC THEN MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
 UNDISCH_TAC `~collinear{v1:real^N,v2,v3}` THEN REWRITE_TAC[] THEN
 MATCH_MP_TAC AFFINE_DEPENDENT_3_IMP_COLLINEAR THEN
 SIMP_TAC[AFFINE_DEPENDENT_EXPLICIT_FINITE; FINITE_INSERT; FINITE_RULES;
          SUM_CLAUSES; VSUM_CLAUSES] THEN
 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
 EXISTS_TAC `\x. if x = v1 then f v1 - ta
                 else if x = v2 then f v2 - tb
                 else (f:real^N->real) v3 - tc` THEN
 ASM_REWRITE_TAC[REAL_ADD_RID; VECTOR_ADD_RID] THEN REPEAT CONJ_TAC THENL
  [ASM_REAL_ARITH_TAC;
   ASM_REWRITE_TAC[EXISTS_OR_THM; RIGHT_OR_DISTRIB; UNWIND_THM2] THEN
   ASM_REWRITE_TAC[REAL_SUB_0] THEN ASM_MESON_TAC[];
   ASM_REWRITE_TAC[VECTOR_ARITH
    `(a - a') % x + (b - b') % y + (c - c') % z = vec 0 <=>
     a % x + b % y + c % z = a' % x + b' % y + c' % z`] THEN
   ASM_MESON_TAC[]]);;



 
let FAFKVLR_ALT = 
prove
  (`!v1 v2 v3 v:real^N.
         ~collinear{v1,v2,v3} /\ v IN (affine hull {v1,v2,v3})
         ==> ?!(t1,t2,t3). v = t1 % v1 + t2 % v2 + t3 % v3 /\
                           t1 + t2 + t3 = &1`,

   REWRITE_TAC(map(REWRITE_RULE[ETA_AX])
    [EXISTS_UNIQUE; FORALL_PAIR_THM; EXISTS_PAIR_THM]) THEN
   REWRITE_TAC[PAIR_EQ; GSYM CONJ_ASSOC; FAFKVLR]);;



let equivalent_lemma = 
prove(` (?t1 t2 t3.
         !v1 v2 v3 (v:real^N).
             v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
             ==> v =
                 t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\
                 t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\
                 (!ta tb tc.
                      v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1 
                      ==> ta = t1 v1 v2 v3 v /\
                          tb = t2 v1 v2 v3 v /\
                          tc = t3 v1 v2 v3 v))  <=>
     
          ( !v1 v2 v3 (v:real^N).
             v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
          ==> (?t1 t2 t3.
                   v = t1 % v1 + t2 % v2 + t3 % v3 /\
                   t1 + t2 + t3 = &1 /\
                   (!ta tb tc.
                        v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1
                        ==> ta = t1 /\ tb = t2 /\ tc = t3))) `,


 
let LAMBDA_TRIPLED_THM = 
prove
  (`!t. (\(x,y,z). t x y z) = (\p. t (FST p) (FST(SND p)) (SND(SND p)))`,

   REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;

 
let FORALL_TRIPLED_THM = 
prove
  (`!P. (!(x,y,z). P x y z) <=> (!x y z. P x y z)`,

   REWRITE_TAC[LAMBDA_TRIPLED_THM] THEN REWRITE_TAC[FORALL_PAIR_THM]);;

 
let EXISTS_TRIPLED_THM = 
prove
  (`!P. (?(x,y,z). P x y z) <=> (?x y z. P x y z)`,

   REWRITE_TAC[LAMBDA_TRIPLED_THM] THEN REWRITE_TAC[EXISTS_PAIR_THM]);;

 
let EXISTS_UNIQUE_TRIPLED_THM = 
prove
  (`!P. (?!(x,y,z). P x y z) <=>
        (?x y z. P x y z /\
                 (!x' y' z'. P x' y' z' ==> x' = x /\ y' = y /\ z' = z))`,

   REWRITE_TAC[REWRITE_RULE[ETA_AX] EXISTS_UNIQUE] THEN
   REWRITE_TAC[FORALL_TRIPLED_THM; EXISTS_TRIPLED_THM] THEN
   REWRITE_TAC[EXISTS_PAIR_THM; FORALL_PAIR_THM; PAIR_EQ]);;


 
let theoremmm = 
prove
 (`( !v1 v2 v3 v:real^N.
      v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
      ==> (?t1 t2 t3.
               v = t1 % v1 + t2 % v2 + t3 % v3 /\
               t1 + t2 + t3 = &1 /\
               (!ta tb tc.
                    v = ta % v1 + tb % v2 + tc % v3 /\
                    ta + tb + tc = &1
                    ==> ta = t1 /\ tb = t2 /\ tc = t3)) )
   <=>
   ( !v1 v2 v3 v:real^N.
            ~collinear {v1, v2, v3} /\ v IN affine hull {v1, v2, v3}
            ==> (?!(t1,t2,t3). v = t1 % v1 + t2 % v2 + t3 % v3 /\
                               t1 + t2 + t3 = &1))`,

   REWRITE_TAC[EXISTS_UNIQUE_TRIPLED_THM] THEN REWRITE_TAC[CONJ_ACI]);;





let FAFKVLR = 
prove(` (?t1 t2 t3.
         !v1 v2 v3 (v:real^N).
             v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
             ==> v =
                 t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\
                 t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\
                 (!ta tb tc.
                      v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1 
                      ==> ta = t1 v1 v2 v3 v /\
                          tb = t2 v1 v2 v3 v /\
                          tc = t3 v1 v2 v3 v))  `,

SIMP_TAC[equivalent_lemma; FAFKVLR]);;
let LEMMA11 = FAFKVLR;;
let lemma11 = REWRITE_RULE[equivalent_lemma] FAFKVLR;;

let COEFS = new_specification ["coef1";
 "coef2"; "coef3"] FAFKVLR;;

let lem11 = REWRITE_RULE[simp_def2; IN_ELIM_THM] lemma11;;

let REAL_PER3 = REAL_ARITH `!a b c. a + b + c = b + a + c /\ a + b + c = c + b + a `;;


MESON[VEC_PER2_3]` (!ta tb tc.
      v = ta % v1 + tb % v2 + tc % v3 ==> ta = t1 /\ tb = t2 /\ tc = t3) /\bbb/\
 v = ta''' % v1 + tb''' % v2 + t''' % v3 /\
 v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
 v = ta' % v2 + tb' % v3 + t' % v1 /\
aa  ==> t' = t1 /\ t'' = t2 /\ t''' = t3 `;;

let NOT_COLLINEAR_IMP_2_UNEQUAL = MESON[INSERT_INSERT; COLLINEAR_2; INSERT_AC]
`~collinear {v0, va, vb} ==> ~(v0 = va) /\ ~(v0 = vb) `;;


let COLLINEAR_DISJOINT3  = 
prove(`!v1:real^A v2 v3. ~collinear {v1,v2,v3} ==>
  DISJOINT {v2,v3} {v1}`,

  REWRITE_TAC[DISJOINT_INSERT;DISJOINT_EMPTY;IN_INSERT;NOT_IN_EMPTY] THEN
  MESON_TAC[NOT_COLLINEAR_IMP_2_UNEQUAL]
			      );;


let COLLINEAR_DISJOINT_PERM3  = 
prove(`!v1:real^A v2 v3. (~collinear {v1,v2,v3} ==>
  DISJOINT {v1,v2} {v3}) /\ (~collinear {v1,v2,v3} ==> DISJOINT {v2,v3} {v1}) /\ 
   (~collinear {v1,v2,v3} ==> DISJOINT {v3,v1} {v2})`,

  REPEAT GEN_TAC THEN
  SUBGOAL_THEN `{v3:real^A,v1,v2} = {v1,v2,v3} /\ {v2,v3,v1}={v1,v2,v3}` MP_TAC THENL
  [SET_TAC[] ; ASM_MESON_TAC[COLLINEAR_DISJOINT3]]);;


let simp_def_ge = 
prove(` !a:real^A b v0.
          DISJOINT {a, b} {v0}
          ==> 
              aff_ge {a, b} {v0} =
              {x | ?ta tb t.
                       ta + tb + t = &1 /\
                       &0 <= t /\
                       x = ta % a + tb % b + t % v0} `,

   MESON_TAC[simp_def2]);;



let IN_CONV3_EQ = 
prove(`! (v:real^3) v1 v2 v3. ~collinear {v1,v2,v3} ==> (v IN conv {v1, v2, v3} <=> 
  v IN aff_ge {v1,v2} {v3} /\
  v IN aff_ge {v2,v3} {v1} /\ v IN aff_ge {v3,v1} {v2} )`,

SIMP_TAC[CONV_SET3; COLLINEAR_DISJOINT_PERM3;simp_def_ge; IN_ELIM_THM] THEN 
REPEAT GEN_TAC THEN DISCH_TAC THEN  EQ_TAC THENL [
MESON_TAC[REAL_ARITH` a + b + c = b + a + c /\ a + b + c = c + b + a `;
  VECTOR_ARITH `(a:real^N) + b + c = b + a + c /\ a + b + c = c + b + a `; lem11]; 
NHANH (MESON[]` (? a b c. P a b c /\ Q c /\ R a b c) /\ aa /\ bb ==>
   (? a b c. P a b c /\ R a b c) `) THEN 
FIRST_X_ASSUM MP_TAC THEN 
REWRITE_TAC[IMP_IMP] THEN 
REWRITE_TAC[MESON[]` ~a/\ b <=> b /\ ~ a `] THEN 
PHA THEN 
NHANH (SPEC_ALL lem11) THEN 
STRIP_TR THEN REWRITE_TAC[MESON[]` (v = w:real^N) /\ a <=> a /\ v = w `] THEN PHA] THEN 
NHANH (MESON[VEC_PER2_3; REAL_PER3]` ta + tb + t = &1 /\
 &0 <= t /\
 ta' + tb' + t' = &1 /\
 &0 <= t' /\
 ta'' + tb'' + t'' = &1 /\
 &0 <= t'' /\
a1/\
a2/\
 t1 + t2 + t3 = &1 /\
 (!ta tb tc.
      ta + tb + tc = &1 /\ v = ta % v1 + tb % v2 + tc % v3
      ==> ta = t1 /\ tb = t2 /\ tc = t3) /\
 v = t1 % v1 + t2 % v2 + t3 % v3 /\
a3/\
 v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
 v = ta' % v2 + tb' % v3 + t' % v1 /\
 v = ta % v1 + tb % v2 + t % v3 ==> t1 = t' /\ t2 = t'' /\ t3 = t`) THEN 
MESON_TAC[]);;



let IN_CONV03_EQ = 
prove(
`! (v:real^3) v1 v2 v3. ~collinear {v1,v2,v3} ==> 
(v IN conv0 {v1, v2, v3} <=>   v IN aff_gt {v1,v2} {v3} /\
  v IN aff_gt {v2,v3} {v1} /\ v IN aff_gt {v3,v1} {v2} )`,

SIMP_TAC[CONV_SET3; COLLINEAR_DISJOINT_PERM3;simp_def2; IN_ELIM_THM] THEN 
REPEAT GEN_TAC THEN DISCH_TAC THEN  EQ_TAC THENL [
MESON_TAC[REAL_ARITH` a + b + c = b + a + c /\ a + b + c = c + b + a `;
  VECTOR_ARITH `(a:real^N) + b + c = b + a + c /\ a + b + c = c + b + a `; lem11]; 
NHANH (MESON[]` (? a b c. P a b c /\ Q c /\ R a b c) /\ aa /\ bb ==>
   (? a b c. P a b c /\ R a b c) `) THEN 
FIRST_X_ASSUM MP_TAC THEN 
REWRITE_TAC[IMP_IMP] THEN 
REWRITE_TAC[MESON[]` ~a/\ b <=> b /\ ~ a `] THEN 
PHA THEN 
NHANH (SPEC_ALL lem11) THEN 
STRIP_TR THEN REWRITE_TAC[MESON[]` (v = w:real^N) /\ a <=> a /\ v = w `]]
 THEN PHA THEN NHANH (MESON[VEC_PER2_3; REAL_PER3]`
  ta + tb + t = &1 /\
 &0 < t /\
 ta' + tb' + t' = &1 /\
 &0 < t' /\
 ta'' + tb'' + t'' = &1 /\
 &0 < t'' /\ a33 /\ a22 /\
 t1 + t2 + t3 = &1 /\
 (!ta tb tc.
      ta + tb + tc = &1 /\ v = ta % v1 + tb % v2 + tc % v3
      ==> ta = t1 /\ tb = t2 /\ tc = t3) /\
 v = t1 % v1 + t2 % v2 + t3 % v3 /\ a11 /\
 v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
 v = ta' % v2 + tb' % v3 + t' % v1 /\
 v = ta % v1 + tb % v2 + t % v3 ==>
  t1 = t' /\ t2 = t'' /\ t3 = t `) THEN MESON_TAC[]);;



let AFFINE_SET_GEN_BY_TWO_POINTS =

prove(`! a b. affine {x | ?ta tb. ta + tb = &1 /\ x = ta % a + tb % b}`,

REWRITE_TAC[affine; IN_ELIM_THM] THEN 
REPEAT GEN_TAC THEN 
STRIP_TAC THEN 
EXISTS_TAC ` u * ta + v * ta' ` THEN 
EXISTS_TAC ` u * tb + v * tb' ` THEN 
REWRITE_TAC[REAL_ARITH ` (u * ta + v * ta') + u * tb + v * tb' =
  u * (ta + tb) + v * (ta' + tb' ) `] THEN 
ASM_SIMP_TAC[REAL_ARITH ` a * &1 = a `] THEN 
CONV_TAC VECTOR_ARITH);;

let SET2_SU_EX = SET_RULE` {(a:A),b} SUBSET s <=> a IN s /\ b IN s `;;


let GENERATING_POINT_IN_SET_AFF = 
prove(` ! a b. {a,b} SUBSET {x | ?ta tb. 
ta + tb = &1 /\ x = ta % a + tb % b}`,
REWRITE_TAC[SET2_SU_EX; IN_ELIM_THM]
THEN REPEAT GEN_TAC THEN 
MESON_TAC[REAL_ARITH` &0 + &1 = &1 /\ a + b = b + a`; VECTOR_ARITH `
  a = &0 % b + &1 % a /\ a = &1 % a + &0 % b `]);;



let AFF_2POINTS_INTERPRET = 
prove(`!a b. aff {a, b} = {x | ?ta tb. ta + tb = &1 /\ x = ta % a + tb % b}`,

REWRITE_TAC[aff; hull] THEN 
REPEAT GEN_TAC THEN 
REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN 
SIMP_TAC[INTERS_SUBSET; AFFINE_SET_GEN_BY_TWO_POINTS;
  GENERATING_POINT_IN_SET_AFF] THEN 
REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN 
REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTERS; affine] THEN 
SET_TAC[]);;


(* corrected with DISJOINT by thales *)


let IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF = 
prove(` ! v v1 v2 v3 . 
   DISJOINT{v1,v2} {v3} ==>
(v IN aff_ge {v1,v2} {v3} <=> v IN aff_gt {v1,v2} {v3} \/
  v IN aff {v1,v2}) `,

REPEAT STRIP_TAC THEN 
ASM_SIMP_TAC[simp_def2; AFF_2POINTS_INTERPRET; IN_ELIM_THM ] THEN 
REWRITE_TAC [REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `] THEN 
MESON_TAC[REAL_ARITH ` (&0 <= a <=> &0 < a \/ a = &0 )/\( a + &0 = a ) `;
  VECTOR_ARITH ` a + &0 % c = a `]);;

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



let AFFINE_AFF_HULL = 
prove(` ! s. affine ( aff s ) `,
 
REWRITE_TAC[aff; AFFINE_AFFINE_HULL]);;



let AFFINE_CONTAIN_LINE = 
prove(`! a b s. affine s /\ {a,b} SUBSET s ==>
 aff {a,b} SUBSET s `,

REWRITE_TAC[affine ; AFF_2POINTS_INTERPRET; IN_ELIM_THM] THEN SET_TAC[]);;


let VECTOR_SUB_DISTRIBUTE = VECTOR_ARITH ` ! a x y. a % x - a % y = a % ( x - y ) `;;



let CHANGE_SIDE = 
prove(` ~( a = &0 ) ==> ( x = a % y <=> ( &1 / a) % x = y )`,

MESON_TAC[ VECTOR_ARITH `  ( a * b ) % x = a % b % x `; VECTOR_MUL_LID;
  REAL_FIELD `~( a = &0 ) ==>  a * &1 / a = &1 `; VECTOR_MUL_LCANCEL]);;



let PRE_INVERSE_SUB = 
prove(` ! a b v w. {a, b} SUBSET aff {v, w} /\ ~(a = b)
 ==> {v, w} SUBSET aff {a, b}`,
 
REWRITE_TAC[AFF_2POINTS_INTERPRET; SET2_SU_EX; IN_ELIM_THM] THEN 
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN 
REWRITE_TAC[IMP_IMP] THEN PHA THEN 
NHANH (MESON[]` (a:real^N) = b /\ gg /\ a' = b' /\ ll ==> a - a' = b - b' `) THEN 
REWRITE_TAC[VECTOR_ARITH` (ta % v + tb % w) - (ta' % v + tb' % w) =
  ( ta - ta') % v + ( tb - tb' ) % w `] THEN 
PHA THEN REWRITE_TAC[MESON[]` a = &1 /\ b <=> b /\ a = &1 `] THEN PHA THEN 
NHANH (REAL_ARITH ` ta + tb = &1 /\ ta' + tb' = &1 ==> ta' - ta = tb - tb' `) THEN 
REWRITE_TAC[VECTOR_ARITH ` a + ( x - y ) % b = a - ( y - x) % b `] THEN 
REWRITE_TAC[MESON[]` a - b = ta % v - tb % w /\aa/\
   ta = tb <=> a - b = ta % v - ta % w /\ aa /\ ta = tb `] THEN 
ASM_CASES_TAC `(ta:real) = ta' ` THENL [ASM_SIMP_TAC[REAL_SUB_REFL; 
VECTOR_MUL_LZERO; VECTOR_SUB_RZERO; VECTOR_SUB_EQ] THEN MESON_TAC[]; ALL_TAC] THEN 
REWRITE_TAC[VECTOR_SUB_DISTRIBUTE] THEN FIRST_X_ASSUM MP_TAC THEN 
ONCE_REWRITE_TAC[REAL_ARITH` ~( a = b) <=> ~( a - b = &0 )`] THEN IMP_IMP_TAC THEN 
REWRITE_TAC[MESON[]` ~( a = b:real) /\ l <=> l /\ ~(a = b) `; MESON[]` 
a = d % b /\ l  <=> l /\  a = d % b `] THEN PHA THEN 
REWRITE_TAC[MESON[CHANGE_SIDE]` x = a % y /\ ~( a = &0 ) <=>  &1 / a % x = y /\
 ~( a = &0 )`] THEN NHANH (MESON[VECTOR_MUL_LCANCEL]` ta - ta' = tb' - tb /\
 a = b  /\ l ==> tb % a = tb % b /\ ta % a = ta % b `) THEN 
ONCE_REWRITE_TAC[MESON[]` a = (b:real^n) /\ l <=> l /\ a = b `] THEN PHA 
THEN REWRITE_TAC[GSYM VECTOR_SUB_DISTRIBUTE] THEN 
ONCE_REWRITE_TAC[VECTOR_ARITH` a = (b:real^N) /\ a1 = (b1:real^N) /\ a2 = 
  (b2:real^N) <=> a2 = b2 /\ a + a2 = b + b2 /\ a2 - a1 = b2 - b1 `] THEN 
REWRITE_TAC[VECTOR_ARITH` (ta % v + tb % w) - (ta % v - ta % w) = ( ta + tb ) % w `;
  VECTOR_ARITH` tb % v - tb % w + ta % v + tb % w = ( ta + tb ) % v `] THEN 
REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ARITH` a - ( x % a - y % b ) = 
(&1 - x ) % a + y % b `] THEN REWRITE_TAC[VECTOR_ARITH` a % x - b % y + x = 
(a + &1 ) % x + --b % y `] THEN 
REWRITE_TAC[MESON[]` a = &1 /\ b = &1 /\ l <=> a = &1 /\ l /\b = &1 `] THEN 
DAO THEN MATCH_MP_TAC (MESON[]`( a1 /\a2/\a3/\a5 ==> l) ==> 
(a1/\a2/\a3/\a4/\a5/\a6   ==> l ) `) THEN PURE_ONCE_REWRITE_TAC[ MESON[]`
 a + b = &1 /\ P ( a + b ) <=> a + b = &1 /\  P (&1) `] THEN 
REWRITE_TAC[VECTOR_MUL_LID] THEN MESON_TAC[REAL_FIELD ` ~(ta - ta' = &0)
     ==> (tb * &1 / (ta - ta') + &1) + --(tb * &1 / (ta - ta')) = &1 /\ 
  &1 - ta * &1 / (ta - ta') + ta * &1 / (ta - ta') = &1 `]);;




let LEMMA5 = 
prove(
`!(a:real^N) b x. line x /\ {a, b} SUBSET x /\ ~(a = b) ==> x = aff {a, b}`,

REWRITE_TAC[line; GSYM aff] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN 
REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN ASM_SIMP_TAC[AFFINE_AFF_HULL; 
AFFINE_CONTAIN_LINE] THEN STRIP_TR THEN 
ABBREV_TAC ` (ki : bool ) = aff {(v:real^N), (w:real^N)} 
  SUBSET aff {(a:real^N), (b:real^N)}` THEN 
REWRITE_TAC[MESON[]` a/\b/\c ==> d <=> b ==> a/\c ==> d `] THEN SIMP_TAC[]
THEN DISCH_TAC THEN IMP_IMP_TAC THEN 
NHANH (MESON[PRE_INVERSE_SUB]`{a, b} SUBSET aff {v, w} /\ aa /\ ~(a = b) 
  ==> {v, w} SUBSET aff {a, b} `) THEN 
NHANH (MESON[AFFINE_AFF_HULL]` aa /\ v SUBSET aff {a, b} ==> affine (aff {a,b})`)
THEN DOWN_TAC THEN MESON_TAC[AFFINE_CONTAIN_LINE]);;

let RCEABUJ = LEMMA5;;


let COL_EQ_UPS_0 = GEN_ALL (MESON[FHFMKIY]` collinear {(v1:real^3), v2, v3} <=>
 ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0`);;




let EQ_POW2_COND = 
prove(`!a b. &0 <= a /\ &0 <= b ==> (a = b <=> a pow 2 = b pow 2)`,

REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN SIMP_TAC[POW2_COND]);;


let D3_POS_LE = MESON[dist3; DIST_POS_LE]` ! x y. &0 <= dist3 x y `;;



let delta_x12 = new_definition ` delta_x12 x12 x13 x14 x23 x24 x34 =
  -- x13 * x23 + -- x14 * x24 + x34 * ( -- x12 + x13 + x14 + x23 + x24 + -- x34 )
  + -- x12 * x34 + x13 * x24 + x14 * x23 `;;


let delta_x13 = new_definition` delta_x13 x12 x13 x14 x23 x24 x34 =
  -- x12 * x23 + -- x14 * x34 + x12 * x34 + x24 * ( x12 + -- x13 + x14 + x23 + 
  -- x24 + x34 ) + -- x13 * x24 + x14 * x23 `;;


let delta_x14 = new_definition`delta_x14 x12 x13 x14 x23 x24 x34 =
         --x12 * x24 +
         --x13 * x34 +
         x12 * x34 +
         x13 * x24 +
         x23 * (x12 + x13 + --x14 + --x23 + x24 + x34) +
         --x14 * x23`;;




let DIST_POW2_DOT =

prove(` ! a (b:real^N) . dist (a,b) pow 2 = ( a - b ) dot ( a- b) `,


(* REMOVED. thales
(* the following lemma is in Multivariate/convex.ml *)
let AFFINE_HULL_3 = new_axiom_removed` affine hull {a,b,c} =
    { u % a + v % b + w % c | u + v + w = &1}`;;
*)

let LET_TR = CONV_TAC (TOP_DEPTH_CONV let_CONV);;


(* BEGINING *)
(* lemma 16 SDIHJZK *)


let TO_UYCH = 
prove(` &0 < ups_x a12 a13 a23 ==>
  delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 +
     delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 +
     delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 =
     &1 `,

REWRITE_TAC[ups_x; delta_x12; delta_x13; delta_x14] THEN CONV_TAC REAL_FIELD);;





let NOT_UPS_X_ZERO_IMP_SMT = 
prove(`~(ups_x a12 a13 a23 = &0)
 ==> (delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a12 +
     delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
     delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
     (a12 + a13 - a23) +
     (delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a13 
     =
     a01 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 /\

(delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a23 +
     delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
     delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
     (a23 + a12 - a13) +
     (delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a12 
      =
     a02 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 /\

(delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a13 +
     delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
     delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
     (a13 + a23 - a12) +
     (delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a23 =
     a03 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23`,

ONCE_REWRITE_TAC[REAL_FIELD` ~( a = &0 ) ==> ( x = y ) /\ ( xx = yy ) /\ ( xxx = yyy)
  <=> ~( a = &0 ) ==> ( x * a pow 2 = y * a pow 2 ) /\
  ( xx * a pow 2 = yy * a pow 2 ) /\
  ( xxx * a pow 2 = yyy * a pow 2 ) `] THEN 
SIMP_TAC[REAL_FIELD` ~( a = &0 ) ==> ( b - c / a ) * a pow 2 = b * a pow 2 - c * a `
  ; REAL_ADD_RDISTRIB] THEN 
SIMP_TAC[REAL_ARITH` ( a * b ) * c = a * b * c `;
  REAL_FIELD` ~ ( a = &0 ) ==> ( b / a ) pow 2 * c * a pow 2 =
  b pow 2 * c `; REAL_FIELD ` ~ ( a = &0 ) ==> b / a * c / a * d * 
  a pow 2 = b * c * d `] THEN DISCH_TAC THEN 
REWRITE_TAC[delta_x12; delta_x13; delta_x14; delta; ups_x] THEN REAL_ARITH_TAC);;


let TROI_OI_DAT_HOI = MESON[ lemma8; dist; DIST_SYM]` &0 <=
           ups_x ( dist((v1:real^3),v2) pow 2) (dist(v2,v3) pow 2)
           (dist(v1,v3) pow 2)`;;



let ZERO_LE_UPS_X = MESON[TROI_OI_DAT_HOI; dist3; DIST_SYM]` 
  &0 <= ups_x (dist3 x y pow 2) (dist3 x z pow 2) (dist3 y z pow 2) `;;



let UPS_X_EQ_ZERO_COND = 
prove(` ! v1 v2 (v3: real^3). (collinear {v1, v2, v3} <=>
            ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2)
            (dist (v2,v3) pow 2) =
            &0) `,

MP_TAC FHFMKIY THEN MESON_TAC[]);;




let NORM_POW2_SUM2 = 
prove(` norm ( a % x + b % y ) pow 2 =
  a pow 2 * norm x pow 2 + &2 * ( a * b ) * ( x dot y ) + 
  b pow 2 * norm y pow 2 `,
 REWRITE_TAC[vector_norm] THEN 
SIMP_TAC[DOT_POS_LE; SQRT_WORKS] THEN CONV_TAC VECTOR_ARITH);;




let X_DOT_X_EQ = 
prove( ` x dot x = norm x pow 2 `,




let SUB_DIST_POW2_INTERPRETE = 
prove(`! x y (v:real^N) c. 
dist(x,v) pow 2 - dist(y,v) pow 2 = c <=>
( &2 % v  - ( x + y )) dot ( y - x ) = c `,

SIMP_TAC[DIST_POW2_DOT; DOT_SUB_ADD; VECTOR_ARITH`
 (x - v - (y - v)) dot (x - v + y - v) =  (&2 % v - (x + y)) dot (y - x) `]);;

let D3_SYM = MESON[trg_dist3_sym]` ! x y. dist3 x y = dist3 y x `;;


let REAL_DIV_LZERO = 
prove(
  `!x. &0 / x = &0`,

  REPEAT GEN_TAC THEN REWRITE_TAC[real_div; REAL_MUL_LZERO]);;


let SDIHJZK = 
prove(`! (v1:real^3) v2 v3 (a01: real) a02 a03.
         ~collinear {v1, v2, v3} /\
         (let x12 = dist3 v1 v2 pow 2 in
          let x13 = dist3 v1 v3 pow 2 in
          let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
         ==> (?!v0. a01 = dist3 v0 v1 pow 2 /\
                    a02 = dist3 v0 v2 pow 2 /\
                    a03 = dist3 v0 v3 pow 2 /\
                    (let x12 = dist3 v1 v2 pow 2 in
                     let x13 = dist3 v1 v3 pow 2 in
                     let x23 = dist3 v2 v3 pow 2 in
                     let vv = ups_x x12 x13 x23 in
                     let t1 = delta_x12 a01 a02 a03 x12 x13 x23 / vv in
                     let t2 = delta_x13 a01 a02 a03 x12 x13 x23 / vv in
                     let t3 = delta_x14 a01 a02 a03 x12 x13 x23 / vv in
                     v0 = t1 % v1 + t2 % v2 + t3 % v3 /\ t1 + t2 + t3 = &1 ))`,
 
REPEAT GEN_TAC THEN 
LET_TR THEN 
STRIP_TAC THEN 
REWRITE_TAC[EXISTS_UNIQUE] THEN 
EXISTS_TAC ` delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
       (dist3 v2 v3 pow 2) /
       ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
       v1 +
       delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
       (dist3 v2 v3 pow 2) /
       ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
       v2 +
       delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
       (dist3 v2 v3 pow 2) /
       ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
       v3 ` THEN 
UNDISCH_TAC `~collinear {(v1:real^3), v2, v3}` THEN 
MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN 
REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN 
REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `; dist3] THEN 
NHANH (MESON[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `]`
   (!(x:real^3) y z.
        &0 <= ups_x (dist (x,y) pow 2) (dist (x,z) pow 2) (dist (y,z) pow 2)) /\
   ~(ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0)
    ==> &0 < ups_x (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) `) THEN 
REWRITE_TAC[ GSYM dist3] THEN 
STRIP_TAC THEN 
CONJ_TAC THENL [

UNDISCH_TAC ` &0 < ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2)` THEN 
ABBREV_TAC ` a12 = dist3 v1 v2 pow 2 ` THEN ABBREV_TAC ` a13 = dist3 v1 v3 pow 2 ` THEN 
ABBREV_TAC ` a23 = dist3 v2 v3 pow 2 ` THEN SIMP_TAC[TO_UYCH] THEN 
REWRITE_TAC[MESON[dist3; dist] ` aa = dist3 a b pow 2 <=> aa = norm ( a- b ) pow 2 `] THEN 
ONCE_REWRITE_TAC[VECTOR_ARITH ` a - b = a - &1 % b `] THEN 
NHANH (GSYM TO_UYCH) THEN SIMP_TAC[] THEN 
SIMP_TAC[VECTOR_ARITH ` (a % v1 + b % v2 + c % v3) - (a + b + c) % v2 =
     (b % v2 + c % v3 + a % v1) - (b + c + a) % v2 /\
  (a % v1 + b % v2 + c % v3) - (a + b + c) % v3 = 
  (c % v3 + a % v1 + b % v2 ) - ( c + a + b ) % v3 `] THEN 
REWRITE_TAC[VECTOR_ARITH` ( a % v1 + b % v2 + c % v3)  - 
  ( a + b + c ) % v1 = b % ( v2 - v1 ) + c % ( v3 - v1 ) `] THEN 
REWRITE_TAC[NORM_POW2_SUM2 ; REAL_ARITH ` &2 * ( a * b ) * c = a * b * &2 * c `] THEN 
REWRITE_TAC[VECTOR_ARITH ` &2 * ( x dot y ) = x dot x + y dot y - ( x - y ) dot ( x - y ) `] THEN 
REWRITE_TAC[VECTOR_ARITH` v1 - v3 - (v2 - v3) = (v1:real^3) - v2 `] THEN 
REWRITE_TAC[X_DOT_X_EQ; GSYM dist; GSYM dist3] THEN 
SIMP_TAC[D3_SYM] THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN 
UNDISCH_TAC ` ~(ups_x a12 a13 a23 = &0)` THEN NHANH NOT_UPS_X_ZERO_IMP_SMT  THEN 
ASM_SIMP_TAC[REAL_DIV_LZERO; REAL_SUB_RZERO];
MESON_TAC[]]);;




let HALF_OF_LE16 = 
prove(` ! (v1:real^3) v2 v3 (a01: real) a02 a03.
         ~collinear {v1, v2, v3} /\
         (let x12 = dist3 v1 v2 pow 2 in
          let x13 = dist3 v1 v3 pow 2 in
          let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
==> ?v0. (v0 IN aff {v1, v2, v3} /\
       a01 = dist3 v0 v1 pow 2 /\
       a02 = dist3 v0 v2 pow 2 /\
       a03 = dist3 v0 v3 pow 2 /\
       (let x12 = dist3 v1 v2 pow 2 in
        let x13 = dist3 v1 v3 pow 2 in
        let x23 = dist3 v2 v3 pow 2 in
        let vv = ups_x x12 x13 x23 in
        let t1 = delta_x12 a01 a02 a03 x12 x13 x23 / vv in
        let t2 = delta_x13 a01 a02 a03 x12 x13 x23 / vv in
        let t3 = delta_x14 a01 a02 a03 x12 x13 x23 / vv in
        v0 = t1 % v1 + t2 % v2 + t3 % v3)) `,

REPEAT GEN_TAC THEN LET_TR THEN STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN 
EXISTS_TAC ` delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
       (dist3 v2 v3 pow 2) /
       ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
       v1 +
       delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
       (dist3 v2 v3 pow 2) /
       ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
       v2 +
       delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
       (dist3 v2 v3 pow 2) /
       ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
       v3 ` THEN 
UNDISCH_TAC `~collinear {(v1:real^3), v2, v3}` THEN 
MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN 
REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN 
REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `; dist3] THEN 
NHANH (MESON[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `]`
   (!(x:real^3) y z.
        &0 <= ups_x (dist (x,y) pow 2) (dist (x,z) pow 2) (dist (y,z) pow 2)) /\
   ~(ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0)
    ==> &0 < ups_x (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) `) THEN 
REWRITE_TAC[ GSYM dist3] THEN 
STRIP_TAC THEN 
UNDISCH_TAC ` &0 < ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2)` THEN 
ABBREV_TAC ` a12 = dist3 v1 v2 pow 2 ` THEN ABBREV_TAC ` a13 = dist3 v1 v3 pow 2 ` THEN 
ABBREV_TAC ` a23 = dist3 v2 v3 pow 2 ` THEN SIMP_TAC[TO_UYCH] THEN 
REWRITE_TAC[MESON[dist3; dist] ` aa = dist3 a b pow 2 <=> aa = norm ( a- b ) pow 2 `] THEN 
ONCE_REWRITE_TAC[VECTOR_ARITH ` a - b = a - &1 % b `] THEN 
NHANH (GSYM TO_UYCH) THEN SIMP_TAC[] THEN 
SIMP_TAC[VECTOR_ARITH ` (a % v1 + b % v2 + c % v3) - (a + b + c) % v2 =
     (b % v2 + c % v3 + a % v1) - (b + c + a) % v2 /\
  (a % v1 + b % v2 + c % v3) - (a + b + c) % v3 = 
  (c % v3 + a % v1 + b % v2 ) - ( c + a + b ) % v3 `] THEN 
REWRITE_TAC[VECTOR_ARITH` ( a % v1 + b % v2 + c % v3)  - 
  ( a + b + c ) % v1 = b % ( v2 - v1 ) + c % ( v3 - v1 ) `] THEN 
REWRITE_TAC[NORM_POW2_SUM2 ; REAL_ARITH ` &2 * ( a * b ) * c = a * b * &2 * c `] THEN 
REWRITE_TAC[VECTOR_ARITH ` &2 * ( x dot y ) = x dot x + y dot y - ( x - y ) dot ( x - y ) `] THEN 
REWRITE_TAC[VECTOR_ARITH` v1 - v3 - (v2 - v3) = (v1:real^3) - v2 `] THEN 
REWRITE_TAC[X_DOT_X_EQ; GSYM dist; GSYM dist3] THEN 
SIMP_TAC[D3_SYM] THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN 
UNDISCH_TAC ` ~(ups_x a12 a13 a23 = &0)` THEN NHANH NOT_UPS_X_ZERO_IMP_SMT  THEN 
ASM_SIMP_TAC[REAL_DIV_LZERO; REAL_SUB_RZERO] THEN 
REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN ASM_MESON_TAC[]);;





let EQ_SUB_DIST_POW2_IMP_IDENTIFIED = 
prove(` ! v1 v2 v3 (u:real^N) w. 
{u,w} SUBSET affine hull {v1,v2,v3} /\
dist (u,v2) pow 2 - dist (u,v1) pow 2 = dist (w,v2) pow 2 - dist (w,v1) pow 2 /\
dist (u,v3) pow 2 - dist (u,v1) pow 2 = dist (w,v3) pow 2 - dist (w,v1) pow 2 ==>
w = u `,
 
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN 
SIMP_TAC[SUB_DIST_POW2_INTERPRETE ] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 
SIMP_TAC[SUB_DIST_POW2_INTERPRETE ] THEN 
ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN 
SIMP_TAC[GSYM DOT_LSUB] THEN 
SIMP_TAC[GSYM DOT_LSUB; VECTOR_ARITH` a - b - ( aa - b ) =
  (a:real^N) - aa `; GSYM VECTOR_SUB_LDISTRIB; AFFINE_HULL_3;
  SET2_SU_EX; IN_ELIM_THM] THEN STRIP_TAC THEN 
REPEAT (FIRST_X_ASSUM MP_TAC ) THEN 
REWRITE_TAC[MESON[]` a ==> b ==> c <=> b /\ a ==> c `] THEN 
NHANH (MESON[]` a = (aa:real^N) /\ la /\ b = bb /\ lb ==>
  a - b = aa - bb `) THEN 
REWRITE_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN PHA THEN 
STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN UNDISCH_TAC`u' = &1 - (v + w')` THEN 
UNDISCH_TAC`u'' = &1 - (v' + w'')` THEN SIMP_TAC[] THEN 
SIMP_TAC[VECTOR_ARITH` ((&1 - (v' + w'')) % v1 + v' % v2 + w'' % v3) -
     ((&1 - (v + w')) % v1 + v % v2 + w' % v3) =
  ( v - v' ) % ( v1 - v2 ) + (w' - w'' ) % ( v1 - v3 ) `] THEN 
REPEAT STRIP_TAC THEN 
ONCE_REWRITE_TAC[VECTOR_ARITH ` a = b <=> b - a = vec 0` ] THEN 
REWRITE_TAC[GSYM DOT_EQ_0] THEN FIRST_X_ASSUM MP_TAC THEN 
REWRITE_TAC[MESON[]` a = b ==> a dot a = &0 <=> a = b ==>
  a dot b = &0 `] THEN 
REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_ARITH ` a * ( b dot c ) + aa * bb = &0
  <=> a * &2 * ( b dot c ) + aa * &2 * bb = &0 `] THEN 
ONCE_REWRITE_TAC[GSYM DOT_LMUL] THEN 
ABBREV_TAC ` as = &2 % ((w:real^N) - u) dot (v1 - v2)` THEN 
ABBREV_TAC ` bs = &2 % ((w:real^N) - u) dot (v1 - v3)` THEN 
DISCH_TAC THEN ASM_SIMP_TAC[] THEN REAL_ARITH_TAC);;

(* lemma 16 SDIHJZK *)


let SDIHJZK = 
prove(`! (v1:real^3) v2 v3 (a01: real) a02 a03.
         ~collinear {v1, v2, v3} /\
         (let x12 = dist3 v1 v2 pow 2 in
          let x13 = dist3 v1 v3 pow 2 in
          let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
         ==> (?v0. v0 IN aff {v1,v2,v3} /\
                    a01 = dist3 v0 v1 pow 2 /\
                    a02 = dist3 v0 v2 pow 2 /\
                    a03 = dist3 v0 v3 pow 2 /\ 
                   (! vv0. vv0 IN aff {v1,v2,v3} /\
                    a01 = dist3 vv0 v1 pow 2 /\
                    a02 = dist3 vv0 v2 pow 2 /\
                    a03 = dist3 vv0 v3 pow 2 ==> vv0 = v0 ) /\
                    (let x12 = dist3 v1 v2 pow 2 in
                     let x13 = dist3 v1 v3 pow 2 in
                     let x23 = dist3 v2 v3 pow 2 in
                     let vv = ups_x x12 x13 x23 in
                     let t1 = delta_x12 a01 a02 a03 x12 x13 x23  / vv in
                     let t2 = delta_x13 a01 a02 a03 x12 x13 x23  / vv in
                     let t3 = delta_x14 a01 a02 a03 x12 x13 x23  / vv in
                     v0 = t1 % v1 + t2 % v2 + t3 % v3))`,

REPEAT GEN_TAC THEN NHANH (SPEC_ALL HALF_OF_LE16  ) THEN STRIP_TAC THEN 
EXISTS_TAC `v0:real^3` THEN ASM_SIMP_TAC[] THEN 
GEN_TAC THEN UNDISCH_TAC ` (v0:real^3) IN aff {v1, v2, v3}` THEN 
ONCE_REWRITE_TAC[REAL_ARITH ` a1 = b1 /\ a2 = b2 /\ a3 = b3 <=>
  a2 - a1 = b2 - b1 /\ a3 - a1 = b3 - b1 /\ a1 = b1 `] THEN 
REWRITE_TAC[aff; SET2_SU_EX] THEN REWRITE_TAC[dist3] THEN 
PHA THEN MESON_TAC[SET2_SU_EX; EQ_SUB_DIST_POW2_IMP_IDENTIFIED]);;




let SDIHJZK_INTERPRETE = 
prove(`!(v1:real^3) v2 v3 a01 a02 a03.
     ~collinear {v1, v2, v3} /\
     delta a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) =
     &0
     ==> (?v0. v0 IN aff {v1, v2, v3} /\
               a01 = dist3 v0 v1 pow 2 /\
               a02 = dist3 v0 v2 pow 2 /\
               a03 = dist3 v0 v3 pow 2 /\
               (!vv0. vv0 IN aff {v1, v2, v3} /\
                      a01 = dist3 vv0 v1 pow 2 /\
                      a02 = dist3 vv0 v2 pow 2 /\
                      a03 = dist3 vv0 v3 pow 2
                      ==> vv0 = v0) /\
               v0 =
               delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
               (dist3 v2 v3 pow 2) /
               ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
               v1 +
               delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
               (dist3 v2 v3 pow 2) /
               ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
               v2 +
               delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
               (dist3 v2 v3 pow 2) /
               ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
               v3)`,
 MP_TAC SDIHJZK THEN LET_TR THEN SIMP_TAC[]);;




let DELTA_RRR_INTERPRETE = 
prove(` delta r r r a b c = -- a * b * c + r * ups_x a b c `,

REWRITE_TAC[delta; ups_x] THEN REAL_ARITH_TAC);;



let NOT_UPS_X_EQ_0_IMP = 
prove(` ~( ups_x a b c = &0 ) 
 ==> delta ( ( a * b * c ) / ups_x a b c ) ( ( a * b * c ) / ups_x a b c ) 
  ( ( a * b * c ) / ups_x a b c ) a b c = &0 `,

REWRITE_TAC[DELTA_RRR_INTERPRETE ] THEN CONV_TAC REAL_FIELD);;




let COL_EQ_UPS_0 = GEN_ALL (MESON[FHFMKIY]` collinear {(v1:real^3), v2, v3} <=>
 ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0`);;


(* CDEUSDF POST ZERO_LE_UPS_X *)


let REAL_LE_SQUARE_POW =
MESON[REAL_POW_2; REAL_LE_SQUARE]`! x. &0 <= x pow 2 `;;



let PROVE_EXISTS_RADV = 
prove(`!(va:real^3) vb vc.
     ~collinear {va, vb, vc}
     ==> (?p. p IN affine hull {va, vb, vc} /\
              (?c. ( !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
                 (!p'. p' IN affine hull {va, vb, vc} /\
                    ( !w. w IN {va, vb, vc} ==> c = dist (p',w))
                    ==> p = p'))) `,

REWRITE_TAC[COL_EQ_UPS_0] THEN 
NHANH (NOT_UPS_X_EQ_0_IMP ) THEN 
REWRITE_TAC[GSYM COL_EQ_UPS_0] THEN 
REWRITE_TAC[GSYM dist3] THEN 
NHANH (SPEC_ALL SDIHJZK_INTERPRETE) THEN 
REWRITE_TAC[EXISTS_UNIQUE] THEN 
REPEAT STRIP_TAC THEN 
ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
      ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2)  ` THEN 
EXISTS_TAC ` v0 :real^3` THEN 
UNDISCH_TAC ` (v0:real^3) IN aff {va, vb, vc}` THEN 
SIMP_TAC[aff; SET_RULE ` (! x. x IN {a,b,c} ==> P x ) <=>
  P a /\ P b /\ P c `] THEN 
DISCH_TAC THEN EXISTS_TAC ` sqrt ( r ) ` THEN 
UNDISCH_TAC ` (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
      ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) = r` THEN 
NHANH (MESON[REAL_LE_SQUARE_POW; REAL_LE_DIV; REAL_LE_MUL; 
  ZERO_LE_UPS_X ]` (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) =
 r ==> &0 <= r `) THEN 
SIMP_TAC[SQRT_WORKS; EQ_POW2_COND; D3_POS_LE] THEN 
ASM_MESON_TAC[aff]);;





let COND_FOR_CIRCUMCENTER_PROPERTIESS = 
prove(`~collinear {(v1:real^3), v2, v3}
 ==> circumcenter {v1, v2, v3} IN affine hull {v1, v2, v3} /\
     (?c. !v. v IN {v1, v2, v3} ==> c = dist (circumcenter {v1, v2, v3}, v))`,

NHANH (MESON[PROVE_EXISTS_RADV]`~collinear {(va:real^3), vb, vc}
         ==> (?p. p IN affine hull {va, vb, vc} /\
                  (?c. (!w. w IN {va, vb, vc} ==> c = dist (p,w)))) `) THEN 
REWRITE_TAC[IN; circumcenter] THEN MESON_TAC[EXISTS_THM]);;



let DELTA_X14_RRR = 
prove(` delta_x14 r r r a b c = a * ( b + c - a ) `,

REWRITE_TAC[delta_x14] THEN REAL_ARITH_TAC);;



let DELTA_X1I_RRR = 
prove(` delta_x12 r r r a b c = c * ( b + a - c ) /\
  delta_x13 r r r a b c = b * ( c + a  - b ) /\
  delta_x14 r r r a b c = a * (c + b - a) `,

REWRITE_TAC[delta_x12; delta_x13; delta_x14] THEN REAL_ARITH_TAC);;






let PRE_RADV_COND = 
prove(` ~ collinear {va,vb,vc} ==>
(? c. ! w. {va,vb,(vc:real^3)} w ==> c = dist(circumcenter {va,vb,vc} , w )) `,

NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS ) THEN MESON_TAC[IN]);;



let NOT_COL_IMP_RADV_PROPERTIY = 
prove(` ~collinear {(va:real^3), vb, vc}
 ==>  ( ! w. {va, vb, vc} w ==> 
  radV {va, vb, vc} = dist (circumcenter {va, vb, vc},w)) `,

NHANH (PRE_RADV_COND ) THEN SIMP_TAC[EXISTS_THM; radV]);;





let CIRCUMCENTER_FORMULAR2 = 
prove(`! (va:real^3) vb vc a b c.
     a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
     ==> 
         (let al_a =
              (a pow 2 * (b pow 2 + c pow 2 - a pow 2)) /
              (ups_x (a pow 2) (b pow 2) (c pow 2)) in
          let al_b =
              (b pow 2 * (a pow 2 + c pow 2 - b pow 2)) /
              (ups_x (a pow 2) (b pow 2) (c pow 2)) in
          let al_c =
              (c pow 2 * (a pow 2 + b pow 2 - c pow 2)) /
              (ups_x (a pow 2) (b pow 2) (c pow 2)) in
          al_a % va + al_b % vb + al_c % vc = circumcenter {va, vb, vc})`,

REWRITE_TAC[COL_EQ_UPS_0] THEN 
NHANH (NOT_UPS_X_EQ_0_IMP) THEN 
REWRITE_TAC[GSYM COL_EQ_UPS_0; GSYM dist3] THEN 
NHANH (SPEC_ALL SDIHJZK_INTERPRETE ) THEN 
REPEAT STRIP_TAC THEN 
ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
           ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) ` THEN 
UNDISCH_TAC ` v0 =
      delta_x12 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
      ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
      va +
      delta_x13 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
      ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
      vb +
      delta_x14 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
      ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
      vc`  THEN 
LET_TR THEN 
UNDISCH_TAC ` a = dist3 vb vc ` THEN 
UNDISCH_TAC ` b = dist3 va vc ` THEN 
UNDISCH_TAC ` c = dist3 va vb ` THEN 
SIMP_TAC[DELTA_X1I_RRR] THEN 
SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `] THEN 
ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 
SIMP_TAC[] THEN 
REPEAT STRIP_TAC THEN 
UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc} ` THEN 
NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS) THEN 
REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
  <=> P a /\ P b /\ P c `] THEN 
REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
  <=> P a /\ P b /\ P c `; MESON[]` (? cc. cc = a /\ cc = b /\ cc = c)
  <=> a = b /\ a = c  `] THEN 
UNDISCH_TAC ` v0 IN aff {va, vb, (vc:real^3)}` THEN 
REWRITE_TAC[aff; SET_RULE ` a IN s ==> b /\ aa IN s /\ l ==>
  ll <=> b ==>  {a,aa} SUBSET s /\ l ==> ll `] THEN 
DISCH_TAC THEN 
UNDISCH_TAC` r = dist3 v0 va pow 2 ` THEN 
UNDISCH_TAC` r = dist3 v0 vb pow 2 ` THEN 
UNDISCH_TAC` r = dist3 v0 vc pow 2 ` THEN 
REWRITE_TAC[MESON[]` r = a1 ==> r = a2 ==> r = a3 ==> l ==> ll <=>
  r = a1 /\ l /\ a2 = a3 /\ a1 = a3 ==> ll `;dist3] THEN 
ONCE_REWRITE_TAC[MESON[]` dist(a,b) = s <=> s = dist(a,b) `] THEN 
SIMP_TAC[DIST_POS_LE; EQ_POW2_COND] THEN 
ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN 
MESON_TAC[EQ_SUB_DIST_POW2_IMP_IDENTIFIED ]);;


let REAL_LE_POW_2 = 
prove(` ! x. &0 <= x pow 2 `,

REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;




let NOT_COLL_IMP_RADV_FORMULAR = 
prove(`! (va:real^3) vb vc a b c.
     a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
     ==>  radV {va, vb, vc} = eta_y a b c`,

REWRITE_TAC[COL_EQ_UPS_0] THEN 
NHANH (NOT_UPS_X_EQ_0_IMP) THEN 
REWRITE_TAC[GSYM COL_EQ_UPS_0; GSYM dist3] THEN 
NHANH (SPEC_ALL SDIHJZK_INTERPRETE ) THEN 
REPEAT STRIP_TAC THEN 
ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
           ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) ` THEN 
LET_TR THEN 
UNDISCH_TAC ` a = dist3 vb vc ` THEN 
UNDISCH_TAC ` b = dist3 va vc ` THEN 
UNDISCH_TAC ` c = dist3 va vb ` THEN 
SIMP_TAC[DELTA_X1I_RRR] THEN 
SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `] THEN 
ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 
SIMP_TAC[] THEN 
REPEAT STRIP_TAC THEN 
UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc} ` THEN 
NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS) THEN 
REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
  <=> P a /\ P b /\ P c `] THEN 
REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
  <=> P a /\ P b /\ P c `; MESON[]` (? cc. cc = a /\ cc = b /\ cc = c)
  <=> a = b /\ a = c  `] THEN 
UNDISCH_TAC ` v0 IN aff {va, vb, (vc:real^3)}` THEN 
REWRITE_TAC[aff; SET_RULE ` a IN s ==> b /\ aa IN s /\ l ==>
  ll <=> b ==>  {a,aa} SUBSET s /\ l ==> ll `] THEN 
DISCH_TAC THEN 
UNDISCH_TAC` r = dist3 v0 va pow 2 ` THEN 
UNDISCH_TAC` r = dist3 v0 vb pow 2 ` THEN 
UNDISCH_TAC` r = dist3 v0 vc pow 2 ` THEN 
REWRITE_TAC[MESON[]` r = a1 ==> r = a2 ==> r = a3 ==> l ==> ll <=>
  r = a1 /\ l /\ a2 = a3 /\ a1 = a3 ==> ll `;dist3] THEN 
ONCE_REWRITE_TAC[MESON[]` dist(a,b) = s <=> s = dist(a,b) `] THEN 
SIMP_TAC[DIST_POS_LE; EQ_POW2_COND] THEN 
ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN 
REWRITE_TAC[MESON[]` ( a /\ a1 = &0 /\ a2 = &0 ) /\ b1 = &0 /\ b2 = &0 <=>
  b1 = &0 /\ b2 = &0 /\ a /\ b1 = a1 /\ b2 = a2 `] THEN 
NHANH (SPEC_ALL EQ_SUB_DIST_POW2_IMP_IDENTIFIED ) THEN 
STRIP_TAC THEN 
UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc}` THEN 
NHANH (NOT_COL_IMP_RADV_PROPERTIY ) THEN 
FIRST_X_ASSUM MP_TAC THEN 
SIMP_TAC[] THEN 
SIMP_TAC[SET_RULE ` (!w. {va, vb, vc} w ==> P w ) <=>
  P va /\ P vb /\ P vc `] THEN 
REPEAT STRIP_TAC THEN 
EXPAND_TAC "a" THEN 
EXPAND_TAC "b" THEN 
EXPAND_TAC "c" THEN 
UNDISCH_TAC ` r - dist ((v0:real^3),vc) pow 2 = &0 ` THEN 
SIMP_TAC[REAL_ARITH` a - b = &0 <=> b = a `] THEN 
EXPAND_TAC "r" THEN 
REWRITE_TAC[eta_y; eta_x] THEN 
LET_TR THEN 
MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN 
SIMP_TAC[GSYM REAL_POW_2] THEN 
SIMP_TAC[REAL_ARITH` a * b * c = c * b * a `;
  UPS_X_SYM; dist3] THEN 
MP_TAC (MESON[dist3; DIST_POS_LE]` &0 <= dist3 v0 vc `) THEN 
MP_TAC (MESON[REAL_LE_DIV; REAL_LE_MUL_EQ; REAL_LE_POW_2;REAL_LE_MUL; ZERO_LE_UPS_X;
SQRT_WORKS]` &0 <= ((dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
      ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2)) /\
  &0 <= sqrt ((dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
      ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2)) `) THEN 
REWRITE_TAC[MESON[]` a ==> b ==> c <=> b /\ a ==> c `] THEN 
MATCH_MP_TAC (MESON[]` (a1 /\ a3 ==> l) ==> a1 /\a2 /\a3 ==> l`) THEN 
SIMP_TAC[dist3; EQ_POW2_COND; SQRT_WORKS]);;



let CDEUSDF = 
prove(`!(va:real^3) vb vc a b c.
     a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
     ==> (?p. p IN affine hull {va, vb, vc} /\
              (?c. ( !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
              (!p'. p' IN affine hull {va, vb, vc} /\
                    ( !w. w IN {va, vb, vc} ==> c = dist (p',w))
                    ==> p = p'))) /\
         (let al_a =
              (a pow 2 * (b pow 2 + c pow 2 - a pow 2)) /
              (ups_x (a pow 2) (b pow 2) (c pow 2)) in
          let al_b =
              (b pow 2 * (a pow 2 + c pow 2 - b pow 2)) /
              (ups_x (a pow 2) (b pow 2) (c pow 2)) in
          let al_c =
              (c pow 2 * (a pow 2 + b pow 2 - c pow 2)) /
              (ups_x (a pow 2) (b pow 2) (c pow 2)) in
          al_a % va + al_b % vb + al_c % vc = circumcenter {va, vb, vc}) /\
         radV {va, vb, vc} = eta_y a b c`,

let LEMMA17 = CDEUSDF;;


let DIST_EQ_IS_UNIQUE = 
prove(` {u, w} SUBSET affine hull {v1, v2, v3} /\
  dist (u,v2) = dist (u,v1) /\ dist (u,v3) = dist (u,v1) /\
  dist (w,v2) = dist (w,v1) /\ dist (w,v3) = dist (w,v1) ==>
  u = w `,

SIMP_TAC[EQ_POW2_COND; DIST_POS_LE] THEN ONCE_REWRITE_TAC[REAL_ARITH`
 a = b <=> a - b = &0 `] THEN MESON_TAC[EQ_SUB_DIST_POW2_IMP_IDENTIFIED]);;



let NEVER_USED_AGAIN = 
prove(` p IN affine hull {va, vb, vc} /\ c = dist (p,va) 
/\ c = dist (p,vb) /\ c = dist (p,vc)  ==>
  (! p'.  p' IN affine hull {va, vb, vc} /\
           dist (p',vb) = dist (p',va) /\
           dist (p',vc) = dist (p',va) <=>
  p' IN affine hull {va, vb, vc} /\
  c = dist (p',va) /\
  c = dist (p',vb) /\
  c = dist (p',vc) )`,

MESON_TAC[DIST_EQ_IS_UNIQUE; SET2_SU_EX]);;




let TRUONG_WELL = 
prove(`! (va:real^3) vb vc. ~collinear {va, vb, vc}
     ==> (?p. p IN affine hull {va, vb, vc} /\
              (?c. !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
              (!p'. p' IN affine hull {va, vb, vc} /\
                    (?c. !w. w IN {va, vb, vc} ==> c = dist (p',w))
                    ==> p = p'))`,

NHANH (SPEC_ALL PROVE_EXISTS_RADV) THEN REPEAT STRIP_TAC THEN EXISTS_TAC `p:real^3`
THEN CONJ_TAC THENL [ASM_SIMP_TAC[]; CONJ_TAC] THENL [ASM_MESON_TAC[]; 
REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN 
REWRITE_TAC[SET_RULE` (!a. a IN {x,y,z} ==> p a)
  <=> p x /\ p y /\ p z `] THEN 
REWRITE_TAC[MESON[]` (?c. c = a /\ c = b /\ c = cc ) <=>
 b = a /\ cc = a `]] THEN 
REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\b ==> c `] THEN 
  PHA THEN MESON_TAC[NEVER_USED_AGAIN ]);;




let NGAY_MONG6 = MESON[TRUONG_WELL] `! va vb (vc:real^3). 
         ~collinear {va, vb, vc} ==> (?p. p IN affine hull {va, vb, vc} /\
                  (?c. !w. w IN {va, vb, vc} ==> c = dist (p,w))  ) `;;



let CIRCUMCENTER_PROPTIES = 
prove(`!va vb (vc:real^3).
     ~collinear {va, vb, vc}
     ==> circumcenter {va, vb, vc} IN affine hull {va, vb, vc} /\
(?c. !w. w IN {va, vb, vc}
                  ==> c = dist (circumcenter {va, vb, vc},w))`,

NHANH (SPEC_ALL NGAY_MONG6) THEN REWRITE_TAC[IN; 
circumcenter; EXISTS_THM] THEN SIMP_TAC[]);;







let SIMP_DOT_ALEM = 
prove(  `&0 < (b - a) dot x <=> x dot (a - b) < &0`,

SIMP_TAC[DOT_SYM] THEN 
REWRITE_TAC[ REAL_ARITH ` a < &0 <=> &0 < -- a `; GSYM DOT_RNEG] THEN 
REWRITE_TAC[VECTOR_ARITH ` -- ((a:real^N) - b) = b - a `]);;





let MONG7_ROI = 
prove(` ! p a (b:real^A). dist (p,a) = dist (p,b) <=> 
  (p - &1 / &2 % ( a + b )) dot ( a - b)  = &0 `,

REWRITE_TAC[ REAL_ARITH ` a = b <=> ~ ( a < b) /\ ~( b < a ) `; 
DIST_LT_HALF_PLANE] THEN 
REWRITE_TAC[VECTOR_ARITH` (p - &1 / &2 % (a + b)) dot (a - b)
  = &1 / &2 * ( (&2 % p - (a + b ) ) dot ( a- b ) )  `] THEN 
REWRITE_TAC[REAL_ARITH `( &1 / &2 * a < &0 <=> a < &0) /\ 
(&0 < &1 / &2 * a <=> &0 < a )`] THEN 
REWRITE_TAC[SIMP_DOT_ALEM] THEN 
SIMP_TAC[VECTOR_ARITH` (a - b) dot (c - d) = (b - a) dot (d - c)`; DOT_SYM; 
VECTOR_ADD_SYM] THEN MESON_TAC[]);;


let LEMMA26 = 
prove(`!v1 v2 (v3:real^3) p.
     ~collinear {v1, v2, v3} /\ p = circumcenter {v1, v2, v3}
     ==> (p - &1 / &2 % (v1 + v2)) dot (v1 - v2) = &0 /\
         (p - &1 / &2 % (v2 + v3)) dot (v2 - v3) = &0 /\
         (p - &1 / &2 % (v3 + v1)) dot (v3 - v1) = &0`,

NHANH (SPEC_ALL CIRCUMCENTER_PROPTIES) THEN 
NHANH (SET_RULE` (?c. !w. w IN {v1, v2, v3} ==> c = P w) ==> P v1 = P v2
  /\ P v2 = P v3 /\ P v3 = P v1 `) THEN 
SIMP_TAC[MONG7_ROI]);;

let POXDVXO = LEMMA26;;



let NOT_COLL_IMP_RADV_EQ_ETA_Y = MESON[prove(`!va vb vc a b c.
     a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
     ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`,
SIMP_TAC[CDEUSDF])]` 
  !va vb vc . ~collinear {va, vb, vc}
     ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`;;


let COLLINEAR2 = 
prove(` ! x (y:real^N). collinear {x,y} `,

   REPEAT GEN_TAC THEN REWRITE_TAC[collinear] THEN
   EXISTS_TAC ` x -(y: real^N)` THEN
   ASM_SIMP_TAC[SET_RULE` a = b ==> {a,b,c} = {a,c} `] THEN
   REWRITE_TAC[IN_SET2] THEN
   REPEAT GEN_TAC THEN
   STRIP_TAC THENL
   [ASM_SIMP_TAC[] THEN EXISTS_TAC ` &0 ` THEN CONV_TAC VECTOR_ARITH;
   ASM_SIMP_TAC[] THEN EXISTS_TAC ` &1 ` THEN CONV_TAC VECTOR_ARITH;
   ASM_SIMP_TAC[] THEN EXISTS_TAC ` -- &1 ` THEN CONV_TAC VECTOR_ARITH;
   ASM_SIMP_TAC[] THEN EXISTS_TAC ` &0 ` THEN CONV_TAC VECTOR_ARITH]
		      );;


let TWO_EQ_IMP_COL3 = 
prove(` ! (x:real^N) y z .  x = y ==> collinear {x, y, z} `,

STRIP_TR THEN SIMP_TAC[SET_RULE` a = b ==> {a,b,c} = {a,c} `; COLLINEAR2]);;



let NOT_CO_IMP_DIST_POS = 
prove(`! x y z. ~ collinear {x,y,z} ==> &0 < dist (x,y) `,

NHANH (MESON[TWO_EQ_IMP_COL3]` ~collinear {x, y, z} ==> ~( x= y) `) THEN 
SIMP_TAC[DIST_POS_LT]);;



let NOT_COLL_IMP_POS_SUM = 
prove( ` !x y z.
     ~collinear {x, y, z} ==> &0 < ( dist3 x y + dist3 y z + dist3 z x) / &2 `,

NHANH (SPEC_ALL NOT_CO_IMP_DIST_POS) THEN 
NHANH (MESON[DIST_POS_LE]` ~collinear {x, y, z} ==>
  &0 <= dist (y,z) /\ &0 <= dist (z,x) `) THEN 
SIMP_TAC[dist3] THEN REAL_ARITH_TAC);;

let PER_SET2 = SET_RULE ` {a,b} = {b,a} `;;


let COLLINEAR_AS_IN_CONV2 = MESON[PER_SET2; COLLINERA_AS_IN_CONV2]`! x y (z:real^3). collinear {x, y, z} <=>
 x IN conv {y, z} \/ y IN conv {z, x} \/ z IN conv {x, y}`;;


let COLLINEAR_IMP_POS_UPS2 = 
prove(` ! x y (z:real^3). ~ collinear {x,y,z} ==>
  &0 < ups_x_pow2 ( dist3 x y ) ( dist3 y z ) ( dist3 z x ) `,

REWRITE_TAC[PRE_HER] THEN NHANH (SPEC_ALL NOT_COLL_IMP_POS_SUM ) THEN 
REWRITE_TAC[COLLINEAR_AS_IN_CONV2] THEN REWRITE_TAC[MID_COND] THEN 
REWRITE_TAC[LENGTH_EQ_EX] THEN REWRITE_TAC[DE_MORGAN_THM] THEN 
SIMP_TAC[dist3] THEN REPEAT GEN_TAC THEN SIMP_TAC[
prove(` &0 < a ==> ( &0 < &16 * a * b <=> &0 < b ) `,
REWRITE_TAC[REAL_ARITH ` &0 < &16 * a <=> &0 < a `] THEN 
REWRITE_TAC[REAL_LT_MUL_EQ])] THEN 
REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - a = ( b + c - a ) / &2 `] THEN 
REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - b = ( c + a - b ) / &2 `] THEN 
REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - c = ( a + b - c ) / &2 `] THEN 
REWRITE_TAC[REAL_ARITH ` a < b + c <=> &0 < ( b + c - a ) / &2 `] THEN 
SIMP_TAC[DIST_SYM] THEN SIMP_TAC[REAL_ARITH ` a + b - c = b + a - c `] THEN 
SIMP_TAC[REAL_LT_MUL]);;



let RADV_FORMULAR = MESON[CDEUSDF]` !(va:real^3) vb vc.
     ~collinear {va, vb, vc}
     ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`;;



let MUL3_SYM = REAL_ARITH ` ! a b c. a * b * c = b * a * c /\
  a * b * c = c * b * a `;;


let ETA_X_SYMM = 
prove(` ! a b c. eta_x a b c = eta_x b a c /\
 eta_x a b c = eta_x c b a `,
SIMP_TAC[eta_x; MUL3_SYM; UPS_X_SYM]);;


let ETA_Y_SYYM = 
prove(` ! x y z. eta_y x y z = eta_y y x z /\ 
eta_y x y z = eta_y z y x `,
 REWRITE_TAC[eta_y] THEN 
CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN MESON_TAC[ETA_X_SYMM]);;



let NOT_COL3_IMP_DIFF = MESON[PER_SET3; TWO_EQ_IMP_COL3]`!a b c. 
~collinear {a, b, c} ==> ~(a = b \/ a = c \/ b = c)`;;

let LET_TR = CONV_TAC (TOP_DEPTH_CONV let_CONV);;


let POW2_COND_LT = MESON[POW2_COND; REAL_ARITH ` &0 < a ==> &0 <= a `]` 
  !a b. &0 < a /\ &0 < b ==> (a <= b <=> a pow 2 <= b pow 2)`;;



let ETA_Y_2 = 
prove(` eta_y (&2) (&2) (&2)  = &2 / sqrt (&3) `,

REWRITE_TAC[eta_y; eta_x; ups_x] THEN 
LET_TR THEN 
REWRITE_TAC[REAL_ARITH ` ((&2 * &2) * (&2 * &2) * &2 * &2) /
  (--(&2 * &2) * &2 * &2 - (&2 * &2) * &2 * &2 - (&2 * &2) * &2 * &2 +
   &2 * (&2 * &2) * &2 * &2 +
   &2 * (&2 * &2) * &2 * &2 +
   &2 * (&2 * &2) * &2 * &2) = &4 / &3 `] THEN 
MP_TAC (MESON[REAL_LT_DIV; MESON[SQRT_POS_LT; REAL_ARITH` &0 < &3 `] ` 
&0 < sqrt (&3) `; REAL_ARITH ` &0 < &2 /\ &0 < &4 /\ &0 < &3 `] ` &0 < &4 / &3 
/\ &0 < &2 / sqrt (&3) `) THEN 
REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN 
SIMP_TAC[SQRT_POS_LT; POW2_COND_LT] THEN 
REWRITE_TAC[GSYM (REAL_ARITH` a = b <=> a <= b /\ b <= a `)] THEN 
SIMP_TAC[REAL_LT_IMP_LE; SQRT_POW_2] THEN 
REWRITE_TAC[REAL_FIELD` (a/ b) pow 2 = a pow 2 / ( b pow 2 ) `] THEN 
SIMP_TAC[REAL_ARITH ` &0 <= &3 `; SQRT_POW_2] THEN 
REAL_ARITH_TAC);;

let D3_POS_LE = MESON[dist3; DIST_POS_LE]` ! x y. &0 <= dist3 x y `;;


(* le 19. p 17 *)




let cayleytr = new_definition ` 
  cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = 
  &2 * x23 * x25 * x34 +
      &2 * x23 * x24 * x35 +
      -- &1 * x23 pow 2 * x45 +
      -- &2 * x15 * x23 * x34 +
      -- &2 * x15 * x23 * x24 +
      &2 * x15 * x23 pow 2 +
      -- &2 * x14 * x23 * x35 +
      -- &2 * x14 * x23 * x25 +
      &2 * x14 * x23 pow 2 +
      &4 * x14 * x15 * x23 +
      -- &2 * x13 * x25 * x34 +
      -- &2 * x13 * x24 * x35 +
      &4 * x13 * x24 * x25 +
      &2 * x13 * x23 * x45 +
      -- &2 * x13 * x23 * x25 +
      -- &2 * x13 * x23 * x24 +
      &2 * x13 * x15 * x34 +
      -- &2 * x13 * x15 * x24 +
      -- &2 * x13 * x15 * x23 +
      &2 * x13 * x14 * x35 +
      -- &2 * x13 * x14 * x25 +
      -- &2 * x13 * x14 * x23 +
      -- &1 * x13 pow 2 * x45 +
      &2 * x13 pow 2 * x25 +
      &2 * x13 pow 2 * x24 +
      &4 * x12 * x34 * x35 +
      -- &2 * x12 * x25 * x34 +
      -- &2 * x12 * x24 * x35 +
      &2 * x12 * x23 * x45 +
      -- &2 * x12 * x23 * x35 +
      -- &2 * x12 * x23 * x34 +
   -- &2 * x12 * x15 * x34 +
      &2 * x12 * x15 * x24 +
      -- &2 * x12 * x15 * x23 +
      -- &2 * x12 * x14 * x35 +
      &2 * x12 * x14 * x25 +
      -- &2 * x12 * x14 * x23 +
      &2 * x12 * x13 * x45 +
      -- &2 * x12 * x13 * x35 +
      -- &2 * x12 * x13 * x34 +
      -- &2 * x12 * x13 * x25 +
      -- &2 * x12 * x13 * x24 +
      &4 * x12 * x13 * x23 +
      -- &1 * x12 pow 2 * x45 +
      &2 * x12 pow 2 * x35 +
      &2 * x12 pow 2 * x34 `;;



let LTCTBAN = 
prove(` cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = 
ups_x x12 x13 x23 * x45 pow 2 + cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 ( &0 )
* x45 + cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 ( &0 ) `,

REWRITE_TAC[ups_x; cayleyR;cayleytr] THEN REAL_ARITH_TAC);;



(* ------------------------------------------------------------------------- *)
(* Flyspeck definitions we use.                                              *)
(* ------------------------------------------------------------------------- *)


let plane = new_definition
 `plane x = (?u v w. ~(collinear {u,v,w}) /\ (x = affine hull {u,v,w}))`;;

(* renamed from coplanar, because j. harrison changed the def. -thales *)


let coplanar_alt = new_definition `coplanar_alt S = (?x. plane x /\ S SUBSET x)`;;


(* renamed condA to condA, thales *)

(*
let condA = new_definition `condA (v1:real^3) v2 v3 v4 x12 x13 x14 x23 x24 x34 = 
  ( ~ ( v1 = v2 ) /\ coplanar_alt {v1,v2,v3,v4} /\
  ( dist ( v1, v2) pow 2 ) = x12 /\
  dist (v1,v3) pow 2 = x13 /\
  dist (v1,v4) pow 2 = x14 /\
  dist (v2,v3) pow 2 = x23 /\ dist (v2,v4) pow 2 = x24 )`;;
*)


let det_vec3 = new_definition ` det_vec3 (a:real^3) (b:real^3) (c:real^3) = 
  a$1 * b$2 * c$3 + b$1 * c$2 * a$3 + c$1 * a$2 * b$3 - 
  ( a$1 * c$2 * b$3 + b$1 * a$2 * c$3 + c$1 * b$2 * a$3 ) `;;


let COPLANAR_DET_EQ_0 = 
prove
 (`!v0 v1 (v2: real^3) v3.
       coplanar_alt {v0,v1,v2,v3} <=>
       det(vector[v1 - v0; v2 - v0; v3 - v0]) = &0`,

 REPEAT GEN_TAC THEN REWRITE_TAC[DET_EQ_0_RANK; RANK_ROW] THEN
 REWRITE_TAC[rows; row; LAMBDA_ETA] THEN
 ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
 REWRITE_TAC[GSYM numseg; DIMINDEX_3] THEN
 CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
 SIMP_TAC[IMAGE_CLAUSES; VECTOR_3] THEN EQ_TAC THENL
  [REWRITE_TAC[coplanar_alt; plane; LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
   MAP_EVERY X_GEN_TAC
    [`p:real^3->bool`; `a:real^3`; `b:real^3`; `c:real^3`] THEN
   DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
   FIRST_X_ASSUM SUBST1_TAC THEN
   W(MP_TAC o PART_MATCH lhand AFFINE_HULL_INSERT_SUBSET_SPAN o
       rand o lhand o goal_concl) THEN
   REWRITE_TAC[GSYM IMP_CONJ_ALT] THEN
   DISCH_THEN(MP_TAC o MATCH_MP SUBSET_TRANS) THEN
   DISCH_THEN(MP_TAC o ISPEC `\x:real^3. x - a` o MATCH_MP IMAGE_SUBSET) THEN
   ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
   REWRITE_TAC[IMAGE_CLAUSES; GSYM IMAGE_o; o_DEF; VECTOR_ADD_SUB; IMAGE_ID;
               SIMPLE_IMAGE] THEN
   REWRITE_TAC[INSERT_SUBSET] THEN STRIP_TAC THEN
   GEN_REWRITE_TAC LAND_CONV [GSYM DIM_SPAN] THEN MATCH_MP_TAC LET_TRANS THEN
   EXISTS_TAC `CARD {b - a:real^3,c - a}` THEN
   CONJ_TAC THENL
    [MATCH_MP_TAC SPAN_CARD_GE_DIM;
     SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC] THEN
   REWRITE_TAC[FINITE_INSERT; FINITE_RULES] THEN
   GEN_REWRITE_TAC RAND_CONV [GSYM SPAN_SPAN] THEN
   MATCH_MP_TAC SPAN_MONO THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
   MP_TAC(VECTOR_ARITH `!x y:real^3. x - y = (x - a) - (y - a)`) THEN
   DISCH_THEN(fun th -> REPEAT CONJ_TAC THEN
     GEN_REWRITE_TAC LAND_CONV [th]) THEN
   MATCH_MP_TAC SPAN_SUB THEN ASM_REWRITE_TAC[];

   DISCH_TAC THEN
   MP_TAC(ISPECL [`{v1 - v0,v2 - v0,v3 - v0}:real^3->bool`; `2`]
                 LOWDIM_EXPAND_BASIS) THEN
   ASM_REWRITE_TAC[ARITH_RULE `n <= 2 <=> n < 3`; DIMINDEX_3; ARITH] THEN
   DISCH_THEN(X_CHOOSE_THEN `t:real^3->bool`
    (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
   CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
   MAP_EVERY X_GEN_TAC [`a:real^3`; `b:real^3`] THEN
   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
   REWRITE_TAC[coplanar_alt; plane] THEN
   EXISTS_TAC `affine hull {v0,v0 + a,v0 + b}:real^3->bool` THEN
   CONJ_TAC THENL
    [MAP_EVERY EXISTS_TAC [`v0:real^3`; `v0 + a:real^3`; `v0 + b:real^3`] THEN
     REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA;
                 VECTOR_ARITH `--x = vec 0 <=> x = vec 0`;
                 VECTOR_ARITH `u - (u + a):real^3 = --a`;
                 VECTOR_ARITH `(u + b) - (u + a):real^3 = b - a`] THEN
     REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ;
       VECTOR_ARITH `b - a = c % -- a <=> (c - &1) % a + &1 % b = vec 0`] THEN
     ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
      [ASM_MESON_TAC[IN_INSERT; INDEPENDENT_NONZERO]; ALL_TAC] THEN
     DISCH_THEN(X_CHOOSE_TAC `u:real`) THEN
     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
     REWRITE_TAC[DEPENDENT_EXPLICIT] THEN
     MAP_EVERY EXISTS_TAC [`{a:real^3,b}`;
                           `\x:real^3. if x = a then u - &1 else &1`] THEN
     REWRITE_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL] THEN
     CONJ_TAC THENL
      [EXISTS_TAC `b:real^3` THEN ASM_REWRITE_TAC[IN_INSERT] THEN
       REAL_ARITH_TAC;
       ALL_TAC] THEN
     SIMP_TAC[VSUM_CLAUSES; FINITE_RULES] THEN
     ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID];
     ALL_TAC] THEN
   W(MP_TAC o PART_MATCH (lhs o rand) AFFINE_HULL_INSERT_SPAN o
     rand o goal_concl) THEN
   ANTS_TAC THENL
    [REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
     REWRITE_TAC[VECTOR_ARITH `u = u + a <=> a = vec 0`] THEN
     ASM_MESON_TAC[INDEPENDENT_NONZERO; IN_INSERT];
     ALL_TAC] THEN
   DISCH_THEN SUBST1_TAC THEN
   ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
   REWRITE_TAC[SIMPLE_IMAGE; IMAGE_CLAUSES; IMAGE_ID; VECTOR_ADD_SUB] THEN
   MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
    `IMAGE (\v:real^3. v0 + v) (span{v1 - v0, v2 - v0, v3 - v0})` THEN
   ASM_SIMP_TAC[IMAGE_SUBSET] THEN
   REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_IMAGE] THEN CONJ_TAC THENL
    [EXISTS_TAC `vec 0:real^3` THEN REWRITE_TAC[SPAN_0] THEN VECTOR_ARITH_TAC;
     REWRITE_TAC[VECTOR_ARITH `v1:real^N = v0 + x <=> x = v1 - v0`] THEN
     REWRITE_TAC[UNWIND_THM2] THEN REPEAT CONJ_TAC THEN
     MATCH_MP_TAC SPAN_SUPERSET THEN REWRITE_TAC[IN_INSERT]]]);;


(* renamed from COPLANAR Jan 2013, to avoid clash with hol-light/Multivariate/Flyspeck.ml thm *)


let COPLANAR_ALT = 
prove
 (`2 <= dimindex(:N)
  ==> !s:real^N->bool. coplanar_alt s <=> ?u v w. s SUBSET affine hull {u,v,w}`,

 DISCH_TAC THEN GEN_TAC THEN REWRITE_TAC[coplanar_alt; plane] THEN
 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 ONCE_REWRITE_TAC[MESON[]
  `(?x u v w. p x u v w) <=> (?u v w x. p x u v w)`] THEN
 REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM2] THEN
 EQ_TAC THENL [MESON_TAC[]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
 MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`; `w:real^N`] THEN DISCH_TAC THEN
 SUBGOAL_THEN
  `s SUBSET {u + x:real^N | x | x IN span {y - u | y IN {v,w}}}`
 MP_TAC THENL
  [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
    (REWRITE_RULE[IMP_CONJ] SUBSET_TRANS)) THEN
   REWRITE_TAC[AFFINE_HULL_INSERT_SUBSET_SPAN];
   ALL_TAC] THEN
 ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
 DISCH_THEN(MP_TAC o ISPEC `\x:real^N. x - u` o MATCH_MP IMAGE_SUBSET) THEN
 REWRITE_TAC[GSYM IMAGE_o; o_DEF; VECTOR_ADD_SUB; IMAGE_ID; SIMPLE_IMAGE] THEN
 REWRITE_TAC[IMAGE_CLAUSES] THEN
 MP_TAC(ISPECL [`{v - u:real^N,w - u}`; `2`] LOWDIM_EXPAND_BASIS) THEN
 ANTS_TAC THENL
  [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LE_TRANS THEN
   EXISTS_TAC `CARD{v - u:real^N,w - u}` THEN
   SIMP_TAC[DIM_LE_CARD; FINITE_INSERT; FINITE_RULES] THEN
   SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC;
   ALL_TAC] THEN
 DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool`
  (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
 CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
 UNDISCH_TAC `span {v - u, w - u} SUBSET span {a:real^N, b}` THEN
 REWRITE_TAC[GSYM IMP_CONJ_ALT] THEN
 DISCH_THEN(ASSUME_TAC o MATCH_MP SUBSET_TRANS) THEN
 MAP_EVERY EXISTS_TAC [`u:real^N`; `u + a:real^N`; `u + b:real^N`] THEN
 CONJ_TAC THENL
  [REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA;
               VECTOR_ARITH `--x = vec 0 <=> x = vec 0`;
               VECTOR_ARITH `u - (u + a):real^N = --a`;
               VECTOR_ARITH `(u + b) - (u + a):real^N = b - a`] THEN
   REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ;
     VECTOR_ARITH `b - a = c % -- a <=> (c - &1) % a + &1 % b = vec 0`] THEN
   ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
    [ASM_MESON_TAC[IN_INSERT; INDEPENDENT_NONZERO]; ALL_TAC] THEN
   DISCH_THEN(X_CHOOSE_TAC `u:real`) THEN
   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
   REWRITE_TAC[DEPENDENT_EXPLICIT] THEN
   MAP_EVERY EXISTS_TAC [`{a:real^N,b}`;
                         `\x:real^N. if x = a then u - &1 else &1`] THEN
   REWRITE_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL] THEN
   CONJ_TAC THENL
    [EXISTS_TAC `b:real^N` THEN ASM_REWRITE_TAC[IN_INSERT] THEN
     REAL_ARITH_TAC;
     ALL_TAC] THEN
   SIMP_TAC[VSUM_CLAUSES; FINITE_RULES] THEN
   ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID];
   ALL_TAC] THEN
 W(MP_TAC o PART_MATCH (lhs o rand) AFFINE_HULL_INSERT_SPAN o rand o goal_concl) THEN
 ANTS_TAC THENL
  [REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
   REWRITE_TAC[VECTOR_ARITH `u = u + a <=> a = vec 0`] THEN
   ASM_MESON_TAC[INDEPENDENT_NONZERO; IN_INSERT];
   ALL_TAC] THEN
 DISCH_THEN SUBST1_TAC THEN
 FIRST_ASSUM(MP_TAC o ISPEC `\x:real^N. u + x` o MATCH_MP IMAGE_SUBSET) THEN
 REWRITE_TAC[GSYM IMAGE_o; o_DEF; IMAGE_ID;
             ONCE_REWRITE_RULE[VECTOR_ADD_SYM] VECTOR_SUB_ADD] THEN
 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] SUBSET_TRANS) THEN
 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
 REWRITE_TAC[SIMPLE_IMAGE; IMAGE_CLAUSES; VECTOR_ADD_SUB] THEN
 SET_TAC[]);;

(* this LEMMA in determinants.ml 
let DET_3 = new_axiom_removed`!A:real^3^3.
        det(A) = A$1$1 * A$2$2 * A$3$3 +
                 A$1$2 * A$2$3 * A$3$1 +
                 A$1$3 * A$2$1 * A$3$2 -
                 A$1$1 * A$2$3 * A$3$2 -
                 A$1$2 * A$2$1 * A$3$3 -
                 A$1$3 * A$2$2 * A$3$1`;;
*)


let det_vec3 = new_definition ` det_vec3 (a:real^3) (b:real^3) (c:real^3) = 
  a$1 * b$2 * c$3 + b$1 * c$2 * a$3 + c$1 * a$2 * b$3 - 
  ( a$1 * c$2 * b$3 + b$1 * a$2 * c$3 + c$1 * b$2 * a$3 ) `;;



let DET_VEC3_EXPAND = 
prove
 (`det (vector [a; b; (c:real^3)] ) = det_vec3 a b c`,

 REWRITE_TAC[det_vec3; DET_3; VECTOR_3] THEN REAL_ARITH_TAC);;


let COPLANAR_DET_VEC3_EQ_0 = 
prove( `!v0 v1 (v2: real^3) v3.
       coplanar_alt {v0,v1,v2,v3} <=>
       det_vec3 ( v1 - v0 ) ( v2 - v0 ) ( v3 - v0 ) = &0`,




let COPLANAR_3 = 
prove
 (`!a b c:real^N. 2 <= dimindex(:N) ==> coplanar_alt {a,b,c}`,

 SIMP_TAC[COPLANAR_ALT; SUBSET] THEN MESON_TAC[HULL_INC]);;


let NONCOPLANAR_4_DISTINCT = 
prove
 (`!a b c d:real^N.
       ~(coplanar_alt{a,b,c,d}) /\ 2 <= dimindex(:N)
       ==> ~(a = b) /\ ~(a = c) /\ ~(a = d) /\
           ~(b = c) /\ ~(b = d) /\ ~(c = d)`,

 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
 STRIP_TAC THEN ASM_SIMP_TAC[INSERT_AC; COPLANAR_3]);;




let NONCOPLANAR_3_BASIS = 
prove
 (`!v1 v2 v3 v0 v:real^3.
    ~coplanar_alt {v0, v1, v2, v3}
    ==> (?t1 t2 t3.
             v = t1 % (v1 - v0) + t2 % (v2 - v0) + t3 % (v3 - v0) /\
             (!ta tb tc.
                  v = ta % (v1 - v0) + tb % (v2 - v0) + tc % (v3 - v0)
                  ==> ta = t1 /\ tb = t2 /\ tc = t3))`,

 REPEAT STRIP_TAC THEN
 FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
   NONCOPLANAR_4_DISTINCT)) THEN
 REWRITE_TAC[DIMINDEX_3; ARITH] THEN STRIP_TAC THEN
 SUBGOAL_THEN `independent {v1 - v0:real^3,v2 - v0,v3 - v0}` ASSUME_TAC THENL
  [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [COPLANAR_DET_EQ_0]) THEN
   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[independent] THEN
   DISCH_TAC THEN MATCH_MP_TAC DET_DEPENDENT_ROWS THEN
   REWRITE_TAC[rows; row; LAMBDA_ETA; GSYM IN_NUMSEG; DIMINDEX_3] THEN
   ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
   CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
   ASM_REWRITE_TAC[IMAGE_CLAUSES; VECTOR_3];
   ALL_TAC] THEN
 MP_TAC(ISPECL [`(:real^3)`; `{v1 - v0:real^3,v2 - v0,v3 - v0}`]
   CARD_GE_DIM_INDEPENDENT) THEN
 ASM_REWRITE_TAC[DIM_UNIV; SUBSET_UNIV] THEN ANTS_TAC THENL
  [SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_RULES] THEN
   ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DIMINDEX_3; ARITH;
                   VECTOR_ARITH `x - a:real^N = y - a <=> x = y`];
   ALL_TAC] THEN
 REWRITE_TAC[SUBSET; IN_UNIV; SPAN_BREAKDOWN_EQ; SPAN_EMPTY] THEN
 DISCH_THEN(MP_TAC o SPEC `v:real^3`) THEN
 MAP_EVERY (fun t -> MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC t)
           [`t1:real`; `t2:real`; `t3:real`] THEN
 REWRITE_TAC[IN_SING; VECTOR_ARITH
   `a - b - c - d:real^N = vec 0 <=> a = b + c + d`] THEN
 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[] THEN
 MAP_EVERY X_GEN_TAC [`ta:real`; `tb:real`; `tc:real`] THEN
 REWRITE_TAC[VECTOR_ARITH
  `t1 % x + t2 % y + t3 % z = ta % x + tb % y + tc % z <=>
   (t1 - ta) % x + (t2 - tb) % y + (t3 - tc) % z = vec 0`] THEN
 STRIP_TAC THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
 REWRITE_TAC[DEPENDENT_EXPLICIT; NOT_EXISTS_THM] THEN
 DISCH_THEN(MP_TAC o SPECL
  [`{v1 - v0:real^3,v2 - v0,v3 - v0}`;
   `\v:real^3. if v = v1 - v0 then t1 - ta
               else if v = v2 - v0 then t2 - tb
               else t3 - tc`]) THEN
 SIMP_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL; VSUM_CLAUSES] THEN
 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID;
                 RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2;
                   VECTOR_ARITH `x - a:real^N = y - a <=> x = y`] THEN
 SIMP_TAC[DE_MORGAN_THM; REAL_SUB_0]);;




let DET_VEC3_AND_DELTA = 
prove(`!(a:real^3) b c d.
     &4 * ( det_vec3 (a - d) (b - d) (c - d) ) pow 2 =
     delta  ( dist3 a d pow 2)
     (dist3 b d pow 2)
     (dist3 c d pow 2) (dist3 a b pow 2) (dist3 a c pow 2) (dist3 b c pow 2)   `,

SIMP_TAC[dist3; dist] THEN 
REWRITE_TAC[GSYM (MESON[VECTOR_ARITH ` (a :real^N) - b = ( a - x ) - ( b - x ) `]`
  delta      (norm (a - d) pow 2)     (norm (b - d) pow 2)
     (norm (c - d) pow 2) (norm ((a - d)  - (b - d )) pow 2) 
(norm ((a - d)  - ( c - d )) pow 2) (norm ((b - d ) - ( c - d )) pow 2)    =
   delta   (norm (a - d) pow 2)     (norm (b - d) pow 2)   (norm (c - d) pow 2)
(norm (a - b) pow 2) (norm (a - c) pow 2) (norm (b - c) pow 2)    `)] THEN 
SIMP_TAC[ vector_norm; DOT_POS_LE; SQRT_WORKS] THEN 
REWRITE_TAC[DOT_3] THEN 
REWRITE_TAC[MESON[lemma_cm3]`((a:real^3) - d - (b - d))$1 = (a - d)$1 - (b - d)$1 /\
  (a - d - (b - d))$2 = (a - d)$2 - (b - d)$2 /\
  (a - d - (b - d))$3 = (a - d)$3 - (b - d)$3 `] THEN 
REWRITE_TAC[delta; det_vec3] THEN 
REAL_ARITH_TAC);;




let POLFLZY = 
prove(` !(x1:real^3) x2 x3 x4.
         let x12 = dist (x1,x2) pow 2 in
         let x13 = dist (x1,x3) pow 2 in
         let x14 = dist (x1,x4) pow 2 in
         let x23 = dist (x2,x3) pow 2 in
         let x24 = dist (x2,x4) pow 2 in
         let x34 = dist (x3,x4) pow 2 in
         coplanar_alt {x1, x2, x3, x4} <=> delta x12 x13 x14 x23 x24 x34 = &0 `,

LET_TR THEN REPEAT GEN_TAC THEN MP_TAC (GSYM (SPECL [` x2 :real^3`; 
` x3:real^3`;` x4:real^3`; ` x1 :real^3`] DET_VEC3_AND_DELTA)) THEN 
SIMP_TAC[dist3; DIST_SYM] THEN REWRITE_TAC[REAL_ARITH ` &4 * a = &0 <=> a = &0 `]
THEN SIMP_TAC[GSYM ( REAL_FIELD ` x = &0 <=> x pow 2 = &0 `);
COPLANAR_DET_VEC3_EQ_0]);;


let LEMMA15 = POLFLZY;;


let muy_delta = new_definition ` muy_delta = delta `;;


(* LEMMA29 *)
(*
let VCRJIHC = prove(`!(v1:real^3) v2 v3 v4 x34 x12 x13 x14 x23 x24.
         condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34
         ==> muy_delta x12 x13 x14 x23 x24 (dist (v3,v4) pow 2) = &0`,
REWRITE_TAC[condA; muy_delta] THEN MP_TAC POLFLZY THEN LET_TR THEN MESON_TAC[]);;
*)

let ZERO_NEUTRAL = REAL_ARITH ` ! x. &0 * x = &0 /\ x * &0 = &0 /\ &0 + x = x /\ x + &0 = x /\ x - &0 = x /\
  -- &0 = &0 `;;


let EQUATE_CONEFS_POLINOMIAL_POW2 = 
prove( `!a b c aa bb cc. ( ! x. 
     a * x pow 2 + b * x + c = aa * x pow 2 + bb * x + cc ) <=>
     a = aa /\ b = bb /\ c = cc`,
 REPEAT GEN_TAC THEN EQ_TAC THENL [
NHANH (MESON[]` (! (x:real). P x ) ==> P ( &0 ) /\ P ( &1 ) /\ P ( -- &1 )`) THEN 
REAL_ARITH_TAC THEN REAL_ARITH_TAC; SIMP_TAC[]]);;


let GJWYYPS = 
prove(`!x12 x13 x14 x15 x23 x24 x25 x34 x35 a b c.
    (! x45.  cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
     a  * x45 pow 2 + b * x45 + c )
     ==> b pow 2 - &4 * a * c =
         &16 * delta x12 x13 x14 x23 x24 x34 * delta x12 x13 x15 x23 x25 x35`,

ONCE_REWRITE_TAC[LTCTBAN] THEN REPEAT GEN_TAC THEN 
REWRITE_TAC[EQUATE_CONEFS_POLINOMIAL_POW2] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]
THEN SIMP_TAC[] THEN DISCH_TAC THEN REWRITE_TAC[ups_x; cayleytr; cayleyR;
 delta; ZERO_NEUTRAL] THEN REAL_ARITH_TAC);;

let LEMMA51 = GJWYYPS ;;


let NOT_TOW_EQ_IMP_COL_EQUAVALENT = 
prove_by_refinement(
`!v1 v2 (v:real^3). ~(v1 = v2) ==> (collinear {v, v1, v2} <=> v IN aff {v1, v2})`,

  (* {{{ proof *)
  [
  (REWRITE_TAC[COLLINEAR_EX]);
  (NHANH (MESON[]` a % b + c = vec 0 ==> ( a = &0 \/ ~(a = &0 ))`));
  (KHANANG);
  (NGOAC THEN PURE_ONCE_REWRITE_TAC[MESON[]` P a /\ a = &0 <=> P ( &0 )   /\ a = &0 `]);
  (REWRITE_TAC[REAL_ADD_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID]);
  (REWRITE_TAC[REAL_ARITH ` a + b= &0 <=> a = -- b `; VECTOR_ARITH` a % x + b % y = vec 0  <=> a % x = ( -- b) % y`]);
  (NHANH (MESON[REAL_ARITH ` a = &0 <=> -- a = &0 `; VECTOR_MUL_LCANCEL]` (b = --c /\ ~(b = &0 /\ c = &0)) /\ b % v1 = --c % v2  ==> v1 = v2 `));
  (SIMP_TAC[]);
  (REWRITE_TAC[AFF_2POINTS_INTERPRET; IN_ELIM_THM]);
  (REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC);
    (REWRITE_TAC[VECTOR_ARITH ` a % v + b % v1 + c % v2 = vec 0 <=>  a % v = ( -- b) % v1 + ( --c ) % v2 `]);
    (PHA THEN REWRITE_TAC[MESON[CHANGE_SIDE]` a % v = v1  /\               ~(a = &0) <=> v = &1 / a % v1 /\ ~( a = &0 ) `]);
    (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH `&1 / a * b = b / a`]);
     (REWRITE_TAC[AFF_2POINTS_INTERPRET; IN_ELIM_THM]);
    BY( (MESON_TAC[REAL_FIELD ` ~ ( a = &0 ) /\ a = -- (b + c) ==>   ( -- b) / a + ( -- c) / a = &1 `]));
   (STRIP_TAC);
   (EXISTS_TAC ` &1 `);
   (EXISTS_TAC ` -- ta`);
   (EXISTS_TAC ` -- tb`);
   (PHA);
   (ASM_SIMP_TAC[REAL_ARITH` ~(&1 = &0 ) /\ -- ( -- a + -- b ) = a + b `]);
  BY( (CONV_TAC VECTOR_ARITH))
  ]);;
  (* }}} *)


(*
let LEMMA30 = prove(`!v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 a b c.
         condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\
         (!x12 x13 x14 x23 x24 x34.
              muy_delta x12 x13 x14 x23 x24 x34 =
              a x12 x13 x14 x23 x24 * x34 pow 2 +
              b x12 x13 x14 x23 x24 * x34 +
              c x12 x13 x14 x23 x24 )
         ==> (v3 IN aff {v1, v2} \/ v4 IN aff {v1, v2} <=>
              b x12 x13 x14 x23 x24 pow 2 -
              &4 * a x12 x13 x14 x23 x24 * c x12 x13 x14 x23 x24 =
              &0)`,
REWRITE_TAC[muy_delta; DELTA_COEFS; EQUATE_CONEFS_POLINOMIAL_POW2 ] THEN 
ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[] THEN REPEAT GEN_TAC THEN 
DISCH_TAC THEN REWRITE_TAC[REAL_ARITH` a - b * -- c * d = a + b * c * d `; 
AGBWHRD] THEN DOWN_TAC THEN SIMP_TAC[condA; REAL_ENTIRE; 
GSYM NOT_TOW_EQ_IMP_COL_EQUAVALENT] THEN ONCE_REWRITE_TAC[MESON[PER_SET3]`
 p {v3, v1, v2} \/ p {v4, v1, v2}  <=> p {v1,v2,v3} \/ p {v1,v2,v4} `] THEN 
ONCE_REWRITE_TAC[MESON[UPS_X_SYM]` ups_x x12 x23 x13 = &0 \/ 
ups_x x12 x24 x14 = &0 <=>     ups_x x12 x13 x23 = &0 \/ 
ups_x x12 x14 x24 = &0 `] THEN MESON_TAC[UPS_X_SYM; PER_SET3; FHFMKIY]);;
*)

(* let EWVIFXW = LEMMA30;; *)


let LEMMA51 = GJWYYPS;;
let LEMMA50 = LTCTBAN;;

let muy_v = new_definition ` muy_v (x1: real^N ) (x2:real^N) (x3:real^N) (x4:real^N)
(x5:real^N) x45 = 
          (let x12 = dist (x1,x2) pow 2 in
          let x13 = dist (x1,x3) pow 2 in
          let x14 = dist (x1,x4) pow 2 in
          let x15 = dist (x1,x5) pow 2 in
          let x23 = dist (x2,x3) pow 2 in
          let x24 = dist (x2,x4) pow 2 in
          let x25 = dist (x2,x5) pow 2 in
          let x34 = dist (x3,x4) pow 2 in
          let x35 = dist (x3,x5) pow 2 in
          cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45) `;;

let REMOVE_TAC = MATCH_MP_TAC (MESON[]` a ==> b ==> a `);;

let ALE = MESON[LTCTBAN]`!x12 x13 x14 x15 x23 x24 x25 x34 x35.
     (!a b c. (! x.
          cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x =
          a * x pow 2 + b * x + c )
          ==> b pow 2 - &4 * a * c = &0)
     ==> cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) pow 2 -
         &4 *
         ups_x x12 x13 x23 *
         cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) =
         &0`;;

let DISCRIMINANT_OF_CAY = MESON[LTCTBAN; GJWYYPS]`cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) pow 2 -
 &4 * ups_x x12 x13 x23 * cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) =
 &16 * delta x12 x13 x14 x23 x24 x34 * delta x12 x13 x15 x23 x25 x35`;;

let NOT_TWO_EQ_IMP_COL_EQUAVALENT = NOT_TOW_EQ_IMP_COL_EQUAVALENT;;


let GDLRUZB = 
prove(` ! (v1:real^3) (v2:real^3) (v3:real^3) (v4:real^3) (v5:real^3) a b c.
  coplanar_alt {v1, v2, v3, v4} \/ coplanar_alt {v1, v2, v3, v5} <=>
         (! a b c. (! x. muy_v v1 v2 v3 v4 v5 x = a * x pow 2 + b * x + c )
 ==> b pow 2 - &4 * a * c = &0) `,
REWRITE_TAC[muy_v] THEN LET_TR THEN 
REPEAT GEN_TAC THEN EQ_TAC THENL [DISCH_TAC THEN 
NHANH (MESON[GJWYYPS]` (!x45. cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
                a * x45 pow 2 + b * x45 + c)
         ==> b pow 2 - &4 * a * c =
             &16 *
             delta x12 x13 x14 x23 x24 x34 *
             delta x12 x13 x15 x23 x25 x35`) THEN SIMP_TAC[] THEN 
UNDISCH_TAC ` coplanar_alt {(v1:real^3), v2, v3, v4}\/ coplanar_alt {v1, v2, v3, v5}` THEN 
MP_TAC LEMMA15 THEN LET_TR THEN REWRITE_TAC[REAL_FIELD` &16 * a * b = &0 
<=> a = &0 \/ b = &0 `] THEN SIMP_TAC[]; NHANH (SPEC_ALL ALE) THEN 
REWRITE_TAC[DISCRIMINANT_OF_CAY ] THEN MP_TAC POLFLZY THEN LET_TR THEN 
REWRITE_TAC[REAL_FIELD` &16 * a * b = &0 <=> a = &0 \/ b = &0 `] THEN 
MESON_TAC[]]);;



let DET_VECC3_AND_DELTA = 
prove(` (! d a b c .
      delta (dist3 d a pow 2) (dist3 d b pow 2) (dist3 d c pow 2) (dist3 a b pow 2)
      (dist3 a c pow 2)
      (dist3 b c pow 2) =
      &4 * det_vec3 (a - d) (b - d) (c - d) pow 2) `,
 MESON_TAC[D3_SYM; 
DET_VEC3_AND_DELTA]);;



let DELTA_POS_4POINTS = 
prove(`!x1 x2 x3 (x4:real^3).
     &0 <=
     delta (dist (x1,x2) pow 2) (dist (x1,x3) pow 2) (dist (x1,x4) pow 2)
     (dist (x2,x3) pow 2)
     (dist (x2,x4) pow 2)
     (dist (x3,x4) pow 2)`,
 REWRITE_TAC[GSYM dist3] THEN SIMP_TAC[D3_SYM] THEN 
MP_TAC (DET_VECC3_AND_DELTA) THEN SIMP_TAC[] THEN DISCH_TAC THEN MP_TAC
 REAL_LE_SQUARE_POW THEN MESON_TAC[REAL_ARITH` &0 <= x <=> &0 <= &4 * x `]);;




let DIST_POW2_DOT =

prove(` ! a (b:real^N) . dist (a,b) pow 2 = ( a - b ) dot ( a- b) `,

let UPS_X_POS = MESON[lemma8; UPS_X_SYM; NORM_SUB]` &0 <=
          ups_x (norm ((x1 : real^3) - x2) pow 2) (norm (x1 - x3) pow 2)
          (norm (x2 - x3) pow 2) `;;

let UPS_X_SYM = MESON[UPS_X_SYM]` !x y z. ups_x x y z = ups_x y x z /\ ups_x x y z = ups_x x z y
  /\ ups_x x y z = ups_x x z y `;;


end;;