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


(* second half of collect_geom.ml.  
It was split in half by thales Feb 2010.

This file was edited by thales on 2012-5-15
to make it possible to load everything up through lemma GDRQXLG
giving the formula for the circumradius of a simplex.

Everything dependent on unproved axioms was commented out.

Feb 2013, some excess material removed.
 *)

flyspeck_needs "leg/cayleyR_def.hl";;
flyspeck_needs "leg/collect_geom.hl";;

module Collect_geom2 (* : Collect_geom2_type *)  = struct

  open Sphere;;
  open Geomdetail;;
  open Collect_geom;;



  let cayleyR = Cayleyr.cayleyR;;

  let LET_TR = Collect_geom.LET_TR;;
  let DIST_POW2_DOT = Collect_geom.DIST_POW2_DOT;;
  let UPS_X_POS = Collect_geom.UPS_X_POS;;
  let DELTA_POS_4POINTS = Collect_geom.DELTA_POS_4POINTS;;
  let REAL_LDISTRIB = REAL_ADD_LDISTRIB;;
  let POW_2 = REAL_POW_2;;
  let REAL_POSSQ = REAL_LT_SQUARE;;
  let REAL_RDISTRIB = REAL_ARITH 
    `!x y z. (x + y) * z = (x * z) + (y * z)`;;  (* Tactics_jordan *)

  let BY = Hales_tactic.BY;;

(* deprecated def from sphere.hl *)  
  
let mk_vec3 = new_definition 
  `mk_vec3 a b c = vector[a; b; c]`;;
  
let real3_of_triple = new_definition 
    `real3_of_triple (a,b,c) = (mk_vec3 a b c):real^3`;;
  
let triple_of_real3 = new_definition 
    `triple_of_real3 (v:real^3) = 
    (v$1, v$2, v$3)`;;
  
(* deprecated def from sphere.hl *)


(* this lemma is proved as below, but it take quite a long time to run it *)

let CAYLEYR_5POINTS = 
prove(`  !x1 x2 x3 x4 (x5 :real^3). 
         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
         let x45 = dist (x4,x5) pow 2 in
         cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `,

LET_TR THEN REWRITE_TAC[ DIST_POW2_DOT] THEN REPEAT GEN_TAC THEN 
REWRITE_TAC[ MESON[VECTOR_ARITH` (a:real^n) - b = a - x - ( b - x ) `]`
  AA ( (x1 - x5 ) dot ( x1 - x5)) ((x2 - x3) dot (x2 - x3))
 ((x2 - x4) dot (x2 - x4))
 ((x2 - x5) dot (x2 - x5))
 ((x3 - x4) dot (x3 - x4))
 ((x3 - x5) dot (x3 - x5))
 ((x4 - x5) dot (x4 - x5)) =
  AA ( (x1 - x5 ) dot ( x1 - x5)) ((x2 - x1 - ( x3 - x1 )) dot (x2 - x1 - ( x3 - x1 )))
  ((x2 - x1 - ( x4 - x1 )) dot (x2 - x1 - ( x4 - x1 )))
  ((x2 - x1 - ( x5 - x1 )) dot (x2 - x1 - ( x5 - x1 )))
  ((x3 - x1 - ( x4 - x1 )) dot (x3 - x1 - ( x4 - x1 )))
  ((x3 - x1 - ( x5 - x1 )) dot (x3 - x1 - ( x5 - x1 )))
    ((x4 - x1 - ( x5 - x1 )) dot (x4 - x1 - ( x5 - x1 ))) ` ] THEN 
SIMP_TAC[VECTOR_ARITH ` ((x4: real^N) - x1 - (x5 - x1)) = x1 - x5 - ( x1 - x4 ) `] THEN 
ABBREV_TAC ` x12 = (x1 - ( x2:real^3)) ` THEN 
ABBREV_TAC ` x13 = (x1 - ( x3:real^3)) ` THEN 
ABBREV_TAC ` x14 = (x1 - ( x4:real^3)) ` THEN 
ABBREV_TAC ` x15 = (x1 - ( x5:real^3)) ` THEN 
REWRITE_TAC[DOT_3] THEN REWRITE_TAC[lemma_cm3; cayleyR] THEN REAL_ARITH_TAC);;
 




let LEMMA3 = 
prove(` !x1 x2 x3 x4 (x5 :real^3). 
                 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
         let x45 = dist (x4,x5) pow 2 in
         &0 <= ups_x x12 x13 x23 /\
         &0 <= delta x12 x13 x14 x23 x24 x34 /\
         cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `,
 MP_TAC 
CAYLEYR_5POINTS THEN LET_TR THEN 
SIMP_TAC[ dist; UPS_X_POS; DELTA_POS_4POINTS]);;

(* LEMMA 3 *)
let NUHSVLM = LEMMA3;;


(* OLD END OF MODULE *)


let LEMMA52 = 
prove( `! v1 v2 v3 v4 (v5:real^3).
  muy_v v1 v2 v3 v4 v5 ( (dist3 v4 v5) pow 2 ) = &0 `,

REWRITE_TAC[muy_v; dist3] THEN MP_TAC LEMMA3 THEN 
LET_TR THEN SIMP_TAC[]);;
let PFDFWWV = LEMMA52;;

let PRE_VIET = 
REAL_ARITH `!x x1 x2. (x - x1) * (x - x2) = x pow 2 - (x1 + x2) * x + x1 * x2 /\
 a * (x - x1) * (x - x2) = a * x pow 2 + ( -- a * (x1 + x2)) * x + a * x1 * x2 `;;


let VIET_THEOREM = 
prove(`! x1 x2 a b c. (!x. a * x pow 2 + b * x + c = 
a * (x - x1) * (x - x2)) ==>  -- b = a * ( x1 + x2 ) /\ c = a * x1 * x2 `,

REWRITE_TAC[PRE_VIET; REAL_LDISTRIB;REAL_SUB_LDISTRIB;
REAL_ARITH ` a - b * c = a + -- b * c `; REAL_ARITH` ( a + b ) + c = 
a + b + c `] THEN 
REWRITE_TAC[REAL_MUL_ASSOC; EQUATE_CONEFS_POLINOMIAL_POW2] THEN 
SIMP_TAC[] THEN REAL_ARITH_TAC);;
let ADD_SUB_POW2_EX = REAL_RING ` ( a + b ) pow 2 = a pow 2 + &2 * a * b + b pow 2 /\
( a - b ) pow 2 = a pow 2 - &2 * a * b + b pow 2 `;;

let PRESENT_SUB_POW2 = REAL_RING` ! a b. ( a - b ) pow 2 = ( a + b ) pow 2 
  - &4 * a * b `;;

let DIST_ROOT_AND_DISCRIMINANT = 
prove(` ! a b c x1 x2. ( ! x. a * x pow 2 + b * x + c =
 a * ( x - x1 ) * ( x - x2 ) )
  ==> ( a pow 2 ) * ( x1 - x2 ) pow 2 = b pow 2 - &4 * a * c `,

NHANH (SPEC_ALL VIET_THEOREM) THEN REWRITE_TAC[PRESENT_SUB_POW2] THEN 
SIMP_TAC[REAL_ARITH ` -- b = a <=> b = -- a `] THEN REAL_ARITH_TAC);;
(* le 33. P 22 MARKED *)

let REAL_EQ_TO_LE_LT = REAL_ARITH ` 
  ( a = b <=> ~( a < b \/ b < a ) )`;;

let FEBRUARY_13_09 = 
prove(` &0 < (u - v) dot (&2 % x - (u + v)) <=>
  &0 < (u - v) dot (x - &1 / &2 % (u + v)) `,

ONCE_REWRITE_TAC[MESON[REAL_ARITH ` &0 < a <=> &0 < &2 * a `]` (a <=> &0 < b ) <=>
  ( a <=> &0 < &2 * b ) `] THEN ONCE_REWRITE_TAC[VECTOR_ARITH ` x * (a dot b) =
  a dot x % b `] THEN 
REWRITE_TAC[GSYM VECTOR_SUB_DISTRIBUTE; VECTOR_MUL_ASSOC] THEN 
REWRITE_TAC[REAL_ARITH ` &2 * &1 / &2 = &1 `; VECTOR_MUL_LID]);;
let SUB_DOT_NEG_TO_POS = MESON[VECTOR_ARITH ` ( a - b ) dot x = 
--  (( b - a ) dot x ) `;  REAL_ARITH ` -- a < &0 <=> &0 < a `]
`! a b.  ( a - b ) dot x < &0 <=> &0 < ( b - a ) dot x `;;


let LEMMA6 = 
prove(` !(u:real^3) v. ~(u = v) ==> plane_norm (bis u v) `,

REWRITE_TAC[plane_norm; bis] THEN REPEAT STRIP_TAC THEN 
EXISTS_TAC ` (u: real^3) - v ` THEN 
EXISTS_TAC ` &1 / &2 % ((u: real^3) + v )` THEN 
REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN ASM_SIMP_TAC[VECTOR_SUB_EQ] THEN 
REWRITE_TAC[REAL_EQ_TO_LE_LT; DIST_LT_HALF_PLANE;FEBRUARY_13_09;
 SUB_DOT_NEG_TO_POS] THEN SIMP_TAC[VECTOR_ADD_SYM] THEN MESON_TAC[]);;
let BXVMKNF = LEMMA6;;


let b_coef = BC_DEL_FOR;;
let c_coef = b_coef ;;

let DELTA_X34_B = 
prove(` ! x12 x13 x14 x23 x24 x. delta_x34 x12 x13 x14 x23 x24 x =
  -- &2 * x12 * x + b_coef x12 x13 x14 x23 x24 `,
 REWRITE_TAC[ delta_x34; b_coef]);;



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 EQ_SQRT_POW2_EQ = 
prove(` &0 <= a /\ &0 <= b ==> ( a = sqrt b <=> a pow 2 = b ) `,

SIMP_TAC[SQRT_WORKS; EQ_POW2_COND]);;

(*
let LEMMA33 = prove(` !x34 x12 x13 v1 x14 v3 x23 v2 v4 x24 x34' x34'' a.
 condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\
          (! x. muy_delta x12 x13 x14 x23 x24 x = a * ( x - x34' ) * ( x - x34'')) 
/\ x34' <= x34'' 
  ==> delta_x34 x12 x13 x14 x23 x24 x34' =
             sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) /\
             delta_x34 x12 x13 x14 x23 x24 x34'' =
             --sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) `,
REWRITE_TAC[muy_delta; DELTA_X34_B; DELTA_COEFS] THEN 
SIMP_TAC[EQUATE_CONEFS_POLINOMIAL_POW2; PRE_VIET; 
REAL_ARITH ` -- a = b <=> b = -- a`] THEN 
SIMP_TAC[REAL_RING `-- &2 * x12 * x34' + -- --x12 * (x34' + x34'') = a <=>
  -- &2 * x12 * x34'' + -- --x12 * (x34' + x34'') = -- a `] THEN 
REWRITE_TAC[REAL_ARITH` -- &2 * x12 * x34'' + -- --x12 * (x34' + x34'')
  = x12 * ( x34' - x34'' ) `; condA] THEN REPEAT STRIP_TAC THEN 
EXPAND_TAC "x12"  THEN EXPAND_TAC "x13" THEN EXPAND_TAC "x23" THEN 
EXPAND_TAC "x14" THEN EXPAND_TAC "x24" THEN 
UNDISCH_TAC ` x34' <= (x34'':real)` THEN 
ONCE_REWRITE_TAC[REAL_ARITH ` a <= b <=> &0 <= b - a `] THEN 
ONCE_REWRITE_TAC[ REAL_ARITH ` a * ( b - c ) = -- ( a * ( c - b ) ) `] THEN 
MP_TAC (GEN_ALL TROI_OI_DAT_HOI) THEN MP_TAC REAL_LE_POW_2 THEN 
REWRITE_TAC[REAL_ARITH` -- a = -- b <=> a = b `] THEN 
SIMP_TAC[UPS_X_SYM; REAL_LE_MUL; EQ_SQRT_POW2_EQ ] THEN 
ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN 
ONCE_REWRITE_TAC[ REAL_ARITH ` ( a * b ) pow 2 = a pow 2 * b pow 2 `] THEN 
REWRITE_TAC[PRESENT_SUB_POW2] THEN 
REWRITE_TAC[REAL_SUB_LDISTRIB; REAL_ARITH ` a pow 2 * b pow 2 = 
( -- a * b ) pow 2   /\ a pow 2 * &4 * b = -- a * &4 * -- a * b `] THEN 
UNDISCH_TAC `b_coef x12 x13 x14 x23 x24 = --a * (x34' + x34'')` THEN 
UNDISCH_TAC `c_coef x12 x13 x14 x23 x24 = a * x34' * x34''` THEN 
UNDISCH_TAC `(a: real) = --x12` THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 
SIMP_TAC[] THEN SIMP_TAC[REAL_ARITH` -- -- a = a /\ ( -- a * b) pow 2 = 
  ( a * b ) pow 2 /\ ( a * -- b) pow 2 = ( a * b ) pow 2  `; REAL_ADD_SYM;
 REAL_MUL_SYM] THEN SIMP_TAC[REAL_ADD_SYM; REAL_MUL_SYM] THEN 
ONCE_REWRITE_TAC[REAL_ARITH ` ( a * b ) pow 2 = ( b * -- a ) pow 2 `] THEN 
SIMP_TAC[] THEN REPEAT STRIP_TAC THEN EXPAND_TAC "a" THEN 
REWRITE_TAC[REAL_RING ` a - -- c * b * &4 = a + &4 * c * b `] THEN 
MESON_TAC[AGBWHRD; UPS_X_SYM]);;
*)

(* let CMUDPKT = LEMMA33;; *)

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


let LEMMA_OF_LE20 = 
prove(` ! x y z: real^3.
   &2 <= dist3 x y /\
         dist3 x y <= #2.52 /\
         &2 <= dist3 x z /\
         dist3 x z <= #2.2 /\
         &2 <= dist3 y z /\
         dist3 y z <= #2.2
         ==> ~collinear {x, y, z}  `,

MP_TAC JVUNDLC THEN 
SIMP_TAC[] THEN 
ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 
REWRITE_TAC[MESON[]` (! a b c s. P a b c = s ==> Q a b c ) <=> 
  (! a b c . Q a b c ) `] THEN 
SIMP_TAC[COL_EQ_UPS_0] THEN 
MATCH_MP_TAC (TAUT` a ==> b ==> a `) THEN 
REWRITE_TAC[GSYM dist3] THEN 
REWRITE_TAC[REAL_ENTIRE] THEN 
CONV_TAC REAL_FIELD);;


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

let ETA_Y_LT_SQRT2 = 
prove(`eta_y #2.2 #2.2 #2.52 < sqrt #2`,

REWRITE_TAC[eta_y; eta_x; ups_x] THEN LET_TR THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC (REAL_FIELD ` &14641 / &8131< &2 `)
 THEN MP_TAC (REAL_FIELD ` &0 < &2 /\ &0 < &14641 / &8131 `) THEN 
NHANH (SPEC_ALL SQRT_POS_LT) THEN REWRITE_TAC[ REAL_ARITH ` #2 = &2 `] THEN 
SIMP_TAC[REAL_ARITH ` &0 < a ==> &0 <= a `;SQRT_POS_LT; LT_POW2_EQ_LT; SQRT_WORKS]);;
let ETA_YY_LT_SQRT2 = MESON[ETA_Y_LT_SQRT2; REAL_ARITH ` #2 = &2 `]`
  eta_y #2.2 #2.2 #2.52 < sqrt ( &2 ) `;;

let THANG_DEU = 
prove(` &2 <= x ==> &2 pow 2 <= x pow 2 `,

NHANH (REAL_ARITH ` &2 <= x ==> &0 <= &2 /\ &0 <= x `) 
THEN MESON_TAC[POW2_COND]);;
let NGAY23_THANG2_09 = 
prove(` &2 <= y /\ y <= sqrt (&8) ==>
  &2 pow 2 <= y * y /\ y * y <= &8 `,

REWRITE_TAC[ GSYM REAL_POW_2] THEN DISCH_TAC THEN CONJ_TAC THENL 
[ASM_MESON_TAC[REAL_ARITH ` &2 <= a ==> &0 <= &2 /\ &0 <= a `;POW2_COND]; 
ASM_MESON_TAC[ SQRT_WORKS; REAL_ARITH ` &0 <= &8 `;
  POW2_COND; REAL_ARITH `&2 <= a /\ a <= b ==> &0 <= b /\ &0 <= a `]]);;


let ETA_Y_SQRT8_2_251 = 
prove(` eta_y ( sqrt (&8) ) (&2) #2.51 < #1.453`,

REWRITE_TAC[eta_y; eta_x; ups_x; GSYM POW_2] THEN 
LET_TR THEN 
REWRITE_TAC[MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
MP_TAC (REAL_FIELD ` &0 < &20160320000 / &9551113999 /\ &0 < #1.453 `) THEN 
NHANH (SPEC_ALL SQRT_POS_LT) THEN 
SIMP_TAC[LT_POW2_EQ_LT; REAL_ARITH ` &0 < a ==> &0 <= a `; SQRT_POW_2] THEN 
DISCH_TAC THEN 
CONV_TAC REAL_FIELD );;
let CDEUSDF_CHANGE = CDEUSDF;;


let CIRCUMCENTER_FORMULAR = 
prove(` ! va vb vc.  ~collinear {va, vb, vc}
 ==> circumcenter {va, vb, vc} =
  (dist3 vb vc pow 2 *
           (dist3 va vc pow 2 + dist3 va vb pow 2 - dist3 vb vc pow 2)) /
          (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
          va +
          (dist3 va vc pow 2 *
           (dist3 vb vc pow 2 + dist3 va vb pow 2 - dist3 va vc pow 2)) /
          (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
          vb +
          (dist3 va vb pow 2 *
           (dist3 vb vc pow 2 + dist3 va vc pow 2 - dist3 va vb pow 2)) /
          (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
          vc `,

ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 
MP_TAC CDEUSDF_CHANGE THEN LET_TR THEN MESON_TAC[]);;
let LE_EX = REAL_ARITH ` &0 <= a <=> a = &0 \/ &0 < a `;;

let SUM_UPS_X_1 = 
prove(`!a b c.
     &0 < ups_x a b c
     ==> (c * (b + a - c)) / ups_x a b c +
         (a * (c + b - a)) / ups_x a b c +
         (b * (c + a - b)) / ups_x a b c =
         &1`,
 REWRITE_TAC[ups_x] THEN CONV_TAC REAL_FIELD);;

MESON[POW2_COND; REAL_ARITH `&2 <= a /\ a <= b ==> &0 <= b /\ &0 <= a `]`
  &2 <= y /\ y <= b ==> y pow 2 <= b pow 2 `;;


let FACTOR_OF_QUADRARTIC = 
prove(`! a b c x. ~(a = &0) /\ 
&0 <= b pow 2 - &4 * a * c ==> a * x pow 2 + b * x + c =
     a *
     (x - (--b + sqrt (b pow 2 - &4 * a * c)) / (&2 * a)) *
     (x - (--b - sqrt (b pow 2 - &4 * a * c)) / (&2 * a))`   ,

REWRITE_TAC[PRE_VIET] THEN SIMP_TAC[REAL_FIELD ` ~( a = &0 ) ==> 
-- a * ( ( --b + del) / ( &2 * a ) + ( --b - del) / ( &2 * a )) = b `] THEN 
REWRITE_TAC[REAL_FIELD ` a / b * a' / b = ( a * a' ) / ( b pow 2 ) `] THEN 
REWRITE_TAC[REAL_FIELD ` a / b * a' / b = ( a * a' ) / ( b pow 2 ) `; 
  REAL_DIFFSQ; GSYM REAL_POW_2] THEN SIMP_TAC[SQRT_WORKS] THEN 
SIMP_TAC[REAL_FIELD ` ~ ( a = &0 ) ==> a * (--b pow 2 - 
 (b pow 2 - &4 * a * c)) / (&2 * a) pow 2 = c `]);;

let COMPUTE_TO_QUA_POLY = 
prove(` #2.696 <= x /\ x <= sqrt8  ==> 
x pow 2  * ( &1 / eta_y x #2.45 #2.45 pow 2 -
  &1 / eta_y x ( &2 ) #2.51 pow 2 ) = &4331842500 / &363188227801 * x pow 4 +
     -- &45702201 / &302530802 * x pow 2 +
     &529046001 / &2520040000 `,
 REWRITE_TAC[eta_y; eta_x; ups_x] THEN 
LET_TR THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
NHANH (MESON[REAL_ARITH ` #2.696 <= x /\ x <= sqrt8 ==>
  &0 <= #2.696 /\ &0 <= x `; REAL_LE_MUL2] ` #2.696 <= x /\ x <= sqrt8 ==>
   #2.696 * #2.696 <= x * x /\ x * x <= sqrt8 * sqrt8 `) THEN 
NHANH (MESON[REAL_ARITH ` #2.696 * #2.696 <= x ==> &0 <= #2.696 * #2.696 /\ &0 <= x `; REAL_LE_MUL2] `
  #2.696 * #2.696 <= x /\ x <= hh ==> (#2.696 * #2.696) * #2.696 * #2.696 <= x * x /\
  x * x <= hh * hh `) THEN 
REWRITE_TAC[sqrt8] THEN 
REWRITE_TAC[REAL_POLY_CONV ` (--(x * x) * x * x - &16 - &3969126001 / &100000000 +
        &2 * (x * x) * &63001 / &10000 +
        &2 * (x * x) * &4 +
        &63001 / &1250) `] THEN 
REWRITE_TAC[REAL_POLY_CONV `
  (--(x * x) * x * x - &5764801 / &160000 - &5764801 / &160000 +
        &2 * (x * x) * &2401 / &400 +
        &2 * (x * x) * &2401 / &400 +
        &5764801 / &80000) `] THEN 
REWRITE_TAC[REAL_ARITH ` x pow 4 = ( x pow 2 ) pow 2 `] THEN 
MP_TAC (REAL_ARITH ` ~ ( -- &1 = &0 ) /\ &0 <= ( &103001 / &5000 ) pow 2 - &4 * ( -- &1 ) * -- &529046001 / &100000000 `) THEN 
SIMP_TAC[FACTOR_OF_QUADRARTIC] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
REWRITE_TAC[REAL_ARITH ` (&252004 / &625) = ( &502 / &25 ) * ( &502 / &25 ) `] THEN 
REWRITE_TAC[MESON[REAL_ARITH ` &0 <= &502 / &25 /\ x * x = x pow 2 `; POW_2_SQRT]`
  sqrt ( ( &502 / &25 ) * ( &502 / &25 )) = ( &502 / &25 ) `] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
REWRITE_TAC[ GSYM POW_2] THEN 
REWRITE_TAC[REAL_ARITH `  a * x pow 2 + b * x = ( a * x + b ) * x `] THEN 
REWRITE_TAC[MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8`]` sqrt (&8) pow 2 = &8 `] THEN 
NHANH (REAL_FIELD ` (&113569 / &15625 <= x pow 2 /\ x pow 2 <= &8) 
  ==> &0 <= (-- &1 * x pow 2 + &2401 / &100) /\
  &0 <= (x pow 2 - &2601 / &10000 ) /\
  &0 <= -- ((x pow 2 - &203401 / &10000) )/\ &0 <= &5764801 / &160000 /\ 
&0 <= &63001 / &2500`) THEN 
MP_TAC REAL_LE_POW_2 THEN 
REWRITE_TAC[REAL_ARITH ` -- &1 * a * b = a * -- b `] THEN 
REWRITE_TAC[REAL_FIELD ` ( &1 / a ) pow 2  = &1 / ( a pow 2 ) `] THEN 
MP_TAC REAL_LE_MUL THEN 
MP_TAC REAL_LE_DIV THEN 
SIMP_TAC[ SQRT_WORKS] THEN 
REWRITE_TAC[REAL_SUB_LDISTRIB] THEN 
REWRITE_TAC[REAL_FIELD ` &1 / ( a / b ) = b / a `] THEN 
SIMP_TAC[REAL_FIELD ` &113569 / &15625 <= a ==> a * ( b / ( a * c )) = b / c `] THEN 
REWRITE_TAC[REAL_POLY_CONV ` ((-- &1 * x pow 2 + &2401 / &100) * x pow 2) / (&5764801 / &160000) -
     ((x pow 2 - &2601 / &10000) * --(x pow 2 - &203401 / &10000)) /
     (&63001 / &2500) `] THEN 
REWRITE_TAC[REAL_ARITH ` a pow 4 = a pow 2 pow 2 `]);;
(*
REAL_ARITH ` &4650694416 = ( &68196 ) pow 2 `;;
REAL_ARITH` &4650694416 / &363188227801 = ( &68196 / &602651 ) pow 2 `;;
*)

let PHAN_TICH = 
prove(  `! x. &4331842500 / &363188227801 *
     (x pow 2 - &488365801 / &44090000) *
     (x pow 2 - &2081667 / &1310000) =
     &4331842500 / &363188227801 * x pow 4 +
     -- &45702201 / &302530802 * x pow 2 +
     &529046001 / &2520040000`   ,
 REAL_ARITH_TAC);;
let Q_TR = 
prove(`! x. #2.696 <= x /\ x <= sqrt8 ==>
  x pow 2 *
         (&1 / eta_y x #2.45 #2.45 pow 2 - &1 / eta_y x (&2) #2.51 pow 2) <= &0 `,
 
SIMP_TAC[COMPUTE_TO_QUA_POLY; GSYM PHAN_TICH ] THEN 
NHANH (MESON[REAL_ARITH ` #2.696 <= x /\ x <= hh ==> &0 <= #2.696 /\ &0 <= x`
  ; REAL_LE_MUL2] ` #2.696 <= x /\ x <= hh ==>
   #2.696 * #2.696 <= x * x /\ x * x <= hh * hh `) THEN 
REWRITE_TAC[REAL_ARITH `
         &4331842500 / &363188227801 * a <= &0 <=> a <= &0 `] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
REWRITE_TAC[REAL_ARITH ` &0 <=
         &4331842500 / &363188227801 * a <=> &0 <= a `; sqrt8; GSYM POW_2;
  MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `] THEN 
NHANH (REAL_ARITH ` &113569 / &15625 <= x pow 2 /\
     x pow 2 <= &8 ==> x pow 2 - &488365801 / &44090000 <= &0 /\
  x pow 2 - &2081667 / &1310000 >= &0 `) THEN 
REWRITE_TAC[ REAL_ARITH ` ( a >= &0 <=> &0 <= a)/\ (a <= &0 <=> &0 <= -- a ) `] THEN 
REWRITE_TAC[REAL_ARITH ` -- ( a * b ) = -- a * b `] THEN 
MESON_TAC[REAL_LE_MUL]);;
let SQRT8_LT = 
prove(` sqrt (&8) < &4 * #2.45 `,

MP_TAC (REAL_ARITH ` &0 < &8 /\ &0 <  &4 * #2.45`) THEN 
SIMP_TAC[SQRT_POS_LT; LT_POW2_EQ_LT] THEN 
SIMP_TAC[REAL_LT_IMP_LE; SQRT_WORKS] THEN REAL_ARITH_TAC);;


let SQRT8_POW2 = MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `;;


let IM_UP_POS = 
prove(`! x. #2.696 <= x /\ x <= sqrt8 ==>
&0 < ups_x (x * x) (#2.45 * #2.45) (#2.45 * #2.45) /\
&0 < ups_x (x * x) (&2 * &2) (#2.51 * #2.51) `,

REWRITE_TAC[ups_x] THEN 
REWRITE_TAC[REAL_IDEAL_CONV [` (x:real) pow 2 `]` 
         --(x * x) * x * x -
         (#2.45 * #2.45) * #2.45 * #2.45 -
         (#2.45 * #2.45) * #2.45 * #2.45 +
         &2 * (x * x) * #2.45 * #2.45 +
         &2 * (x * x) * #2.45 * #2.45 +
         &2 * (#2.45 * #2.45) * #2.45 * #2.45 `] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
REWRITE_TAC[REAL_POLY_CONV ` --(x * x) * x * x - &16 - &3969126001 / &100000000 +
         &2 * (x * x) * &63001 / &10000 +
         &2 * (x * x) * &4 +
         &63001 / &1250 `] THEN 
NHANH (REAL_ARITH` #2.696 <= x /\ x <= s ==> &0 <= #2.696 /\
  &0 <= x /\ &0 <= s `) THEN 
ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> b ==> a ==> c `] THEN 
SIMP_TAC[POW2_COND; sqrt8; SQRT8_POW2] THEN 
NHANH (REAL_ARITH` #2.696 pow 2 <= x /\ x <= &8 ==> 
  &0 < &2401 / &100 + -- &1 * x /\ &0 < x /\
  ~ ( -- &1 = &0 ) /\ &0 <= ( &103001 / &5000 ) pow 2 - &4 * -- &1 *
  -- &529046001 / &100000000 `) THEN 
SIMP_TAC[REAL_ARITH ` x pow 4 = x pow 2 pow 2 `; FACTOR_OF_QUADRARTIC] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
REWRITE_TAC[REAL_ARITH ` &252004 / &625 = ( &502 / &25) pow 2 `] THEN 
REWRITE_TAC[MESON[POW_2_SQRT; REAL_ARITH ` &0 <= &502 / &25 `]` 
  sqrt ((&502 / &25) pow 2) = &502 / &25 `] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
NHANH (REAL_ARITH ` &113569 / &15625 <= x pow 2 /\ x pow 2 <= &8 ==>
  &0 < x pow 2 - &2601 / &10000 /\ &0 < -- (x pow 2 - &203401 / &10000) `) THEN 
REWRITE_TAC[REAL_ARITH ` -- &1 * a * b = a * --b `] THEN 
SIMP_TAC[REAL_LT_MUL]);;

let IMP_ETAY_POS = 
prove( `! x. #2.696 <= x /\ x <= sqrt8 ==>
&0 < eta_y x #2.45 #2.45 /\ &0 < eta_y x (&2) #2.51 `,

REWRITE_TAC[eta_y; eta_x] THEN 
LET_TR THEN 
NHANH (MESON[REAL_ARITH ` &0 <= #2.696`; REAL_LE_MUL2]`
  #2.696 <= x ==> #2.696 * #2.696 <= x * x `) THEN 
NHANH (REAL_ARITH ` #2.696 * #2.696 <= x * x ==>
  &0 < ((x * x) * (#2.45 * #2.45) * #2.45 * #2.45) /\
  &0 < ((x * x) * (&2 * &2) * #2.51 * #2.51) `) THEN 
MESON_TAC[IM_UP_POS; REAL_LT_DIV; SQRT_POS_LT]);;

let REAL_LE_RDIV_0 = 
prove(` ! a b. &0 < b ==> ( &0 <= a / b <=> &0 <= a ) `,

REWRITE_TAC[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `] THEN 
SIMP_TAC[REAL_LT_RDIV_0] THEN 
SIMP_TAC[REAL_FIELD `&0 < b ==> ( a / b = &0 <=> a = &0 ) `]);;

let NHSJMDH = 
prove(` ! y. #2.696 <= y /\ y <= sqrt8 ==>
     eta_y y (&2) (#2.51) <= eta_y y #2.45 (#2.45) `,

NHANH (SPEC_ALL Q_TR) THEN 
ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN 
NHANH (MESON[REAL_ARITH ` &0 <= #2.696`; REAL_LE_MUL2]`
  #2.696 <= x ==> #2.696 * #2.696 <= x * x `)  THEN 
REWRITE_TAC[POW_2] THEN 
NHANH (REAL_ARITH `#2.696 * #2.696 <= y ==> &0 < y `) THEN 
REWRITE_TAC[REAL_ARITH ` a * b <= &0 <=> &0 <= a * -- b `] THEN 
SIMP_TAC[REAL_LE_MUL_EQ] THEN 
ONCE_REWRITE_TAC[MESON[]`( a/\b ) /\ c <=> ( a /\ c ) /\ b `] THEN 
NHANH (SPEC_ALL IMP_ETAY_POS) THEN 
NHANH (REAL_ARITH ` &0 < eta_y a b c ==> ~(eta_y a b c = &0 ) `) THEN 
REWRITE_TAC[GSYM REAL_POSSQ] THEN SIMP_TAC[REAL_FIELD ` &0 < a /\
 &0 < b ==>  -- (&1 / a - &1 / b) = (a - b) / ( a * b ) `] THEN 
PHA THEN SIMP_TAC[REAL_LT_MUL; REAL_LE_RDIV_0] THEN 
REWRITE_TAC[GSYM REAL_DIFFSQ] THEN 
SIMP_TAC[REAL_LT_ADD; REAL_LE_MUL_EQ] THEN REAL_ARITH_TAC);;
(* NEW WORKS *)
let SQRT8_LE = MESON[ REAL_ARITH ` &0 <= &8`; SQRT_WORKS]` &0 <= sqrt (&8) `;;

let RELATE_POW2 = 
prove(` ( a = &0 <=> a pow 2 = &0 ) /\
  ( &0 < a pow 2 <=> &0 < a \/ ~( &0 <= a )) `,

MP_TAC (REAL_FIELD ` a = &0 <=> a pow 2 = &0 `) THEN DISCH_TAC THEN 
CONJ_TAC THENL [ASM_SIMP_TAC[]; MP_TAC REAL_LE_POW_2] THEN 
MP_TAC (REAL_ARITH `( ! a. &0 < a \/ ~(&0 <= a) \/ a = &0 )`) THEN 
MP_TAC (REAL_FIELD ` a = &0 <=> a pow 2 = &0 `) THEN 
REWRITE_TAC[REAL_ARITH ` A <= b <=> A = b \/ A < b `] THEN 
MESON_TAC[REAL_ARITH ` ~ ( a = &0 /\ ( &0 < a \/ ~( &0 <= a ) )) `]);;
let LT_POW2_COND = 
prove(`!a b. &0 <= a /\ &0 <= b ==> (a < b <=> a pow 2 < b pow 2)`,

REPEAT GEN_TAC THEN ASM_CASES_TAC ` a = &0 ` THENL
[ASM_SIMP_TAC[REAL_ARITH` &0 pow 2 = &0 `] THEN MESON_TAC[RELATE_POW2]; 
ASM_SIMP_TAC[REAL_LE_LT]] THEN STRIP_TAC THENL [ASM_MESON_TAC[LT_POW2_EQ_LT];
EXPAND_TAC "b"] THEN UNDISCH_TAC `&0 < a ` THEN REWRITE_TAC[REAL_ARITH `
 &0 pow 2 = &0 /\ (a < &0 <=> ~(&0 <= a))`] THEN MP_TAC REAL_LE_POW_2 THEN 
MESON_TAC[REAL_LT_IMP_LE]);;

let POS_IMP_POW2 = MESON[REAL_LE_TRANS; POW2_COND]` &0 <= a /\ a <= b ==> a pow 2 
  <= b pow 2 `;;


let SQRT8_LE_EQ_8_LESS_POW2 = 
prove(` sqrt (&8 ) <= a ==> &8 <= a pow 2 `,

MP_TAC SQRT8_LE THEN MESON_TAC[SQRT8_POW2; POS_IMP_POW2]);;

let MINIMAL_QUADRATIC_POLY = 
prove(` 
! b c (x:real). ( &4 * c - b pow 2 ) / &4 <= x pow 2 + b * x + c `,

ONCE_REWRITE_TAC[REAL_ARITH ` a <= b <=> &0 <= b - a `] THEN 
REWRITE_TAC[REAL_ARITH ` (x pow 2 + b * x + c) - (&4 * c - b pow 2) / &4
  = ( x + b / &2 ) pow 2 `; REAL_LE_POW_2]);;
let GREATER_THAN_MID_QUADRATIC_PO = 
prove(` ! b c x x0. -- b / &2 <= x0 /\ x0 <= x ==>
  x0 pow 2 + b * x0 + c <= x pow 2 + b * x + c `,

REWRITE_TAC[REAL_ARITH ` x0 pow 2 + b * x0 + c <= x pow 2 + b * x + c
  <=> &0 <= ( x - x0 ) * ( x + x0 + b ) `] THEN 
MESON_TAC[REAL_ARITH ` --b / &2 <= x0 /\ x0 <= x ==>
  &0 <= x - x0 /\ &0 <= x + x0 + b `; REAL_LE_MUL]);;
(* PERMAINENCE *)
(* MARCH WORKS *)

let SQRT8_TWO_TWO = 
prove(` sqrt (&8) <= &2 + &2 `,

MP_TAC SQRT8_LE THEN NHANH (MESON[REAL_ARITH ` &0 <= &2 + &2 `]
`&0 <= sqrt (&8) ==> &0 <= &2 + &2 `) THEN SIMP_TAC[POW2_COND] THEN 
SIMP_TAC[REAL_ARITH ` &0 <= &8 `; SQRT_WORKS] THEN REAL_ARITH_TAC);;

let A_POS_DELTA = 
prove(` &0 < delta (#3.2 pow 2 ) (sqrt8 pow 2 ) (&2 pow 2) (sqrt8 pow 2) 
(&2 pow 2) (&2 pow 2) `,
 REWRITE_TAC[delta; sqrt8; SQRT8_POW2] THEN REAL_ARITH_TAC);;
let MET_LAM_ROI = 
prove(` #3.2 < sqrt8 + &2 /\ #3.2 < &2 + &2 /\ sqrt8 < sqrt8 + &2 /\
sqrt8 < &2 + &2 `,

REWRITE_TAC[sqrt8; REAL_ARITH ` a < sqrt (&8) + b <=> a - b < sqrt (&8) `] THEN 
REWRITE_TAC[REAL_ARITH ` sqrt (&8) - &2 < sqrt (&8) `] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC SQRT8_LE  THEN 
MP_TAC (REAL_ARITH` &0 <= &6 / &5 /\ &0 <= &4 `) THEN 
SIMP_TAC[LT_POW2_COND ] THEN SIMP_TAC[LT_POW2_COND; SQRT8_POW2 ] THEN 
REAL_ARITH_TAC);;

let PROVE_POS_THINGS = 
prove(` ! x. x IN {#3.2 , sqrt8, &2 , sqrt8, &2, &2 } ==> &0 <= x `,

REWRITE_TAC[SET_RULE `( !x. x IN {a,b,c,d,s,e} ==> p x ) <=>
  p a /\ p b /\ p c /\ p d /\ p s /\ p e `;sqrt8;  SQRT8_LE] THEN REAL_ARITH_TAC);;


let IMP_GT_THAN_TWO = 
prove(` ! v1 v2 w1 (w2:real^3).
           CARD {v1, w1,v2, w2} = 4 /\
           packing {v1, w1,v2, w2}
==>       &2 <= dist3 w1 v2 /\
         &2 <= dist3 v2 w2 /\
         &2 <= dist3 v1 w2  `,

REWRITE_TAC[CARD4; packing; GSYM dist3; sqrt8] THEN SET_TAC[]);;
(*       THADGSB         *)


let LEMMA_FOR_PAHFWSI = 
prove(`! v1 v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\
         packing {v1, v2, v3, v4} /\
         dist (v1,v3) <= #3.2 /\
         #2.51 <= dist (v1,v2) /\
         dist (v2,v4) <= #2.51
==>     (!x. x IN {#3.2, #2.51, &2, #2.51, &2, &2} ==> &0 <= x) /\
         #3.2 < #2.51 + &2 /\
         #3.2 < &2 + &2 /\
         #2.51 < #2.51 + &2 /\
         #2.51 < &2 + &2 /\
         &0 <
         delta (#3.2 pow 2) (#2.51 pow 2) (&2 pow 2) (#2.51 pow 2) (&2 pow 2)
         (&2 pow 2) /\
         CARD {v1, v2, v3, v4} = 4 /\
         #2.51 <= dist3 v1 v2 /\
         &2 <= dist3 v2 v3 /\
         &2 <= dist3 v3 v4 /\
         &2 <= dist3 v1 v4 /\
         dist3 v1 v3 <= #3.2 /\
         dist3 v2 v4 <= #2.51 `,

REWRITE_TAC[SET_RULE ` (!x. x IN {a,b,c,d,e,f} ==> P x ) <=>
  P a /\ P b /\ P c /\ P d /\ P e /\ P f `; REAL_ARITH ` 
  &0 <= #2.51 /\
          &0 <= &2 /\
          &0 <= &2 /\
          &0 <= #3.2 /\
          &0 <= &2 /\
          &0 <= #2.51 /\ #2.51 < &2 + #2.51 /\
         #2.51 < &2 + &2 /\
         #3.2 < &2 + &2 /\
         #3.2 < #2.51 + &2 /\ #3.2 < &2 + #2.51 /\
         #2.51 < #2.51 + &2  `] THEN SIMP_TAC[GSYM dist3] THEN 
REWRITE_TAC[CARD4; packing; delta; dist3] THEN CONV_TAC REAL_RAT_REDUCE_CONV
THEN SET_TAC[]);;
let LEMMA_OF_39 = 
prove(` ! (v1:real^3) v2 w1 w2.
         CARD {v1, v2, w1, w2} = 4 /\
         packing {v1, v2, w1, w2} /\
         dist (w1,w2) <= #2.51 /\
         dist (v1,v2) <= #3.07
==> (!x. x IN {#2.51, &2, &2, #3.07, &2, &2} ==> &0 <= x) /\
     #2.51 < &2 + &2 /\
     #2.51 < &2 + &2 /\
     #3.07 < &2 + &2 /\
     #3.07 < &2 + &2 /\
     &0 <
     delta (#2.51 pow 2) (&2 pow 2) (&2 pow 2) (#3.07 pow 2) (&2 pow 2)
     (&2 pow 2) /\
     CARD {w1, v1, w2, v2} = 4 /\
     &2 <= dist3 w1 v1 /\
     &2 <= dist3 v1 w2 /\
     &2 <= dist3 w2 v2 /\
     &2 <= dist3 w1 v2 /\
     dist3 w1 w2 <= #2.51 /\
     dist3 v1 v2 <= #3.07 `,

REWRITE_TAC[SET_RULE ` (!x. x IN {a,b,c,d,e,f} ==> P x ) <=>
  P a /\ P b /\ P c /\ P d /\ P e /\ P f `; delta; GSYM dist3] THEN CONV_TAC 
REAL_RAT_REDUCE_CONV THEN REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL 
[ASM_MESON_TAC[SET_RULE ` {v1, v2, w1, w2} = {w1, v1, w2, v2}`];DOWN_TAC]
 THEN REWRITE_TAC[CARD4; packing; dist3] THEN SET_TAC[]);;
let LEMMA_OF_LEMMA40 = 
prove(`! v1 v2 w1 (w2:real^3).  CARD {v1, v2, w1, w2} = 4 /\
         packing {v1, v2, w1, w2} /\
         dist (v1,v2) <= #3.2 /\
         dist (w1,w2) <= #2.51 /\
         #2.2 <= dist (v1,w1)
==> (!x. x IN {#3.2, #2.2, &2, #2.51, &2, &2} ==> &0 <= x) /\
     #3.2 < #2.2 + &2 /\
     #3.2 < &2 + &2 /\
     #2.51 < #2.2 + &2 /\
     #2.51 < &2 + &2 /\
     &0 <
     delta (#3.2 pow 2) (#2.2 pow 2) (&2 pow 2) (#2.51 pow 2) (&2 pow 2)
     (&2 pow 2) /\
     CARD {v1, w1, v2, w2} = 4 /\
     #2.2 <= dist3 v1 w1 /\
     &2 <= dist3 w1 v2 /\
     &2 <= dist3 v2 w2 /\
     &2 <= dist3 v1 w2 /\
     dist3 v1 v2 <= #3.2 /\
     dist3 w1 w2 <= #2.51 `,

REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c,d,e,f} ==> P x ) <=>
  P a /\ P b /\ P c /\ P d /\ P e /\ P f `; delta] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN SIMP_TAC[SET_RULE ` 
{v1, v2, w1, w2} = {v1, w1, v2, w2} `; packing] THEN 
SIMP_TAC[CARD4; GSYM dist3] THEN SET_TAC[]);;
let LEOF41 = 
prove(
`#3.114467 < x ==> delta (#2.51 pow 2) (&2 pow 2) (&2 pow 2) (&2 pow 2)
 (&2 pow 2) (x pow 2) < &0`,

NHANH (MESON[REAL_ARITH ` #3.114467 < x ==> &0 < #3.114467 /\ &0 < x `;
  LT_POW2_EQ_LT]` #3.114467 < x ==> ( #3.114467 ) pow 2 < x pow 2 `) THEN 
REWRITE_TAC[delta] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN 
REWRITE_TAC[ REAL_POLY_CONV ` -- &126002 / &625 - &4 * &4 * x pow 2 - &4 * &4 * x pow 2 +
     &63001 / &10000 *     x pow 2 *
     (-- &63001 / &10000 + &4 + &4 + &4 + &4 - x pow 2) +
     &4 * &4 * (&23001 / &10000 + &4 + &0 + x pow 2) +
     &4 * &4 * (&63001 / &10000 + -- &4 + &4 + x pow 2) `] THEN 
REWRITE_TAC[REAL_ARITH ` a pow 4 = a pow 2 pow 2 `] THEN 
REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x = ( a * x + b ) * x `] THEN 
NHANH (REAL_ARITH `&9699904694089 / &1000000000000 < x pow 2
     ==> -- &63001 / &10000 * x pow 2 + &6111033999 / &100000000 < &0` ) THEN 
NHANH (REAL_ARITH `&9699904694089 / &1000000000000 < x ==> &0 < x `) THEN 
REWRITE_TAC[REAL_ARITH ` a < &0 <=> &0 < -- a `;
  REAL_ARITH ` -- ( a * b ) = -- a * b `] THEN MESON_TAC[REAL_LT_MUL]);;

let LEMMA41 = 
prove(`! v1 v2 v3 (v4:real^3).
 CARD {v1,v2,v3,v4} = 4 /\ 
 dist3 v1 v2 = #2.51 /\
         dist3 v1 v3 = &2 /\
         dist3 v1 v4 = &2 /\
         dist3 v2 v3 = &2 /\
         dist3 v2 v4 = &2
         ==> dist3 v3 v4 <= #3.114467 `,

REPEAT GEN_TAC THEN MP_TAC LEMMA3 THEN LET_TR THEN 
REWRITE_TAC[REAL_ARITH ` x <= #3.114467 <=> ~ (#3.114467 < x ) `] THEN 
REWRITE_TAC[REAL_ARITH ` x <= #3.114467 <=> ~ (#3.114467 < x ) `;
   MESON[]` a ==> ~ b <=> a /\ b ==> F `] THEN PHA THEN 
NHANH (SPEC_ALL (prove(`! (v1:real^3) v2 v3 v4. dist3 v1 v2 = #2.51 /\
dist3 v1 v3 = &2 /\ dist3 v1 v4 = &2 /\ dist3 v2 v3 = &2 /\ dist3 v2 v4 = &2 /\ 
#3.114467 < dist3 v3 v4 ==> delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) 
(dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2)
 (dist (v3,v4) pow 2) < &0 `, SIMP_TAC[dist3] THEN MESON_TAC[LEOF41]))) THEN 
REWRITE_TAC[REAL_ARITH ` a < &0 <=> ~( &0 <= a ) `; dist3] THEN MESON_TAC[]);;
let YXWIPMH = LEMMA41;;

let LEMMA_OF_L42 = 
prove(`sqrt8 <= dist3 v2 v4 /\ #3.488 <= x
 ==> -- &1 * x pow 2 * dist3 v2 v4 pow 2 +
     -- &1 * x pow 4 +
     &103001 / &5000 * x pow 2 +
     -- &529046001 / &100000000 <
     &0`,

MP_TAC SQRT8_LE THEN 
IMP_IMP_TAC THEN 
NHANH (MESON[REAL_ARITH ` &0 <= a /\ a <= b /\ #3.488 <= x ==> &0 <= b /\
  &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
  &0 <= a /\ a <= b /\ #3.488 <= x ==> a pow 2 <= b pow 2 /\
  #3.488 pow 2 <= x pow 2 `) THEN 
REWRITE_TAC[SQRT8_POW2; sqrt8] THEN 
NHANH (MESON[REAL_ARITH ` &0 <= a /\ a <= b /\ #3.488 <= x ==> &0 <= b /\
  &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
  &0 <= a /\ a <= b /\ #3.488 <= x ==> a pow 2 <= b pow 2 /\
  #3.488 pow 2 <= x pow 2 `) THEN 
REWRITE_TAC[SQRT8_POW2] THEN 
NHANH (MESON[REAL_ARITH ` &0 <= &8 /\ &0 <= #3.488 pow 2 `; REAL_LE_MUL2]` &8 <= a /\
 #3.488 pow 2 <= b ==> &8 * #3.488 pow 2 <= a * b `) THEN 
REWRITE_TAC[REAL_ARITH` a pow 4 = a pow 2 pow 2 `] THEN 
NHANH (MESON[REAL_ARITH ` #3.488 pow 2 <= x ==> &0 <= #3.488 pow 2 /\
  &0 <= x `; POW2_COND]` #3.488 pow 2 <= x ==> #3.488 pow 2 pow 2 <= x pow 2 `) THEN 
REWRITE_TAC[REAL_ARITH ` a + -- &1 * x pow 2 + b * x + c =
  a + -- &1 * ( x pow 2 + -- b * x + -- c ) `] THEN 
NHANH (prove(` #3.488 pow 2 <= x pow 2 ==>
  #3.488 pow 2 pow 2 +
      --(&103001 / &5000) * #3.488 pow 2 +
      --(-- &529046001 / &100000000) <= x pow 2 pow 2 +
      --(&103001 / &5000) * x pow 2 +
      --(-- &529046001 / &100000000) `,
MP_TAC (REAL_ARITH ` -- (  --(&103001 / &5000))  / &2 <= #3.488 pow 2 `) THEN 
MESON_TAC[GREATER_THAN_MID_QUADRATIC_PO ])) THEN 
REAL_ARITH_TAC);;


let LEMMA_IN_LEMMA42_P25 = 
prove(` ! v1 v2 v3 v4 x. 
            dist3 v1 v2 = #2.51 /\
            dist3 v1 v4 = #2.51 /\
            dist3 v2 v3 = &2 /\
            dist3 v3 v4 = &2 /\
            sqrt8 <= dist3 v2 v4 /\
            #3.488 <= x
==>   delta (dist3 v1 v2 pow 2) ( x pow 2) (dist3 v1 v4 pow 2)
      (dist3 v2 v3 pow 2)
      (dist3 v2 v4 pow 2)
      (dist3 v3 v4 pow 2) < &0 `,

SIMP_TAC[] THEN 
NHANH (MESON[REAL_ARITH` #3.488 <= x ==> &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
  #3.488 <= x ==> (#3.488 pow 2 <= x pow 2 ) `) THEN 
REWRITE_TAC[delta] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
REWRITE_TAC[REAL_POLY_CONV `--(&63001 / &10000 * x pow 2 * &4) -
         &63001 / &10000 * &63001 / &10000 * dist3 v2 v4 pow 2 -
         x pow 2 * &63001 / &2500 -
         &4 * dist3 v2 v4 pow 2 * &4 +
         &63001 / &10000 *
         &4 *
         (-- &63001 / &10000 +
          x pow 2 +
          &63001 / &10000 +
          &4 +
          dist3 v2 v4 pow 2 - &4) +
         x pow 2 *
         dist3 v2 v4 pow 2 *
         (&63001 / &10000 - x pow 2 +
          &63001 / &10000 +
          &4 - dist3 v2 v4 pow 2 +
          &4) +
         &63001 / &10000 *
         &4 *
         (&63001 / &10000 +
          x pow 2 - &63001 / &10000 - &4 +
          dist3 v2 v4 pow 2 +
          &4) `] THEN 
REWRITE_TAC[REAL_IDEAL_CONV [` y pow 2 `] `-- &1 * x pow 4 * y pow 2 +
         -- &1 * x pow 2 * y pow 4 +
         &103001 / &5000 * x pow 2 * y pow 2 +
         -- &529046001 / &100000000 * y pow 2 `] THEN 
REWRITE_TAC[MESON[]` a/\ #3.488 <= x /\ c <=> (a/\ #3.488 <= x )/\ c`] THEN 
NHANH (LEMMA_OF_L42) THEN 
REWRITE_TAC[sqrt8] THEN 
NHANH (SQRT8_LE_EQ_8_LESS_POW2) THEN 
REPEAT GEN_TAC THEN 
STRIP_TAC THEN 
UNDISCH_TAC ` &8 <= dist3 v2 v4 pow 2 ` THEN 
UNDISCH_TAC ` -- &1 * x pow 2 * dist3 v2 v4 pow 2 +
      -- &1 * x pow 4 +
      &103001 / &5000 * x pow 2 +
      -- &529046001 / &100000000 <
      &0 ` THEN 
ABBREV_TAC ` xx = (-- &1 * x pow 2 * dist3 v2 v4 pow 2 +
      -- &1 * x pow 4 +
      &103001 / &5000 * x pow 2 +
      -- &529046001 / &100000000)` THEN 
NHANH (REAL_ARITH ` &8 <= a ==> &0 < a `) THEN 
REWRITE_TAC[REAL_ARITH ` ( a * b < &0 <=> &0 < ( -- a ) * b )/\
  ( a < &0 <=> &0 < -- a )`] THEN 
SIMP_TAC[REAL_LT_MUL]);;
let PAATDXJ =
prove(` ! v1 v2 v3 (v4:real^3).
         CARD {v1,v2,v3,v4} = 4 /\ 
         dist3 v1 v2 = #2.51 /\
         dist3 v1 v4 = #2.51 /\
         dist3 v2 v3 = &2 /\
         dist3 v3 v4 = &2 /\
         sqrt8 <= dist3 v2 v4
         ==> dist3 v1 v3 < #3.488 `,

MP_TAC LEMMA3 THEN LET_TR THEN REWRITE_TAC[REAL_ARITH ` a < b <=> ~ ( b <= a )`]
THEN REWRITE_TAC[MESON[]` a ==> ~ b <=> ~( a /\b)`] THEN 
PHA THEN NHANH (SPEC_ALL LEMMA_IN_LEMMA42_P25) THEN 
REWRITE_TAC[REAL_ARITH` a < b <=> ~(b <= a ) `] THEN SIMP_TAC[dist3]);;

let CONVEX_NORMBALL = REWRITE_RULE[GSYM NORMBALL_BALL] CONVEX_BALL ;;

let CONVEX_HULL4 = 
SPEC `{(v1:real^N),v2,v3,v4}` CONVEX_HULL_FINITE;;

let CONVEX_HULL_4_EQUIV = 
prove(` ! v1 v2 v3 (v4:real^N).
  conv {v1,v2,v3,v4} = { x | ? a b c d. 
  &0 <= a /\
          &0 <= b /\
          &0 <= c /\
          &0 <= d /\
          a + b + c + d = &1 /\
          a % v1 + b % v2 + c % v3 + d % v4 = x } `,

REWRITE_TAC[conv; FUN_EQ_THM; affsign; lin_combo; UNION_EMPTY; 
 IN_ELIM_THM; sgn_ge] THEN 
REWRITE_TAC[MESON[]` x = vsum aa bb /\ a /\ b <=>
  a /\ b /\ vsum aa bb = x `] THEN 
ONCE_REWRITE_TAC[SET_RULE ` a s ==> b <=> s IN a ==> b `] THEN 
 SIMP_TAC[CONVEX_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
 REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
             VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
 REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[IN]);;

let TXDIACY = 
prove(`! (a:real^3) b c d (v0: real^3) r.
 {a, b, c, d} SUBSET normball v0 r
         ==> convex hull {a, b, c, d} SUBSET normball v0 r `,

REPEAT GEN_TAC THEN MP_TAC (MESON[CONVEX_NORMBALL]` convex (normball (v0:real^3) r)`) THEN 
NHANH (MESON[FINITE6] ` {a, b, c, d} SUBSET s ==> FINITE {(a:real^3),b,c,d} `) THEN 
REWRITE_TAC[CONVEX_HULL4; CONVEX_EXPLICIT] THEN 
IMP_IMP_TAC THEN 
REWRITE_TAC[SET_RULE ` {a | P a } SUBSET b <=> (! a. P a ==> a IN b)`] THEN 
REWRITE_TAC[MESON[]` (! y. ( ? u. P u y ) ==> Q y ) <=>
  (! y u. P u y ==> Q y ) `] THEN 
REWRITE_TAC[MESON[]`(!y u. P u /\ Q u /\ R u = y ==> Z y) <=> 
  (!u. P u /\ Q u ==> Z (R u)) `] THEN MESON_TAC[]);;
let LEMMA14 = TXDIACY;;


let ECSEVNC = 
prove(`?t1 t2 t3 t4.
     !v1 v2 v3 v4 (v: real^3).
         ~coplanar_alt {v1, v2, v3, v4}
         ==> t1 v1 v2 v3 v4 v +
             t2 v1 v2 v3 v4 v +
             t3 v1 v2 v3 v4 v +
             t4 v1 v2 v3 v4 v =
             &1 /\
             v =
             t1 v1 v2 v3 v4 v % v1 +
             t2 v1 v2 v3 v4 v % v2 +
             t3 v1 v2 v3 v4 v % v3 +
             t4 v1 v2 v3 v4 v % v4 /\
             (!ta tb tc td.
                  v = ta % v1 + tb % v2 + tc % v3 + td % v4 /\
                  ta + tb + tc + td = &1
                  ==> ta = t1 v1 v2 v3 v4 v /\
                      tb = t2 v1 v2 v3 v4 v /\
                      tc = t3 v1 v2 v3 v4 v /\
                      td = t4 v1 v2 v3 v4 v) `,

REWRITE_TAC[GSYM SKOLEM_THM; RIGHT_EXISTS_IMP_THM] THEN REPEAT 
GEN_TAC THEN NHANH (SPEC_ALL (prove(`!v1 v2 v3 v0 v:real^3.
    ~coplanar_alt {v0, v1, v2, v3} ==> (?t1 t2 t3. v - v0 = t1 % (v1 - v0)
 + t2 % (v2 - v0) + t3 % (v3 - v0) /\ (!ta tb tc. v - v0 = ta % (v1 - v0)
 + tb % (v2 - v0) + tc % (v3 - v0)   ==> ta = t1 /\
 tb = t2 /\ tc = t3))`, SIMP_TAC[NONCOPLANAR_3_BASIS]))) THEN 
STRIP_TAC THEN EXISTS_TAC ` &1 - t1 - t2 - t3 ` THEN 
EXISTS_TAC ` t1:real ` THEN EXISTS_TAC ` t2:real ` THEN 
EXISTS_TAC ` t3:real ` THEN CONJ_TAC THENL [REAL_ARITH_TAC;
 CONJ_TAC] THENL [UNDISCH_TAC ` (v:real^3) - v1 = t1 % (v2 - v1) + 
t2 % (v3 - v1) + t3 % (v4 - v1)` THEN 
CONV_TAC VECTOR_ARITH; REPEAT GEN_TAC] THEN 
REWRITE_TAC[MESON[]` a /\ b ==> c <=> b ==> a ==> c `;
  REAL_ARITH ` ta + tb + tc + td = &1 <=> ta = &1 - tb - tc - td `] THEN 
SIMP_TAC[] THEN REWRITE_TAC[VECTOR_ARITH `   v = (&1 - tb - tc - td) % v1
 + tb % v2 + tc % v3 + td % v4 <=>  v - v1 = tb % ( v2 - v1 ) + 
tc % ( v3 - v1 ) + td % ( v4 - v1 ) `] THEN ASM_MESON_TAC[]);;
let LEMMA76 = ECSEVNC;;

let COEFS_4 = new_specification ["COEF4_1";
 "COEF4_2"; "COEF4_3"; "COEF4_4"] ECSEVNC ;;

let COEF_1_EQ_ZERO = 
prove(` ! v1 v2 v3 v4 (v:real^3).
  ~ coplanar_alt {v1,v2,v3,v4} ==>
  ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) `,

REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN 
NHANH (SPEC_ALL COEFS_4) THEN 
REPEAT GEN_TAC THEN STRIP_TAC THEN 
ONCE_REWRITE_TAC[REAL_ARITH` u + v + w = &0 + u + v + w `] THEN 
ONCE_REWRITE_TAC[VECTOR_ARITH` u + v + w = &0 % v1 + u + v + w `] THEN 
ASM_MESON_TAC[]);;
let EQ_IMP_COPLANAR = 
prove(`! a b c (d:real^3). ( a = b \/ a = c \/ a = d )
 ==> coplanar_alt {a,b,c,d} `,

REPEAT STRIP_TAC THENL [
ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN 
MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3;  ARITH_RULE` a = 3 ==> 2 <= a `];
ONCE_REWRITE_TAC[SET_RULE` {a,b,v,c} = {a,v,b,c} `] THEN 
ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN 
MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3;  ARITH_RULE` a = 3 ==> 2 <= a `];
ONCE_REWRITE_TAC[SET_RULE` {a,b,v,c} = {a,c,v,b} `] THEN 
ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN 
MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3;  ARITH_RULE` a = 3 ==> 2 <= a `]]);;
let AFFINE_HULL_FINITE_STEP_GEN = 
prove
 (`!P:real^N->real->bool.
       ((?u. (!x. x IN {} ==> P x (u x)) /\
             sum {} u = w /\ vsum {} (\x. u(x) % x) = y) <=>
        w = &0 /\ y = vec 0) /\
       (FINITE(s:real^N->bool) /\
        (!y. a IN s /\ P a y ==> P a (y / &2)) /\
        (!x y. a IN s /\ P a x /\ P a y ==> P a (x + y))
        ==> ((?u. (!x. x IN (a INSERT s) ==> P x (u x)) /\
                  sum (a INSERT s) u = w /\
                  vsum (a INSERT s) (\x. u(x) % x) = y) <=>
             ?v u. P a v /\ (!x. x IN s ==> P x (u x)) /\
                   sum s u = w - v /\
                   vsum s (\x. u(x) % x) = y - v % a))`,

 GEN_TAC THEN SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; NOT_IN_EMPTY] THEN
 CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN
 ASM_CASES_TAC `(a:real^N) IN s` THEN ASM_REWRITE_TAC[] THENL
  [ASM_SIMP_TAC[SET_RULE `a IN s ==> a INSERT s = s`] THEN EQ_TAC THEN
   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
    [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN
     EXISTS_TAC `(u:real^N->real) a / &2` THEN
     EXISTS_TAC `\x:real^N. if x = a then u x / &2 else u x`;
     MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->real`] THEN
     STRIP_TAC THEN
     EXISTS_TAC `\x:real^N. if x = a then u x + v else u x`] THEN
   ASM_SIMP_TAC[] THEN (CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]) THEN
   ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
   ASM_SIMP_TAC[VSUM_CASES; SUM_CASES] THEN
   ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE; VSUM_DELETE] THEN
   ASM_SIMP_TAC[SET_RULE `a IN s ==> {x | x IN s /\ x = a} = {a}`] THEN
   REWRITE_TAC[SUM_SING; VSUM_SING] THEN
   (CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]);
   EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
    [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN
     EXISTS_TAC `(u:real^N->real) a` THEN
     EXISTS_TAC `u:real^N->real` THEN ASM_SIMP_TAC[IN_INSERT] THEN
     REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
     CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC];
     MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->real`] THEN
     STRIP_TAC THEN
     EXISTS_TAC `\x:real^N. if x = a then v:real else u x` THEN
     ASM_SIMP_TAC[IN_INSERT] THEN CONJ_TAC THENL
      [ASM_MESON_TAC[]; ALL_TAC] THEN
     ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
     ASM_SIMP_TAC[VSUM_CASES; SUM_CASES] THEN
     ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE; VSUM_DELETE] THEN
     ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> {x | x IN s /\ x = a} = {}`] THEN
     ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> s DELETE a = s`] THEN
     REWRITE_TAC[SUM_CLAUSES; VSUM_CLAUSES] THEN
     CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]]]);;


let THEOREM_RE_AFF_LT31 = 
prove
 (`!v1 v2 v3 vv x:real^N.
       ~(v1 = vv) /\ ~(v2 = vv) /\ ~(v3 = vv)
       ==> ((?f. f vv < &0 /\
                 sum {v1, v2, v3, vv} f = &1 /\
                 x = vsum {v1, v2, v3, vv} (\v. f v % v)) <=>
            {x | ?a b c t.
                     a + b + c + t = &1 /\
                     x = a % v1 + b % v2 + c % v3 + t % vv /\
                     t < &0}
            x)`,

 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 EXISTS_TAC
  `?f. (!x:real^N. x IN {v1, v2, v3, vv} ==> vv = x ==> f x < &0) /\
       sum {v1, v2, v3, vv} f = &1 /\
       vsum {v1, v2, v3, vv} (\v. f v % v) = x` THEN
 CONJ_TAC THENL
  [ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[];
   SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
            REAL_ARITH `x < &0 /\ y < &0 ==> x + y < &0`;
            REAL_ARITH `x < &0 ==> x / &2 < &0`;
            FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
   ASM_REWRITE_TAC[IN_ELIM_THM;
                   REAL_ARITH `x - y:real = z <=> x = y + z`;
                   VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
   REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]]);;
let AFF_LT31 = 
prove(` ! v1 v2 v3 (vv: real^N). ~ (vv IN {v1,v2,v3} ) ==>
aff_lt {v1,v2,v3} {vv} = 
   { x| ? a b c t. t < &0 /\ a + b + c + t = &1 /\
           x = a % v1 + b % v2 + c % v3 + t % vv } `,

REWRITE_TAC[IN_SET3; DE_MORGAN_THM; aff_lt_def;FUN_EQ_THM; 
 affsign; lin_combo; sgn_lt] THEN 
REWRITE_TAC[SET_RULE` {v1, v2, v3} UNION {vv} = {v1, v2, v3, vv}`] THEN 
REWRITE_TAC[SET_RULE` a /\ (!w. {vv} w ==> f w < &0) /\ b
  <=> f vv < &0 /\ b /\ a `] THEN 
SIMP_TAC[THEOREM_RE_AFF_LT31; IN_ELIM_THM] THEN SET_TAC[]);;
let AFF_LT21 = 
prove(`! a b (v0:real^N). ~ ( a = v0 ) /\ ~( b = v0 ) ==>
aff_lt {a,b} {v0} =
          {x | ? ta tb t.
                   ta + tb + t = &1 /\
                   t < &0 /\
                   x = ta % a + tb % b + t % v0} `,

REWRITE_TAC[SET_RULE` ~(a = v0) /\ ~(b = v0) <=>
  ~ ( v0 IN {a,b} ) `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {a,b} = {a,b,b} `] THEN SIMP_TAC[AFF_LT31] THEN 
SIMP_TAC[AFF_LT31; FUN_EQ_THM; IN_ELIM_THM] THEN 
REWRITE_TAC[VECTOR_ARITH` a % b + c % b + x = ( a + c ) % b + x `] THEN 
MESON_TAC[REAL_ARITH` a + b + c = ( a + b ) + c `;
VECTOR_ARITH ` a % v = ( a + &0 ) % v `; REAL_ARITH `
   a + b = a + &0 + b `]);;

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

let AFF_GT33 = 
prove(`! (v1:real^N) v2 v3 w1 w2 w3.
     {v1, v2, v3} INTER {w1, w2, w3} = {}
     ==> aff_gt {v1, v2, v3} {w1, w2, w3} =
         {x | ?a1 a2 a3 b1 b2 b3.
                  &0 < b1 /\
                  &0 < b2 /\
                  &0 < b3 /\
                  a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
                  x =
                  a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3}`,

REWRITE_TAC[aff_gt_def; FUN_EQ_THM; affsign; lin_combo; sgn_gt] THEN 
REPEAT STRIP_TAC THEN 
MATCH_MP_TAC EQ_TRANS  THEN 
REWRITE_TAC[SET_RULE ` ( a INSERT b ) UNION c =
   b UNION ( a INSERT c ) /\ {} UNION b = b `] THEN 
EXISTS_TAC ` (? f. x = vsum {v3, v2, v1, w1, w2, w3} (\v. f v % v) /\
           (!(w:real^N). w IN {v3,v2,v1, w1, w2, w3} ==> w IN {w1,w2,w3} ==>  &0 < f w) /\
           sum {v3, v2, v1, w1, w2, w3} f = &1 ) ` THEN 
REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
  <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `] THEN 
CONJ_TAC THENL [ 
FIRST_X_ASSUM MP_TAC THEN 
REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
  <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `] THEN 
MESON_TAC[SET_RULE` {v1, v2, v3} INTER {w1, w2, w3} = {} ==>
  ( (!w. {w1, w2, w3} w ==> &0 < f w) <=>
  (!w. w IN {v3, v2, v1, w1, w2, w3}
                ==> w IN {w1, w2, w3}
                ==> &0 < f w) ) `];
REWRITE_TAC[MESON[]` a /\ (!z. P z ) /\ aa = &1 <=>
  (!z. P z ) /\ aa = &1 /\ a `]] THEN 
ONCE_REWRITE_TAC[MESON[]` a = vsum b c <=> vsum b c = a `] THEN 
 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;FINITE_INSERT; CONJUNCT1 FINITE_RULES;
            RIGHT_EXISTS_AND_THM;
            REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
            REAL_ARITH `&0 < x  ==> &0 < x / &2 `] THEN 
FIRST_X_ASSUM MP_TAC THEN 
REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
  <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `; SET_RULE` ( a INSERT s ) INTER ss = {} <=>
~ ( a IN ss ) /\ s INTER ss = {} `] THEN 
SIMP_TAC[INSET3] THEN 
SIMP_TAC[INSET3; REAL_ARITH` a - b = c <=> a = b + c `;
  VECTOR_ARITH` a:real^N - b = c <=> a = b + c `] THEN 
REWRITE_TAC[ GSYM  RIGHT_EXISTS_AND_THM; ZERO_NEUTRAL; 
 IN_ELIM_THM; VECTOR_ARITH ` a + vec 0 = a `] THEN 
DISCH_TAC THEN 
MESON_TAC[REAL_ARITH` a + b + c + d = c + b + a + d `;
  VECTOR_ARITH` ( a:real^N ) + b + c + d = c + b + a + d `]);;
let AFF_GE33 = 
prove_by_refinement(
`! (v1:real^N) v2 v3 w1 w2 w3.
     {v1, v2, v3} INTER {w1, w2, w3} = {}
     ==> aff_ge {v1, v2, v3} {w1, w2, w3} =
         {x | ?a1 a2 a3 b1 b2 b3.
                  &0 <= b1 /\
                  &0 <= b2 /\
                  &0 <= b3 /\
                  a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
                  x =
                  a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3}`,

  (* {{{ proof *)
  [
  (REWRITE_TAC[aff_gt_def; aff_ge_def; FUN_EQ_THM; affsign; lin_combo; sgn_gt; sgn_ge]);
  (REPEAT STRIP_TAC);
  (MATCH_MP_TAC EQ_TRANS );
  (REWRITE_TAC[SET_RULE ` ( a INSERT b ) UNION c =   b UNION ( a INSERT c ) /\ {} UNION b = b `]);
  (EXISTS_TAC ` (? f. x = vsum {v3, v2, v1, w1, w2, w3} (\v. f v % v) /\           (!(w:real^N). w IN {v3,v2,v1, w1, w2, w3} ==> w IN {w1,w2,w3} ==>  &0 <= f w) /\           sum {v3, v2, v1, w1, w2, w3} f = &1 ) `);
  (CONJ_TAC);
    (FIRST_X_ASSUM MP_TAC);
    (REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)  <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `]);
    BY((MESON_TAC[SET_RULE` {v1, v2, v3} INTER {w1, w2, w3} = {} ==>  ( (!w. {w1, w2, w3} w ==> &0 <= f w) <=>  (!w. w IN {v3, v2, v1, w1, w2, w3}                ==> w IN {w1, w2, w3}                ==> &0 <= f w) ) `]));
  (REWRITE_TAC[MESON[]` a /\ (!z. P z ) /\ aa = &1 <=>  (!z. P z ) /\ aa = &1 /\ a `]);
  (ONCE_REWRITE_TAC[MESON[]` a = vsum b c <=> vsum b c = a `]);
  ( SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM; REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 <= x + y`; REAL_ARITH `&0 <= x  ==> &0 <= x / &2 `]);
  (FIRST_X_ASSUM MP_TAC);
  (REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)  <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `; SET_RULE` ( a INSERT s ) INTER ss = {} <=> ~ ( a IN ss ) /\ s INTER ss = {} `]);
   (SIMP_TAC[INSET3]);
   (SIMP_TAC[INSET3; REAL_ARITH` a - b = c <=> a = b + c `; VECTOR_ARITH` a:real^N - b = c <=> a = b + c `]);
   (REWRITE_TAC[ GSYM RIGHT_EXISTS_AND_THM; ZERO_NEUTRAL; IN_ELIM_THM; VECTOR_ARITH ` a + vec 0 = a `]);
   (DISCH_TAC);
  BY( (MESON_TAC[REAL_ARITH` a + b + c + d = c + b + a + d `; VECTOR_ARITH` ( a:real^N ) + b + c + d = c + b + a + d `]))
  ]);;
  (* }}} *)


let AFF_GE_12 = 
prove(`!v0 (a:real^N) b.
     ~(v0 = a \/ v0 = b)
     ==> aff_ge {v0} {a, b} =
         {x | ?tv ta tb.
                  &0 <= ta /\
                  &0 <= tb /\
                  tv + ta + tb = &1 /\
                  x = tv % v0 + ta % a + tb % b}`,

REWRITE_TAC[SET_RULE ` ~(v0 = a \/ v0 = b) <=> {v0} INTER {a,b} = {} `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {a} = {a,a} `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {a,a} = {a,a,a} `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {a,b,b,b} = {a,b,b} `] THEN 
SIMP_TAC[AFF_GE33] THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN 
REPEAT STRIP_TAC THEN 
REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_ARITH` a % v + 
  b % v + y = ( a + b ) % v + y `] THEN GONTONG THEN EQ_TAC THENL [
MESON_TAC[REAL_ARITH` a1 + a2 + a3 + b1 + b2 + b3 =
  ( a1 + a2 + a3 ) + b1 + b2 + b3 `; REAL_ARITH ` &0 <= a 
/\ &0 <= b ==> &0 <= a + b `];STRIP_TAC] THEN EXISTS_TAC` tv: real ` 
THEN EXISTS_TAC` &0 ` THEN EXISTS_TAC` &0` THEN EXISTS_TAC` ta :real `
 THEN EXISTS_TAC` &0` THEN EXISTS_TAC` tb:real ` THEN 
ASM_SIMP_TAC[REAL_ARITH ` a <= a `; ZERO_NEUTRAL]);;

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



let AFF_LE_LT33 = 
prove(`! (v1:real^N) v2 v3 w1 w2 w3.
     {v1, v2, v3} INTER {w1, w2, w3} = {}
     ==> aff_le {v1, v2, v3} {w1, w2, w3} =
         {x | ?a1 a2 a3 b1 b2 b3.
                  b1 <= &0 /\
                  b2 <= &0  /\
                  b3 <= &0  /\
                  a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
                  x =
                  a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3} /\
   aff_lt {v1, v2, v3} {w1, w2, w3} =
         {x | ?a1 a2 a3 b1 b2 b3.
                  b1 < &0 /\
                  b2 < &0  /\
                  b3 < &0  /\
                  a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
                  x =
                  a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3} `,

REWRITE_TAC[IN_ELIM_THM; aff_le_def; FUN_EQ_THM; aff_lt_def; 
 affsign; lin_combo; sgn_lt; sgn_le] THEN 
REWRITE_TAC[SET_RULE` {v1, v2, v3} UNION {w1, w2, w3} = 
  {v1,v2,v3,w1,w2,w3} `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {w1, w2, w3} w ==> P w <=>
  w IN {v1,v2,v3,w1,w2,w3} ==> {w1,w2,w3} w ==> P w `] THEN 
REWRITE_TAC[MESON[]` a = vsum aa bb /\
  (! w. P w ) /\ b <=> (! w. P w ) /\ b /\ vsum aa bb = a `] THEN 
 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
            REAL_ARITH `( x < &0 /\ y < &0 ==> x + y < &0) /\ ( x <= &0 /\ y <= &0 ==> x + y <= &0)`;
            REAL_ARITH ` (x < &0 ==> x / &2 < &0 ) /\ (x <= &0 ==> x / &2 <= &0 )`;
            FINITE_INSERT; CONJUNCT1 FINITE_RULES
; RIGHT_EXISTS_AND_THM]  THEN 
SIMP_TAC[ GSYM RIGHT_EXISTS_AND_THM; SET_RULE ` 
  (!x. ({v1, v2, v3} INTER s ) x <=> {} x) <=>
  ~ ( s v1 ) /\ ~ ( s v2 ) /\ ~ ( s v3 ) `; INSET3] THEN 
REWRITE_TAC[REAL_ARITH` a - b = c <=> a = b + c`; REAL_ARITH `
  a + &0 = a `; VECTOR_ARITH` (a:real^N) - b = c <=> a = b + c`;
  VECTOR_ARITH` a + vec 0 = a `] THEN 
MESON_TAC[]);;



let AFF_GES_LTS = 
prove(` ! a b c (v0 :real^N). 
 ~ ( a = v0 ) /\ ~( b = v0 ) /\ ~( c = v0 ) ==>
aff_gt {a, b} {v0} =
          {x | ?ta tb t.
                   ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
aff_ge {a, b} {v0} =
          {x | ?ta tb t.
                   ta + tb + t = &1 /\
                   &0 <= t /\
                   x = ta % a + tb % b + t % v0} /\
aff_lt {a,b,c} {v0} = 
   { x| ? ta tb tc t. t < &0 /\ ta + tb + tc + t = &1 /\
           x = ta % a + tb % b + tc % c + t % v0 }  /\
aff_gt {a,b,c} {v0} =  
   { x| ? ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\
     x = ta % a + tb % b + tc % c + t % v0 } `,
 
ONCE_REWRITE_TAC[SET_RULE` {a} = {a,a,a} `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {a,b,b,b} = {a,b,b} `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {a,b,c,c} = {a,b,c} `] THEN 
NHANH (SET_RULE` ~(a = v0) /\ ~(b = v0) /\ ~(c = v0) ==>
  {a,b,b} INTER {v0,v0,v0} = {} /\ {a,b,c} INTER {v0,v0,v0} = {} `) THEN 
SIMP_TAC[AFF_LE_LT33; AFF_GE33; AFF_GT33] THEN 
REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_ARITH` a % x + b % x + y
  = ( a + b ) % x + y `] THEN 
REWRITE_TAC[REAL_ARITH` (a + b ) + c = a + b + c `] THEN 
REPEAT STRIP_TAC THENL [
REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN 
EQ_TAC THENL [MESON_TAC[REAL_ARITH ` &0 < a /\ &0 < b ==> &0 < a + b `;
  REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; 
MESON_TAC[REAL_ARITH ` a + b + c = a + b / &2 + b / &2 + c / &3 +
  c / &3 + c / &3 `; REAL_ARITH` &0 < a <=> &0 < a / &3 `;
  REAL_ARITH` a = a / &2 + a / &2 /\ b = b / &3 + b / &3 + b / &3 /\ b =
 ( b / &3 + b / &3 ) + b / &3  `]];
REPEAT STRIP_TAC THEN 
REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN 
EQ_TAC THENL [
MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b )  `;
  REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `] ; 
MESON_TAC[REAL_ARITH ` a + b + c = a + b / &2 + b / &2 + c / &3 +
  c / &3 + c / &3 `; REAL_ARITH` ( &0 < a <=> &0 < a / &3) /\ ( &0 <= a <=> &0 <= a / &3) `;
  REAL_ARITH` a = a / &2 + a / &2 /\ b = b / &3 + b / &3 + b / &3 /\ b = ( b / &3 + b / &3 ) + b / &3  `]];
REPEAT STRIP_TAC THEN 
REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN 
EQ_TAC THENL [MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) 
/\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b )  `; REAL_ARITH ` ( a < &0 /\ b < &0 
==> a + b < &0 )`; REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; STRIP_TAC] THEN 
EXISTS_TAC `ta :real` THEN 
EXISTS_TAC `tb :real` THEN 
EXISTS_TAC `tc :real` THEN 
REPEAT (EXISTS_TAC ` t / &3 `) THEN 
ASM_MESON_TAC[REAL_ARITH` a < &0 <=> a / &3 < &0 `;
  REAL_ARITH ` a = a / &3 + a / &3 + a / &3 `];
REPEAT STRIP_TAC THEN 
REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN 
EQ_TAC THENL [MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b
 ==> &0 <= a + b )  `; REAL_ARITH ` ( a < &0 /\ b < &0 ==> a + b < &0 )`;
  REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; STRIP_TAC] THEN 
EXISTS_TAC `ta :real` THEN 
EXISTS_TAC `tb :real` THEN 
EXISTS_TAC `tc :real` THEN 
REPEAT (EXISTS_TAC ` t / &3 `) THEN 
ASM_MESON_TAC[REAL_ARITH ` a = a / &3 + a / &3 + a / &3 `;
  REAL_ARITH ` &0 < a <=> &0 < a / &3 `]]);;

let AFF_GES_GTS = 
prove(` ! a b c (v0:real^N).
~(a = v0) /\ ~(b = v0) /\ ~(c = v0)
     ==> aff_gt {a, b} {v0} =
               {x | ?ta tb t.
                        ta + tb + t = &1 /\
                        &0 < t /\
                        x = ta % a + tb % b + t % v0} /\
               aff_ge {a, b} {v0} =
               {x | ?ta tb t.
                        ta + tb + t = &1 /\
                        &0 <= t /\
                        x = ta % a + tb % b + t % v0} /\
               aff_lt {a, b, c} {v0} =
               {x | ?ta tb tc t.
                        t < &0 /\
                        ta + tb + tc + t = &1 /\
                        x = ta % a + tb % b + tc % c + t % v0} /\
               aff_gt {a, b, c} {v0} =
               {x | ?ta tb tc t.
                        &0 < t /\
                        ta + tb + tc + t = &1 /\
                        x = ta % a + tb % b + tc % c + t % v0} /\
         aff_ge {a, b, c} {v0} =
         {x | ?ta tb tc t.
                  &0 <= t /\
                  ta + tb + tc + t = &1 /\
                  x = ta % a + tb % b + tc % c + t % v0} `,

REPEAT GEN_TAC THEN 
REWRITE_TAC[MESON[]` (a ==> a1 /\ a2 /\ a3 /\ a4 /\ a5) <=>
  ( a ==> a1 /\ a2 /\ a3 /\a4 ) /\ ( a ==> a5) `] THEN 
REWRITE_TAC[AFF_GES_LTS] THEN 
NHANH (SET_RULE` ~(a = v0) /\ ~(b = v0) /\ ~(c = v0) 
  ==> {a,b,c} INTER {v0,v0,v0} = {} `) THEN 
ONCE_REWRITE_TAC[SET_RULE` {v} = {v,v,v} `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {a, b, c, c, c} = {a,b,c} `] THEN 
SIMP_TAC[AFF_GE33] THEN 
REPEAT STRIP_TAC THEN 
REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; GSYM VECTOR_ADD_RDISTRIB] THEN 
GEN_TAC THEN EQ_TAC THENL [ 
MESON_TAC[REAL_ARITH` &0 <= a /\ &0 <= b ==> &0 <= a + b `]; 
STRIP_TAC THEN 
EXISTS_TAC ` ta :real` THEN 
EXISTS_TAC ` tb :real` THEN 
EXISTS_TAC ` tc :real` THEN 
REPEAT ( EXISTS_TAC ` t / &3 `) THEN 
ASM_MESON_TAC[REAL_ARITH` a = a / &3 + a / &3 + a / &3 `;
  REAL_ARITH` &0 <= a <=> &0 <= a / &3 `]]);;

let COEF_1_POS_NEG = 
prove(` ! v1 v2 v3 v4 (v:real^3).
  ~ coplanar_alt {v1,v2,v3,v4} ==>
  ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\
( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) `,

NHANH (MESON[EQ_IMP_COPLANAR]`~coplanar_alt {v1, v2, v3, v4} ==>
  ~ ( v2 = v1 ) /\ ~ ((v3:real^3) = v1 ) /\ ~ (v4 = v1 ) `) THEN 
SIMP_TAC[AFF_GES_LTS] THEN NHANH (SPEC_ALL COEFS_4) THEN 
REWRITE_TAC[IN_ELIM_THM; REAL_ARITH ` a > b <=> b < a `] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN 
ONCE_REWRITE_TAC[REAL_ARITH ` a + b + c + t = t + a + b + c `] THEN 
ONCE_REWRITE_TAC[VECTOR_ARITH ` (a:real^N) + b + c + t = t + a + b + c `] THEN 
ASM_MESON_TAC[]);;

let ALL_ABOUT_COEF_1 = 
prove(` ! v1 v2 v3 v4 (v:real^3).
  ~ coplanar_alt {v1,v2,v3,v4} ==>
  ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\
  ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\
  ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} )`,

SIMP_TAC[COEF_1_EQ_ZERO ; COEF_1_POS_NEG ]);;
let PER_COEF1_WITH_COEF2 = 
prove(`! v1 v2 v3 v4 (v:real^3).
 ~coplanar_alt {v1, v2, v3, v4} ==>
   COEF4_2 v1 v2 v3 v4 v = COEF4_1 v2 v3 v4 v1 v `,

NHANH (SPEC_ALL COEFS_4) THEN 
REPEAT GEN_TAC THEN STRIP_TAC THEN 
MP_TAC (SPECL [` v2:real^3 `; `v3:real^3`; `v4:real^3`; ` v1:real^3`;
 `v:real^3 `] COEFS_4) THEN 
UNDISCH_TAC ` ~coplanar_alt {v1, v2, v3, (v4:real^3)}` THEN 
IMP_IMP_TAC THEN 
REWRITE_TAC[MESON[SET_RULE` {v1, v2, v3, v4} = {v2, v3, v4, v1}`]`
  ~coplanar_alt {v1, v2, v3, v4} /\
 (~coplanar_alt {v2, v3, v4, v1} ==> l ) <=> ~coplanar_alt {v1, v2, v3, v4}
  /\ l `] THEN 
ONCE_REWRITE_TAC[GSYM (REAL_ARITH` a + b + c + d = b + c + d + a `)] THEN 
ONCE_REWRITE_TAC[GSYM (VECTOR_ARITH` (a:real^N) + b + c + d = b + c + d + a `)] THEN 
ASM_MESON_TAC[]);;
let PER_COEF1_WITH_COEF3 = 
prove(`! v1 v2 v3 v4 (v:real^3).
 ~coplanar_alt {v1, v2, v3, v4} ==>
   COEF4_3 v1 v2 v3 v4 v = COEF4_1 v3 v4 v1 v2 v `,

NHANH (SPEC_ALL COEFS_4) THEN 
REPEAT GEN_TAC THEN STRIP_TAC THEN 
MP_TAC (SPECL [`v3:real^3`; `v4:real^3`; ` v1:real^3`; ` v2:real^3`;
 `v:real^3 `] COEFS_4) THEN 
UNDISCH_TAC ` ~coplanar_alt {v1, v2, v3, (v4:real^3)}` THEN 
IMP_IMP_TAC THEN 
REWRITE_TAC[MESON[SET_RULE` {v1, v2, v3, v4} = {v3, v4, v1, v2}`]`
  ~coplanar_alt {v1, v2, v3, v4} /\
 (~coplanar_alt {v3, v4, v1, v2} ==> l ) <=> ~coplanar_alt {v1, v2, v3, v4}
  /\ l `] THEN 
ONCE_REWRITE_TAC[GSYM (REAL_ARITH` a + b + c + d = c + d + a + b`)] THEN 
ONCE_REWRITE_TAC[GSYM (VECTOR_ARITH` (a:real^N) + b + c + d = c + d + a + b`)]
 THEN ASM_MESON_TAC[]);;
let PER_COEF1_WITH_COEF4 = 
prove(`! v1 v2 v3 v4 (v:real^3).
 ~coplanar_alt {v1, v2, v3, v4} ==>
   COEF4_4 v1 v2 v3 v4 v = COEF4_1 v4 v1 v2 v3 v `,

NHANH (SPEC_ALL COEFS_4) THEN 
REPEAT GEN_TAC THEN 
ONCE_REWRITE_TAC[SET_RULE` {v1, v2, v3, v4} = {v4,v1, v2, v3}`] THEN 
NHANH (SPEC_ALL COEFS_4) THEN 
MESON_TAC[REAL_ARITH` ta + tb + tc + td = td + ta + tb + tc`;
  VECTOR_ARITH` ta + tb + tc + td = td + ta + tb + (tc:real^N)`]);;
let ALL_ABOUT_COEF_2 = 
prove(` ! v1 v2 v3 v4 (v:real^3).
  ~ coplanar_alt {v1,v2,v3,v4} ==>
  ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\
  ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\
  ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} )`,

SIMP_TAC[PER_COEF1_WITH_COEF2] THEN MP_TAC ALL_ABOUT_COEF_1 THEN 
MESON_TAC[SET_RULE` {v1, v2, v3, v4} = {v2, v3, v4, v1}`;
SET_RULE` {v1, v2, v3} = {v2, v3,v1}`]);;



let ALL_ABOUT_COEF_3 = 
prove(` ! v1 v2 v3 v4 (v:real^3).
  ~ coplanar_alt {v1,v2,v3,v4} ==>
  ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\
  ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\
  ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} ) `,

SIMP_TAC[PER_COEF1_WITH_COEF3] THEN 
ONCE_REWRITE_TAC[SET_RULE` {v2, v1, v4} = {v4,v1,v2} `] THEN 
ONCE_REWRITE_TAC[SET_RULE` {v1, v4, v3, v2} = {v3,v4,v1,v2} `] THEN 
SIMP_TAC[ALL_ABOUT_COEF_1]);;
let SRGTIHY = 
prove(` ! v1 v2 v3 v4 (v:real^3).
  ~ coplanar_alt {v1,v2,v3,v4} ==>
  ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\
  ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\
  ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\
  ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\
  ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\
  ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} ) /\  
  ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\
  ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\
  ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} )/\  
  ( COEF4_4 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v3} {v4} ) /\
  ( COEF4_4 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v3} ) /\
  ( COEF4_4 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v3} {v4} )`,

SIMP_TAC[ALL_ABOUT_COEF_1; ALL_ABOUT_COEF_2; ALL_ABOUT_COEF_3;
  PER_COEF1_WITH_COEF4] THEN 
ONCE_REWRITE_TAC[SET_RULE` {v2, v1, v3} = {v1,v2,v3}`] THEN 
ONCE_REWRITE_TAC[SET_RULE` {v1, v3, v2, v4} = {v4,v1,v2,v3}`] THEN 
SIMP_TAC[ALL_ABOUT_COEF_1]);;
let LEMMA77 = SRGTIHY;;


 
let CONV0_4 = 
prove
  (`conv0 {v1, v2, v3, v4} =
         {x:real^N | ?a b c d.
         &0 < a /\
         &0 < b /\
         &0 < c /\
         &0 < d /\
         a + b + c + d = &1 /\
         a % v1 + b % v2 + c % v3 + d % v4 = x}`,

   REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN
   REWRITE_TAC[conv0; affsign; sgn_gt; lin_combo; UNION_EMPTY] THEN
   MATCH_MP_TAC EQ_TRANS THEN
   EXISTS_TAC
    `?f. (!w:real^N. w IN {v1, v2, v3, v4} ==> &0 < f w) /\
         sum {v1, v2, v3, v4} f = &1 /\
         vsum {v1, v2, v3, v4} (\v. f v % v) = y` THEN
   CONJ_TAC THENL [REWRITE_TAC[IN] THEN MESON_TAC[]; ALL_TAC] THEN
   SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
            REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
            REAL_ARITH `&0 < x ==> &0 < x / &2`;
            FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
   ASM_REWRITE_TAC[IN_ELIM_THM;
                   REAL_ARITH `x - y:real = z <=> x = y + z`;
                   VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
   REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]);;
(* ======================= *)
(* LEMMA 81 *)
(* ======================= *)

let ARIKWRQ = 
prove(`! v1 v2 v3 (v4:real^3).
  let s = {v1,v2,v3,v4} in
  CARD s = 4 /\ ~ coplanar_alt s ==>
  conv s = aff_ge ( s DIFF {v1} ) {v1} INTER 
  aff_ge ( s DIFF {v2} ) {v2} INTER 
  aff_ge ( s DIFF {v3} ) {v3} INTER 
  aff_ge ( s DIFF {v4} ) {v4} `,
 LET_TR THEN 
SIMP_TAC[CARD4; SET_RULE ` ~(v1 IN {v2, v3, v4}) /\ ~(v2 = v3 \/ v3 = v4 \/ v4 = v2)
  ==> {v1, v2, v3, v4} DIFF {v1} = {v2,v3,v4} /\
  {v1, v2, v3, v4} DIFF {v2} = {v3,v4,v1} /\
  {v1, v2, v3, v4} DIFF {v3} = {v4,v1,v2} /\
  {v1, v2, v3, v4} DIFF {v4} = {v1,v2,v3} `] THEN 
REWRITE_TAC[CARD4; IN_SET3;DE_MORGAN_THM] THEN 
SIMP_TAC[AFF_GES_GTS] THEN 
REWRITE_TAC[CONVEX_HULL_4_EQUIV] THEN 
REPEAT STRIP_TAC THEN 
REWRITE_TAC[SET_RULE ` a = b <=> (! x. x IN a <=> x IN b ) `;
  IN_INTER; IN_ELIM_THM] THEN 
GEN_TAC THEN EQ_TAC THENL [
ASM_MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
  VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `];
FIRST_X_ASSUM MP_TAC ] THEN
NHANH (SPEC ` x: real^3` (GEN ` v:real^3` (SPEC_ALL COEFS_4))) THEN 
ABBREV_TAC ` aa = COEF4_1 v1 v2 v3 v4 x ` THEN 
ABBREV_TAC ` bb = COEF4_2 v1 v2 v3 v4 x ` THEN 
ABBREV_TAC ` cc = COEF4_3 v1 v2 v3 v4 x ` THEN 
ABBREV_TAC ` dd = COEF4_4 v1 v2 v3 v4 x ` THEN 
REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `] THEN PHA THEN 
NHANH (MESON[REAL_ARITH` a + b + c + d = d + a + b + c `;
  VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]`
aa + bb + cc + dd = &1 /\
 x = aa % v1 + bb % v2 + cc % v3 + dd % v4 /\
 (!ta tb tc td.
      x = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
      ==> ta = aa /\ tb = bb /\ tc = cc /\ td = dd) /\
 (?ta tb tc t.
      &0 <= t /\
      ta + tb + tc + t = &1 /\
      x = ta % v2 + tb % v3 + tc % v4 + t % v1) /\
 (?ta tb tc t.
      &0 <= t /\
      ta + tb + tc + t = &1 /\
      x = ta % v3 + tb % v4 + tc % v1 + t % v2) /\
 (?ta tb tc t.
      &0 <= t /\
      ta + tb + tc + t = &1 /\
      x = ta % v4 + tb % v1 + tc % v2 + t % v3) /\
 (?ta tb tc t.
      &0 <= t /\
      ta + tb + tc + t = &1 /\
      x = ta % v1 + tb % v2 + tc % v3 + t % v4)
 ==> &0 <= aa /\ &0 <= bb /\ &0 <= cc /\ &0 <= dd`) THEN 
MATCH_MP_TAC (MESON[]` ( a1 /\ a2 /\ a3 ==> l) ==>
  aa /\ ( a1 /\ a2 /\ a4 ) /\ a3 ==> l `) THEN MESON_TAC[]);;




(* ================ *)
(* LEMMA 82 *)
(* ================= *)




let MXHKOXR = 
prove(`! v1 v2 v3 (v4:real^3). let s = {v1,v2,v3,v4} in
  CARD s = 4 /\ ~ coplanar_alt s ==>
  conv0 s = aff_gt ( s DIFF {v1} ) {v1} INTER 
  aff_gt ( s DIFF {v2} ) {v2} INTER 
  aff_gt ( s DIFF {v3} ) {v3} INTER 
  aff_gt ( s DIFF {v4} ) {v4} `,
 LET_TR THEN 
SIMP_TAC[CARD4; SET_RULE ` ~(v1 IN {v2, v3, v4}) /\ ~(v2 = v3 \/ v3 = v4 \/ v4 = v2)
  ==> {v1, v2, v3, v4} DIFF {v1} = {v2,v3,v4} /\
  {v1, v2, v3, v4} DIFF {v2} = {v3,v4,v1} /\
  {v1, v2, v3, v4} DIFF {v3} = {v4,v1,v2} /\
  {v1, v2, v3, v4} DIFF {v4} = {v1,v2,v3} `] THEN 
REWRITE_TAC[CARD4; IN_SET3;DE_MORGAN_THM] THEN 
SIMP_TAC[AFF_GES_GTS; CONV0_4 ] THEN 
REPEAT STRIP_TAC THEN 
REWRITE_TAC[SET_RULE ` a = b <=> (! x. x IN a <=> x IN b ) `;
  IN_INTER; IN_ELIM_THM] THEN 
GEN_TAC THEN EQ_TAC THENL [
ASM_MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
  VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `];
FIRST_X_ASSUM MP_TAC ] THEN
NHANH (SPEC ` x: real^3` (GEN ` v:real^3` (SPEC_ALL COEFS_4))) THEN 
ABBREV_TAC ` aa = COEF4_1 v1 v2 v3 v4 x ` THEN 
ABBREV_TAC ` bb = COEF4_2 v1 v2 v3 v4 x ` THEN 
ABBREV_TAC ` cc = COEF4_3 v1 v2 v3 v4 x ` THEN 
ABBREV_TAC ` dd = COEF4_4 v1 v2 v3 v4 x ` THEN 
REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `] THEN PHA THEN 
NHANH (MESON[REAL_ARITH` a + b + c + d = d + a + b + c `;
  VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]`
aa + bb + cc + dd = &1 /\
 x = aa % v1 + bb % v2 + cc % v3 + dd % v4 /\
 (!ta tb tc td.
      x = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
      ==> ta = aa /\ tb = bb /\ tc = cc /\ td = dd) /\
 (?ta tb tc t.
      &0 < t /\
      ta + tb + tc + t = &1 /\
      x = ta % v2 + tb % v3 + tc % v4 + t % v1) /\
 (?ta tb tc t.
      &0 < t /\
      ta + tb + tc + t = &1 /\
      x = ta % v3 + tb % v4 + tc % v1 + t % v2) /\
 (?ta tb tc t.
      &0 < t /\
      ta + tb + tc + t = &1 /\
      x = ta % v4 + tb % v1 + tc % v2 + t % v3) /\
 (?ta tb tc t.
      &0 < t /\
      ta + tb + tc + t = &1 /\
      x = ta % v1 + tb % v2 + tc % v3 + t % v4)
==> &0 < aa /\ &0 < bb /\ &0 < cc /\ &0 < dd `) THEN 
MATCH_MP_TAC (MESON[]` ( a1 /\ a2 /\ a3 ==> l) ==>
  aa /\ ( a1 /\ a2 /\ a4 ) /\ a3 ==> l `) THEN MESON_TAC[]);;

 
let CONV0_4 = 
prove
  (`conv0 {v1, v2, v3, v4} =
         {x:real^N | ?a b c d.
         &0 < a /\
         &0 < b /\
         &0 < c /\
         &0 < d /\
         a + b + c + d = &1 /\
         a % v1 + b % v2 + c % v3 + d % v4 = x}`,

   REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN
   REWRITE_TAC[conv0; affsign; sgn_gt; lin_combo; UNION_EMPTY] THEN
   MATCH_MP_TAC EQ_TRANS THEN
   EXISTS_TAC
    `?f. (!w:real^N. w IN {v1, v2, v3, v4} ==> &0 < f w) /\
         sum {v1, v2, v3, v4} f = &1 /\
         vsum {v1, v2, v3, v4} (\v. f v % v) = y` THEN
   CONJ_TAC THENL [REWRITE_TAC[IN] THEN MESON_TAC[]; ALL_TAC] THEN
   SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
            REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
            REAL_ARITH `&0 < x ==> &0 < x / &2`;
            FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
   ASM_REWRITE_TAC[IN_ELIM_THM;
                   REAL_ARITH `x - y:real = z <=> x = y + z`;
                   VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
   REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]);;

let CONV0_4POINTS = CONV0_4;;



(* ================== *)
(* LEMMA 78 *)

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


let ZRFMKPY = 
prove(` ! v1 v2 v3 v4 (v:real^3).
  ~coplanar_alt {v1, v2, v3, v4}
         ==> (v IN conv {v1, v2, v3, v4} <=>
              &0 <= COEF4_1 v1 v2 v3 v4 v /\
              &0 <= COEF4_2 v1 v2 v3 v4 v /\
              &0 <= COEF4_3 v1 v2 v3 v4 v /\
              &0 <= COEF4_4 v1 v2 v3 v4 v) /\
             (v IN conv0 {v1, v2, v3, v4} <=>
              &0 < COEF4_1 v1 v2 v3 v4 v /\
              &0 < COEF4_2 v1 v2 v3 v4 v /\
              &0 < COEF4_3 v1 v2 v3 v4 v /\
              &0 < COEF4_4 v1 v2 v3 v4 v) `,

NHANH (SPEC_ALL COEFS_4) THEN REWRITE_TAC[CONVEX_HULL_4_EQUIV; 
CONV0_4POINTS; IN_ELIM_THM] THEN MESON_TAC[]);;
let LEMMA78 = ZRFMKPY;;



(* APRIL WORKS *)
(* =========== *)
(* NGUYEN QUANG TRUONG *)
let IMP_TAC = IMP_IMP_TAC;;



let QUAANG_TRUOONN = 
prove(` ! v0 v1 v2 v3 (v4:real^N).
   CARD {v0, v1, v2, v3, v4} = 5 /\
         (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4})
         ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {})`,

REWRITE_TAC[CONV_SET2; cone; CARD5; SET_RULE ` a INTER b = {} <=> 
  ~ (? x. a x /\ b x ) `; GSYM aff_ge_def; IN; IN_INTER] THEN 
NHANH (SET_RULE ` ~{v1, v2, v3, v4} v0 ==>
  ~ ( v0 = v1 \/ v0 = v3 ) /\ ~ ( v0 = v2 \/ v0 = v4 ) `) THEN 
ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN 
SIMP_TAC[AFF_GE_12] THEN REWRITE_TAC[DE_MORGAN_THM] THEN 
REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN 
UNDISCH_TAC ` (x:real^N) = tv % v0 + ta % v1 + tb % v3` THEN 
UNDISCH_TAC ` (x:real^N) = tv' % v0 + ta' % v2 + tb' % v4` THEN 
REWRITE_TAC[MESON[]` x = a 
 ==> x = (b:real^N) ==> c <=> x = a /\ a = b ==> c `] THEN 
REWRITE_TAC[VECTOR_ARITH` a % v + d = b % v + e <=>
  ( a - b ) % v + d = e `] THEN 
ASM_CASES_TAC ` &0 < ta + tb ` THENL [DOWN_TAC THEN 
REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL; REAL_FIELD ` &0 < a ==> ~ ( &1 / a = &0 )`]`
  &0 < ta + tb /\ aaa /\
 aa = ta % v1 + tb % v3 <=> &0 < ta + tb /\ aaa /\
  &1 / ( ta + tb ) % aa = &1 / ( ta + tb ) % ( ta % v1 + tb % v3) `] THEN 
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH `
  &1 / a * b = b / a `] THEN STRIP_TAC THEN DOWN_TAC THEN 
NHANH (MESON[REAL_LE_RDIV_0]`&0 <= ta /\ &0 <= tb /\ a1 /\ &0 <= ta' /\
 &0 <= tb' /\ a2 /\
 &0 < ta + tb /\ a3 ==> &0 <= ta / (ta + tb) /\ &0 <= tb / (ta + tb) /\
  &0 <= ta' / (ta + tb) /\ &0 <= tb' / (ta + tb) `) THEN ASM_MESON_TAC[
REAL_FIELD` tv + ta + tb = &1 /\ tv' + ta' + tb' = &1 /\
  &0 < ta + tb ==> (tv' - tv) / (ta + tb) + ta' / (ta + tb) +
  tb' / (ta + tb) = &1 /\ ta / ( ta + tb ) + tb / ( ta + tb ) = &1`];
DOWN_TAC THEN 
NHANH (MESON[REAL_ARITH` &0 <= a /\ &0 <= b /\ ~( &0 < a + b ) 
==> a = &0 /\ b = &0 `]`&0 <= ta /\ &0 <= tb /\a1/\a2 /\a3/\a4 /\
 ~(&0 < ta + tb) /\ a5 ==> ta = &0 /\ tb = &0`) THEN 
PURE_ONCE_REWRITE_TAC[MESON[]` P ta tb /\ ta = &0 /\ tb = &0 
  <=> P ( &0 ) ( &0 ) /\ ta = &0 /\ tb = &0 `] THEN 
REWRITE_TAC[ZERO_NEUTRAL; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN 
REWRITE_TAC[VECTOR_ARITH` (tv' - tv) % v + a = vec 0 <=> tv' % v + a
  = tv % v `; MESON[]` a = b /\ b = c <=> a = c /\ b = c `] THEN 
MESON_TAC[VECTOR_ARITH ` &1 % v = v `]]);;
(* le 80. p 51 *)
(* ================ *)

let JVDAFRS = 
prove(` ! v0 v1 v2 v3 (v4:real^N).
   CARD {v0, v1, v2, v3, v4} = 5 /\
         (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4})
         ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {} /\
               conv {v2, v4} INTER cone v0 {v1, v3} = {})`,
 MESON_TAC[QUAANG_TRUOONN]);;
(* LEMMA 22 *)
(* =========================== *)

let SQRT8_POS = MESON[REAL_ARITH ` &0 < &8 `; SQRT_POS_LT]` &0 < sqrt (&8) `;;

let SQRT8_LT_4_45 = 
prove(` sqrt8 < #4.45 `,

SIMP_TAC[sqrt8; REAL_ARITH ` &0 < #4.45 `; MESON[REAL_ARITH ` &0 < &8 `; 
SQRT_POS_LT]` &0 < sqrt (&8) `; LT_POW2_EQ_LT; SQRT8_POW2] THEN REAL_ARITH_TAC);;

let PROVE_NOT_COLLINEAR = 
prove(` ! v0 v1 (v2:real^3).
         &2 <= dist3 v0 v1 /\
         dist3 v0 v1 <= #2.51 /\
         #2.45 <= dist3 v1 v2 /\
         dist3 v1 v2 <= #2.51 /\
         #2.77 <= dist3 v0 v2 /\
         dist3 v0 v2 <= sqrt8
         ==> ~ collinear {v0, v1, v2}`,

REWRITE_TAC[COLLINEAR_AS_IN_CONV2; MID_COND; dist3; LENGTH_EQ_EX; DE_MORGAN_THM] THEN 
SIMP_TAC[DIST_SYM] THEN 
REPEAT GEN_TAC THEN 
ABBREV_TAC ` a = dist(v0,v1:real^3)` THEN 
ABBREV_TAC ` b = dist(v0,v2:real^3)` THEN 
ABBREV_TAC ` c = dist(v1,v2:real^3)` THEN 
MP_TAC SQRT8_LT_4_45  THEN 
REAL_ARITH_TAC);;
let BPOW8APOW2CPOW2 = 
prove(`&2 <= a /\
 a <= #2.51 /\
 #2.45 <= c /\
 c <= #2.51 /\
 #2.77 <= b /\
 b <= sqrt8
==> b pow 2 <= &8 /\ a pow 2 <= #2.51 pow 2 /\ c pow 2 <= #2.51 pow 2 `,

REWRITE_TAC[MESON[]` a1 /\ a2 /\a3 /\a4 /\a5 /\a6 ==> l <=>
  a1 /\a3 /\a5 ==> a2 /\a4 /\a6 ==> l `] THEN 
NHANH (REAL_ARITH`&2 <= a /\ #2.45 <= c /\ #2.77 <= b ==>
 &0 < a /\ &0 < b /\ &0 < c /\ &0 < #2.51 `) THEN 
SIMP_TAC[sqrt8; POW2_COND_LT; SQRT8_POS; SQRT8_POW2]);;
let IMP_PRE_LE_19 = 
prove(`&2 <= a /\
 a <= #2.51 /\
 #2.45 <= c /\
 c <= #2.51 /\
 #2.77 <= b /\
 b <= sqrt8
 ==> &0 < &2 /\
     &2 <= a /\
     &0 < #2.77 /\
     #2.77 <= b /\
     &0 < #2.45 /\
     #2.45 <= c /\
     a pow 2 <= #2.77 pow 2 + #2.45 pow 2 /\
     b pow 2 <= &2 pow 2 + #2.45 pow 2 /\
     c pow 2 <= &2 pow 2 + #2.77 pow 2 `,

CONV_TAC REAL_RAT_REDUCE_CONV THEN NHANH (BPOW8APOW2CPOW2 ) THEN REAL_ARITH_TAC);;
(* ==================== *)

let LT_SQ8_IMP_LT2 = 
prove_by_refinement(
` a < sqrt (&8) ==> ~ ( &2 <= &1 / &2 * a ) `,

  (* {{{ proof *)
  [
  (ASM_CASES_TAC ` &0 <= a `);
    (UNDISCH_TAC `&0 <= a `);
    (SIMP_TAC[REAL_LT_IMP_LE; SQRT8_POS; LT_POW2_COND; REAL_ARITH `  &2 <= &1 / &2 * a <=> &4 <= a `; REAL_ARITH` &0 <= &4 `; POW2_COND; SQRT8_POW2]);
    BY((REAL_ARITH_TAC));
  (FIRST_X_ASSUM MP_TAC);
  BY((REAL_ARITH_TAC))
  ]);;
  (* }}} *)

(*
let condC = new_definition ` condC M13 m12 m14 M24 m34 (m23:real) =
  ((! x. x IN {M13, m12, m14, M24, m34, m23 } ==> &0 <= x ) /\
  M13 <= m12 + m23 /\
  M13 <= m14 + m34 /\ 
  M24 < m12 + m14 /\
  M24 < m23 + m34 /\ 
  &0 <= delta (M13 pow 2) (m12 pow 2) (m14 pow 2) (M24 pow 2) (m34 pow 2 )
   (m23 pow 2 ) )`;;

let LE_FOR_LEMMA36 = prove(`(CARD {u, v, w} = 3 /\ packing {u, v, w} /\ dist (u,v) < sqrt8) /\
       ~(dist (u,v) / &2 < dist (w,&1 / &2 % (u + v))) ==>
  condC (sqrt (&8)) (&2) (&2) (sqrt (&8)) (&2) (&2) /\
     CARD {u, w, v, u + v - w} = 4 /\
     &2 <= dist3 u w /\
     &2 <= dist3 w v /\
     &2 <= dist3 v (u + v - w) /\
     &2 <= dist3 u (u + v - w) /\
     dist3 u v < sqrt (&8) /\
     dist3 w (u + v - w) <= sqrt (&8) `,
REWRITE_TAC[condC; delta; SQRT8_POW2] THEN 
REWRITE_TAC[SET_RULE ` (! x. x IN ( a INSERT b ) ==> p x ) <=>
  p a /\ (! x. x IN b  ==> p x ) `; NOT_IN_EMPTY] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
SIMP_TAC[SQRT8_POS; REAL_LT_IMP_LE; dist3; sqrt8; packing] THEN 
SIMP_TAC[REAL_LT_IMP_LE; SQRT8_POS; LT_POW2_COND;
  REAL_ARITH ` &0 <= &4 `; POW2_COND; SQRT8_POW2] THEN 
CONV_TAC REAL_RAT_REDUCE_CONV THEN 
REWRITE_TAC[NORM_ARITH` dist (v,u + v - w) = dist (u,w) /\
  dist (u,u + v - w) = dist (v,w) /\ 
  dist (w,u + v - w) = &2 * dist (w,&1 / &2 % (u + v)) `] THEN 
STRIP_TAC THEN CONJ_TAC THENL [
UNDISCH_TAC `CARD {(u:real^3), v, w} = 3` THEN 
REWRITE_TAC[CARD3; CARD4; IN_SET3] THEN 
REWRITE_TAC[DE_MORGAN_THM] THEN DAO THEN 
STRIP_TAC THEN CONJ_TAC THENL [
NHANH (NORM_ARITH`u + v - w = w ==> dist (w,u) = &1 / &2 *  dist (u,v) `) THEN 
UNDISCH_TAC `dist ((u:real^3),v) < sqrt (&8)` THEN 
 NHANH (LT_SQ8_IMP_LT2 ) THEN DOWN_TAC THEN SET_TAC[];  
REWRITE_TAC[VECTOR_ARITH ` ((v:real^N) = u + v - w <=> u = w )`;
  VECTOR_ARITH ` ((u:real^N) = u + v - w <=> v = w ) `] THEN ASM_MESON_TAC[]]; 
DAO THEN CONJ_TAC THENL [REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN 
REAL_ARITH_TAC;DOWN_TAC THEN REWRITE_TAC[CARD3] THEN SET_TAC[]]]);;
*)


let MIDDLE_POINT_IN_CONV2 = 
prove(` &1 / &2 % ( u + v ) IN conv {u,v} `,

REWRITE_TAC[CONV_SET2; IN_ELIM_THM; VECTOR_ADD_LDISTRIB] THEN 
MESON_TAC[REAL_ARITH ` &0 <= &1 / &2 `; REAL_ARITH` &1 / &2 + &1 / &2 = &1 `]);;
let INTER_DISJONT_EX = 
SET_RULE ` ( a INTER b = {} ) <=> (! x. ~ (x IN a /\ x IN b )) `;;


(* LEMMA36 *)

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

MATCH_MP (SPEC_ALL AFFINE_HULL_FINITE) (MESON[FINITE_RULES] ` FINITE {(a:real^N),b,c} `) ;;



let PLANE_IMP_AFFINE = 
prove(`plane (p:real^N -> bool ) ==> affine p `,
 
MESON_TAC[plane; AFFINE_AFFINE_HULL]);;


let PLANE_IMP_AFFINE = 
prove(` plane (p:real^N -> bool ) ==> affine p `,

REWRITE_TAC[plane; AFFINE_HULL_3; affine; FUN_EQ_THM; IN_ELIM_THM] THEN 
STRIP_TAC THEN ASM_SIMP_TAC[IN] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN 
SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN 
REWRITE_TAC[VECTOR_ARITH` (( a:real^N) + b + c ) + a' + b' + c'
  = ( a + a' ) + ( b + b') + c + c' `] THEN EXISTS_TAC ` u' * u'' + v' * u''' ` THEN 
EXISTS_TAC ` (u' * v'' + v' * v''')` THEN EXISTS_TAC ` (u' * w' + v' * w'')` THEN 
ASM_SIMP_TAC[prove(` u' + v' = &1 /\
  u''' + v''' + w'' = &1 /\
  u'' + v'' + w' = &1 ==>
  (u' * u'' + v' * u''') + (u' * v'' + v' * v''') + u' * w' + v' * w'' = &1 `,
SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN REAL_ARITH_TAC);
  GSYM VECTOR_ADD_RDISTRIB]);;



let IMP_AFFINE_HULL_SUBSET = 
prove(` FINITE a /\ a SUBSET s /\ 
~( a = {} )/\ affine s  ==> ( affine hull a ) SUBSET s `,

SIMP_TAC[AFFINE_HULL_FINITE; SUBSET; IN_ELIM_THM] THEN 
REWRITE_TAC[ GSYM SUBSET] THEN MESON_TAC[AFFINE]);;


let SET_EQ_EX = SET_RULE `a = b <=> (! x. x IN a <=> x IN b ) `;;

let SET_EQ_TO_SUBSET = SET_RULE ` a = b <=>  a SUBSET b /\ b SUBSET a `;;




let OTHORGONAL_QUATER_FOR = 
prove(` delta x12 ( x12 + x23 ) ( x12 + x24 )  x23 x24 x34 =
  x12 * ups_x x23 x24 x34 `,
 REWRITE_TAC[delta; ups_x] THEN REAL_ARITH_TAC);;

let ORTHOGONAL_CROSS_PRODUCT = 
prove(` u dot ( u cross v ) = &0 /\
  v dot ( u cross v ) = &0 `,

REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3] THEN
LET_TR THEN REWRITE_TAC[DOT_3; VECTOR_3] THEN REAL_ARITH_TAC);;
let PITHAGOR_CROSS = 
prove(` dist (a +  (b - a) cross (c - a),b) pow 2 = 
dist (b,a) pow 2 +  norm (  (b - a) cross (c - a) ) pow 2 `,

REWRITE_TAC[vector_norm; dist] THEN
SIMP_TAC[DOT_POS_LE; SQRT_WORKS] THEN 
REWRITE_TAC[VECTOR_ARITH` ((a:real^N) + b) - c = b - (c - a ) `] THEN 
ABBREV_TAC ` ab = ( b - (a:real^3)) ` THEN 
ABBREV_TAC ` ac = ( c - (a:real^3)) ` THEN 
REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN 
SIMP_TAC[ORTHOGONAL_CROSS_PRODUCT; DOT_SYM] THEN 
REAL_ARITH_TAC);;
let PITHAGOR_NORM = 
prove(` a dot b = &0 ==> dist (a,b) pow 2 = norm a pow 2 +
  norm b pow 2 `,

SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN 
SIMP_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM] THEN REAL_ARITH_TAC);;
let VEC3_EQ_EX= 
prove(`! a (b:real^3). a = b <=> a$1 = b$1 /\ a$2 = b$2 /\ a$3 = b$3 `,

SIMP_TAC[CART_EQ; DIMINDEX_3] THEN 
REWRITE_TAC[ARITH_RULE`1 <= i /\ i <= 3 <=>
  i = 1 \/ i = 2 \/ i = 3 `] THEN MESON_TAC[]);;
let CROSS_CONVERT = 
prove_by_refinement(
`  (b - a) cross (c - d) =  (a - b) cross (d - c )`,

  (* {{{ proof *)
  [
  (REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3]);
  (LET_TR);
  (REWRITE_TAC[lemma_cm3 ]);
  (REWRITE_TAC[VEC3_EQ_EX]);
  (REWRITE_TAC[VEC3_EQ_EX; VECTOR_3]);
  BY((REAL_ARITH_TAC))
  ]);;
  (* }}} *)


let lemma1 = MESON[prove(` dist(b,c) pow 2 = (a - c - (a - b)) dot (a - c - (a - b)) `,
			 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN 
			   MESON_TAC[VECTOR_ARITH
		` b - (c:real^N) = (a - c) - ( a - b) `])]`
  ups_x  aa bb (dist (b,c) pow 2 ) = 
  ups_x aa bb (( a - c - (a - b)) dot (a - c - (a - b))) `;;

let NORM_CROSS_PRODUCT_UPS_X  = 
prove_by_refinement(
  `&4 * norm ( (b - a) cross (c - a)) pow 2 =
    ups_x (dist (a,b) pow 2) (dist (a,c) pow 2) (dist (b,c) pow 2)`,

  (* {{{ proof *)
  [
  (REWRITE_TAC[lemma1 ]);
  (ONCE_REWRITE_TAC[CROSS_CONVERT]);
  (SIMP_TAC[ups_x;DIST_SYM; dist; vector_norm; DOT_POS_LE; SQRT_WORKS]);
  (REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3]);
  (LET_TR);
  (REWRITE_TAC[DOT_3; VECTOR_3]);
  (ABBREV_TAC ` ab = a - (b:real^3) `);
  (ABBREV_TAC ` cc = a - (c:real^3) `);
  BY((REWRITE_TAC[lemma_cm3 ] THEN REAL_ARITH_TAC))
  ]);;
  (* }}} *)

let lemma1 = 
prove(
  ` dist (  a cross b, a ) pow 2  = norm ( a cross b) pow 2 +   
    norm a pow 2 /\dist (  a cross b, b ) pow 2  = norm ( a cross b) pow 2 +   
    norm b pow 2 `,
 
  SIMP_TAC[DOT_SYM;ORTHOGONAL_CROSS_PRODUCT ; PITHAGOR_NORM; DIST_SYM]
);;
let NOT_COLLINEAR_IMP_CROSS_NOT_COPLANAR = 
prove_by_refinement(
 ` ! u v (w:real^3). ~ collinear {a,b,c} ==> ~ coplanar_alt {
  a +  (b - a ) cross ( c - a ),a,b,c} `,

  (* {{{ proof *)
  [
  (MP_TAC POLFLZY);
  (LET_TR);
  (SIMP_TAC[]);
  (DISCH_TAC);
  (REWRITE_TAC[NORM_ARITH` dist (a + b ,a) = norm (b ) `]);
  (REWRITE_TAC[NORM_ARITH`dist (a + c,b) =  dist ( c, b - a ) `]);
  (SIMP_TAC[lemma1]);
  (REWRITE_TAC[GSYM dist]);
  (SIMP_TAC[DIST_SYM; OTHORGONAL_QUATER_FOR]);
  (ONCE_REWRITE_TAC[REAL_ARITH` a * b = &0 <=> ( &4 * a ) * b = &0 `]);
  (SIMP_TAC[NORM_CROSS_PRODUCT_UPS_X]);
  (REWRITE_TAC[REAL_ENTIRE]);
  BY((MESON_TAC[FHFMKIY]))
  ]);;
  (* }}} *)

let ORTHOGONAL_IMP_PITHAGOR = 
prove(` (x:real^N) dot ((a:real^N) - b) = &0 ==>
  dist (a + x,b) pow 2 = norm x pow 2 + dist (a,b) pow 2`,

SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN 
REWRITE_TAC[VECTOR_ARITH` (a + c) - b = c + a - (b:real^N)`] THEN 
ABBREV_TAC ` aa = ( a - (b:real^N)) ` THEN 
SIMP_TAC[DOT_LADD; DOT_RADD; DOT_SYM; ZERO_NEUTRAL]);;
let NOT_COL_AND_ORTHO_IMP_NOT_COPL = 
prove(`! a b c (x:real^3).
 ~collinear {a, b, c} /\ x dot (a - b) = &0 /\
 x dot (a - c) = &0 /\ ~(x = vec 0)
 ==> ~coplanar_alt {a + x, a, b, c}`,

MP_TAC POLFLZY THEN LET_TR THEN SIMP_TAC[] THEN 
SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR ] THEN 
SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR; NORM_ARITH ` dist (a + x,a) = norm x `] THEN 
SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR; NORM_ARITH ` dist (a + x,a) = norm x `;
OTHORGONAL_QUATER_FOR] THEN SIMP_TAC[COL_EQ_UPS_0] THEN 
SIMP_TAC[COL_EQ_UPS_0; GSYM NORM_POS_LT; REAL_ENTIRE; MESON[RELATE_POW2]`
  a pow 2 = &0 <=> a = &0 `; REAL_ARITH ` &0 < a ==> ~( a = &0 ) `]);;
let PLANE_NORM_IMP_AFFINE = 
prove(`! p. plane_norm p ==> affine p `,

REWRITE_TAC[plane_norm; affine] THEN GEN_TAC THEN STRIP_TAC THEN 
ASM_SIMP_TAC[IN_ELIM_THM;  MESON[]` a = &1 <=> &1 = a `] THEN 
ONCE_REWRITE_TAC[ VECTOR_ARITH ` ( a + b ) - c = ( a + b ) - &1 % c `] THEN 
ASM_SIMP_TAC[ VECTOR_ARITH` (u % x + v % y) - (u + v) % v0 = 
u % ( x - v0 ) +  v % ( y - v0 ) `; DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;
let IN_PLANE_IMP_OTHORGONAL = 
prove(`
 n dot (x - v0) = &0 /\ n dot (y - v0) = &0 /\ n dot (z - v0) = &0 ==>
  n dot ( x - y ) = &0 /\ n dot ( x - z ) = &0 `,

SIMP_TAC[DOT_RSUB] THEN REAL_ARITH_TAC);;
let IMP_A1_EQ_0 = 
prove_by_refinement(
`(n:real^N) dot (x - v0) = &0 /\
 n dot (y - v0) = &0 /\
 n dot (z - v0) = &0 /\
 ~(n = vec 0) /\
 x' = a1 % (x + n) + a2 % x + a3 % y + a4 % z /\
 a1 + a2 + a3 + a4 = &1 /\
 n dot (x' - v0) = &0
 ==> a1 = &0`,

  (* {{{ proof *)
  [
   (STRIP_TAC);
   (UNDISCH_TAC ` (n:real^N) dot (x' - v0) = &0`);
  (ASM_SIMP_TAC[VECTOR_ARITH`(a1 % x + y ) - v0 = a1 % ( x - v0 ) + y - v0 + a1 % v0 `]);
  (ONCE_REWRITE_TAC[ VECTOR_ARITH` a % x - y =  a % ( x - y ) + a % y - y `]);
  (ASM_SIMP_TAC[DOT_RADD; VECTOR_ARITH` ( a + b ) - (c:real^N)   = b + a - c `; DOT_RMUL; ZERO_NEUTRAL]);
  (ASM_SIMP_TAC[DOT_RADD; VECTOR_ARITH` ( a + b ) - (c:real^N)   = b + a - c `; DOT_RMUL; ZERO_NEUTRAL; DOT_RSUB;REAL_ARITH` ((a4 * (n dot v0) - n dot v0 + a3 * (n dot v0)) + a2 * (n dot v0)) + a1 * (n dot v0) = ( a1 + a2 + a3 + a4 ) * ( n dot v0 ) - n dot v0 `; REAL_ARITH ` &1 * a - a = &0 `]);
  BY((ASM_MESON_TAC[REAL_ENTIRE; GSYM DOT_EQ_0]))
  ]);;
  (* }}} *)

let LEMMA7 = 
prove(` !x y z (p:real^3 -> bool).
         plane_norm p /\ ~collinear {x, y, z} /\ {x, y, z} SUBSET p
         ==> p = aff {x, y, z}`,

NHANH (PLANE_IMP_AFFINE) THEN 
REPEAT STRIP_TAC THEN 
REWRITE_TAC[aff; SET_EQ_TO_SUBSET] THEN CONJ_TAC THENL [
UNDISCH_TAC ` plane_norm (p:real^3 -> bool ) ` THEN 
REWRITE_TAC[plane_norm] THEN 
STRIP_TAC THEN 
UNDISCH_TAC ` {(x:real^3), y, z} SUBSET p` THEN 
ASM_SIMP_TAC[SET3_SUBSET; IN_ELIM_THM] THEN 
NHANH (IN_PLANE_IMP_OTHORGONAL ) THEN 
DOWN_TAC THEN 
NHANH (MESON[NOT_COL_AND_ORTHO_IMP_NOT_COPL]`
  ~collinear {(x:real^3), y, z} /\
 ~(n = vec 0) /\a1 /\a2 /\a4 /\a3/\
 n dot (x - y) = &0 /\
 n dot (x - z) = &0 ==> ~coplanar_alt { x + n ,x,y,z} `) THEN 
REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN 
REPEAT STRIP_TAC THEN 
UNDISCH_TAC `~coplanar_alt {x + n, x, y, (z:real^3)} ` THEN 
NHANH (SPEC `x' :real^3` (GEN `v :real^3` ( SPEC_ALL COEFS_4 ))) THEN 
ABBREV_TAC ` a1 = COEF4_1 (x + n) x y z x'` THEN 
ABBREV_TAC ` a2 = COEF4_2 (x + n) x y z x'` THEN 
ABBREV_TAC ` a3 = COEF4_3 (x + n) x y z x'` THEN 
ABBREV_TAC ` a4 = COEF4_4 (x + n) x y z x'` THEN 
STRIP_TAC THEN 
DOWN_TAC THEN 
REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN 
NHANH (MESON[IMP_A1_EQ_0]` ~(n = vec 0) /\
 aa1 /\
 n dot (x - v0) = &0 /\
 n dot (y - v0) = &0 /\
 n dot (z - v0) = &0 /\
 aa2 /\aa3 /\
 n dot (x' - v0) = &0 /\aa4/\aa5 /\aa6/\aa7/\
 ~coplanar_alt {x + n, x, y, z} /\
 a1 + a2 + a3 + a4 = &1 /\
 x' = a1 % (x + n) + a2 % x + a3 % y + a4 % z /\ l ==>
  a1 = &0 `) THEN 
PURE_ONCE_REWRITE_TAC[MESON[]` P a1 /\ a1 = &0 <=> P (&0) /\
  a1 = &0 `] THEN 
REWRITE_TAC[ZERO_NEUTRAL; VECTOR_ARITH` &0 % x + y = y `] THEN 
MESON_TAC[];
ASM_MESON_TAC[PLANE_NORM_IMP_AFFINE ; FINITE_RULES; 
SET_RULE` ~({(x:real^N), y, z} = {} )`;  IMP_AFFINE_HULL_SUBSET]]);;
let SMWTDMU = LEMMA7;;

let DET_VEC3_AS_CROSS_DOT = 
prove_by_refinement(
` det_vec3 v1 v2 v3 = (  v1 cross v2 ) dot v3 `,

  (* {{{ proof *)
  [
  (REWRITE_TAC[det_vec3; cross; triple_of_real3; real3_of_triple; mk_vec3; DOT_3; VECTOR_3]);
  (LET_TR);
  (REWRITE_TAC[det_vec3; cross; triple_of_real3; real3_of_triple; mk_vec3; DOT_3; VECTOR_3]);
  BY((REAL_ARITH_TAC))
  ]);;
  (* }}} *)

let COL_EQ_NORM_CROSS = 
prove_by_refinement(
` ! v1 v2 (v3:real^3). collinear {v1,v2,v3} <=>
 norm ( (v2 - v1) cross (v3 - v1)) pow 2 = &0 `,

  (* {{{ proof *)
  [
  (REWRITE_TAC[COL_EQ_UPS_0]);
  (REWRITE_TAC[GSYM NORM_CROSS_PRODUCT_UPS_X]);
  BY((REAL_ARITH_TAC))
  ]);;
  (* }}} *)




let COLLINEAR_IMP_COPLANAR = 
prove(` ! v1 v2 v3 v3 (v:real^3). collinear {v1,v2,v3} ==>
coplanar_alt {v1,v2,v3,v} `,

REWRITE_TAC[COPLANAR_DET_VEC3_EQ_0; COL_EQ_NORM_CROSS; DET_VEC3_AS_CROSS_DOT ] THEN 
REWRITE_TAC[GSYM RELATE_POW2; NORM_EQ_0] THEN REPEAT GEN_TAC THEN 
SIMP_TAC[VECTOR_ARITH ` vec 0 dot x = &0 `]);;
(* MAY WORKS, LEMMA 85 ; VBVYGGT *)




let POS_EQ_NOT_COPLANANR = 
prove(` &0 <   delta (dist ((x1:real^3),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) <=> ~coplanar_alt {x1, x2, x3, x4} `,

MP_TAC (DELTA_POS_4POINTS) THEN MP_TAC POLFLZY THEN LET_TR THEN 
REWRITE_TAC[REAL_ARITH` a <= b <=> a = b \/ a < b `] THEN 
MESON_TAC[REAL_ARITH` ~( a = b /\ a < b ) `]);;
let SUM_CHI_EQ_2DELTA = 
prove(` let chi11 = chi x12 x13 x14 x23 x24 x34 in
 let chi22 = chi x12 x24 x23 x14 x13 x34 in
 let chi33 = chi x34 x13 x23 x14 x24 x12 in
 let chi44 = chi x34 x24 x14 x23 x13 x12 in
 &2 * delta x12 x13 x14 x23 x24 x34 = chi11 + chi22 + chi33 + chi44`,
 LET_TR THEN 
REWRITE_TAC[chi; delta] THEN REAL_ARITH_TAC);;
let NOT_0_IMP_SUM_CHI_1 = 
prove(`~(delta x12 x13 x14 x23 x24 x34 = &0)
 ==> chi x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) +
     chi x12 x24 x23 x14 x13 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) +
     chi x34 x13 x23 x14 x24 x12 / (&2 * delta x12 x13 x14 x23 x24 x34) +
     chi x34 x24 x14 x23 x13 x12 / (&2 * delta x12 x13 x14 x23 x24 x34) =
     &1`,
 MP_TAC SUM_CHI_EQ_2DELTA THEN 
LET_TR THEN CONV_TAC REAL_FIELD);;
(* MAY WORKS *)

let PROVE_DIST_FROM_V1 = 
prove(` ~coplanar_alt {v1, v2, v3, v4} ==>
let x12 = dist (v1,v2) pow 2 in
 let x13 = dist (v1,v3) pow 2 in
 let x14 = dist (v1,v4) pow 2 in
 let x23 = dist (v2,v3) pow 2 in
 let x24 = dist (v2,v4) pow 2 in
 let x34 = dist (v3,v4) pow 2 in
 let chi11 = chi x12 x13 x14 x23 x24 x34 in
 let chi22 = chi x12 x24 x23 x14 x13 x34 in
 let chi33 = chi x34 x13 x23 x14 x24 x12 in
 let chi44 = chi x34 x24 x14 x23 x13 x12 in
 p =
 &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
 (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)
 ==> dist3 p v1 pow 2 =
    ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) `,

REWRITE_TAC[ GSYM POS_EQ_NOT_COPLANANR] THEN 
NHANH (REAL_ARITH` a < b ==> ~( b = a ) `) THEN 
NHANH NOT_0_IMP_SUM_CHI_1  THEN 
LET_TR THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
  REAL_ARITH` ( &1 / a ) * b = b / a `] THEN 
ABBREV_TAC ` a1 = chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
     (dist (v2,v3) pow 2)
     (dist (v2,v4) pow 2)
     (dist (v3,v4) pow 2) /
     (&2 *
      delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
      (dist (v2,v3) pow 2)
      (dist (v2,v4) pow 2)
      (dist (v3,(v4:real^3)) pow 2))` THEN 
ABBREV_TAC ` a2 = chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
     (dist (v1,v4) pow 2)
     (dist (v1,v3) pow 2)
     (dist (v3,v4) pow 2) /
     (&2 *
      delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
      (dist (v2,v3) pow 2)
      (dist (v2,v4) pow 2)
      (dist (v3,(v4:real^3)) pow 2)) ` THEN 
REWRITE_TAC[ GSYM dist3] THEN 
ABBREV_TAC ` a3 = chi (dist3 v3 v4 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v4 pow 2)
     (dist3 v2 v4 pow 2)
     (dist3 v1 v2 pow 2) /
     (&2 *
      delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
      (dist3 v2 v3 pow 2)
      (dist3 v2 v4 pow 2)
      (dist3 v3 v4 pow 2)) ` THEN 
ABBREV_TAC ` a4 = chi (dist3 v3 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2)
     (dist3 v1 v3 pow 2)
     (dist3 v1 v2 pow 2) /
     (&2 *
      delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
      (dist3 v2 v3 pow 2)
      (dist3 v2 v4 pow 2)
      (dist3 v3 v4 pow 2)) ` THEN 
SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN 
REPEAT STRIP_TAC THEN 
REWRITE_TAC[dist3; dist; NORM_POW_2; VECTOR_ARITH` 
  (((&1 - (a2 + a3 + a4)) % v1 + a2 % v2 + a3 % v3 + a4 % v4) - v1) =
  a2 % ( v2 - v1 ) + a3 % (v3 - v1 ) + a4 % ( v4 - v1 ) `;
  VECTOR_ARITH` ( a + b ) dot ( a + b ) = a dot a + &2 * ( a dot b )
  + b dot b `] THEN 
REWRITE_TAC[DOT_RADD; DOT_LMUL; DOT_RMUL] THEN 
REWRITE_TAC[X_DOT_X_EQ] THEN 
REWRITE_TAC[DOT_NORM_NEG; VECTOR_ARITH` v2 - v1 - (v4 - v1)
  = (v2:real^N) - v4 `] THEN 
SIMP_TAC[GSYM dist; DIST_SYM; GSYM dist3; D3_SYM] THEN 
EXPAND_TAC "a2" THEN 
EXPAND_TAC "a3" THEN 
EXPAND_TAC "a4" THEN 
REWRITE_TAC[GSYM dist3 ] THEN 
ABBREV_TAC ` x12 = dist3 v1 v2 pow 2 ` THEN 
ABBREV_TAC ` x13 = dist3 v1 v3 pow 2 ` THEN 
ABBREV_TAC ` x14 = dist3 v1 v4 pow 2 ` THEN 
ABBREV_TAC ` x23 = dist3 v2 v3 pow 2 ` THEN 
ABBREV_TAC ` x24 = dist3 v2 v4 pow 2 ` THEN 
ABBREV_TAC ` x34 = dist3 v3 v4 pow 2 ` THEN 
UNDISCH_TAC ` &0 < delta x12 x13 x14 x23 x24 x34 ` THEN 
ONCE_REWRITE_TAC[REAL_FIELD` &0 < a ==> b = c <=> &0 < a
 ==> b * ( &2 * a) pow 2 = c * ( &2 * a ) pow 2 `] THEN 
ONCE_REWRITE_TAC[REAL_ARITH` &0 < a <=> &0 < &2 * a `] THEN 
SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
  REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c * 
b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN 
SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
  REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
  REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN 
SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2 
  * d = b * bb * d `] THEN 
SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
  a * b / &2 `] THEN 
REWRITE_TAC[chi; rho_ij';
 delta] THEN 
REAL_ARITH_TAC);;

let PROVE_EQ_DIST_FROM4 = 
prove(` ~coplanar_alt {v1, v2, v3, v4} ==>
let x12 = dist (v1,v2) pow 2 in
 let x13 = dist (v1,v3) pow 2 in
 let x14 = dist (v1,v4) pow 2 in
 let x23 = dist (v2,v3) pow 2 in
 let x24 = dist (v2,v4) pow 2 in
 let x34 = dist (v3,v4) pow 2 in
 let chi11 = chi x12 x13 x14 x23 x24 x34 in
 let chi22 = chi x12 x24 x23 x14 x13 x34 in
 let chi33 = chi x34 x13 x23 x14 x24 x12 in
 let chi44 = chi x34 x24 x14 x23 x13 x12 in
 p =
 &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
 (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)
==>
dist3 p v2 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) /\
dist3 p v3 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) /\
dist3 p v4 pow 2 =
 ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34)  `,

REWRITE_TAC[ GSYM POS_EQ_NOT_COPLANANR] THEN 
NHANH (REAL_ARITH` a < b ==> ~( b = a ) `) THEN 
NHANH NOT_0_IMP_SUM_CHI_1  THEN 
LET_TR THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
  REAL_ARITH` ( &1 / a ) * b = b / a `] THEN 
ABBREV_TAC ` a1 = chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
     (dist (v2,v3) pow 2)
     (dist (v2,v4) pow 2)
     (dist (v3,v4) pow 2) /
     (&2 *
      delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
      (dist (v2,v3) pow 2)
      (dist (v2,v4) pow 2)
      (dist (v3,(v4:real^3)) pow 2))` THEN 
ABBREV_TAC ` a2 = chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
     (dist (v1,v4) pow 2)
     (dist (v1,v3) pow 2)
     (dist (v3,v4) pow 2) /
     (&2 *
      delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
      (dist (v2,v3) pow 2)
      (dist (v2,v4) pow 2)
      (dist (v3,(v4:real^3)) pow 2)) ` THEN 
REWRITE_TAC[ GSYM dist3] THEN 
ABBREV_TAC ` a3 = chi (dist3 v3 v4 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v4 pow 2)
     (dist3 v2 v4 pow 2)
     (dist3 v1 v2 pow 2) /
     (&2 *
      delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
      (dist3 v2 v3 pow 2)
      (dist3 v2 v4 pow 2)
      (dist3 v3 v4 pow 2)) ` THEN 
ABBREV_TAC ` a4 = chi (dist3 v3 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2)
     (dist3 v1 v3 pow 2)
     (dist3 v1 v2 pow 2) /
     (&2 *
      delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
      (dist3 v2 v3 pow 2)
      (dist3 v2 v4 pow 2)
      (dist3 v3 v4 pow 2)) ` THEN 
ONCE_REWRITE_TAC[MESON[VECTOR_ARITH` &1 % x = x `]` dist3 a b pow 2 =
  aa <=> dist3 a ( &1 % b ) pow 2 = aa `] THEN 
ONCE_REWRITE_TAC[MESON[]` a = &1 <=> &1 = a `] THEN 
SIMP_TAC[] THEN 
STRIP_TAC THEN STRIP_TAC THEN 
REWRITE_TAC[dist3; dist] THEN 
REWRITE_TAC[VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v2
  = a1 % ( v1 - v2 ) + a3 % ( v3 - v2 ) + a4 % (v4 - v2 ) `;
  VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v3
  = a1 % ( v1 - v3 ) + a2 % ( v2 - v3 ) + a4 % (v4 - v3 )`;
  VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v4 =
  a1 % ( v1 - v4 ) + a2 % ( v2 - v4 ) + a3 % (v3 - v4 )`] THEN 
REWRITE_TAC[NORM_POW_2] THEN 
REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; GSYM NORM_POW_2] THEN 
REWRITE_TAC[DOT_NORM_NEG; VECTOR_ARITH` v3 - v4 - (v2 - v4) =
  (v3:real^N) - v2 `; GSYM dist; GSYM dist3 ] THEN 
EXPAND_TAC "a1" THEN 
EXPAND_TAC "a2" THEN 
EXPAND_TAC "a3" THEN 
EXPAND_TAC "a4" THEN 
REWRITE_TAC[GSYM dist3 ] THEN 
REWRITE_TAC[prove(` dist3 (v4 - v3) (v1 - v3) = dist3 v1 v4 `, 
REWRITE_TAC[dist3] THEN CONV_TAC NORM_ARITH)] THEN 
SIMP_TAC[D3_SYM] THEN 
ABBREV_TAC ` x12 = dist3 v1 v2 pow 2 ` THEN 
ABBREV_TAC ` x13 = dist3 v1 v3 pow 2 ` THEN 
ABBREV_TAC ` x14 = dist3 v1 v4 pow 2 ` THEN 
ABBREV_TAC ` x23 = dist3 v2 v3 pow 2 ` THEN 
ABBREV_TAC ` x24 = dist3 v2 v4 pow 2 ` THEN 
ABBREV_TAC ` x34 = dist3 v3 v4 pow 2 ` THEN 
UNDISCH_TAC ` &0 < delta x12 x13 x14 x23 x24 x34 ` THEN 
ONCE_REWRITE_TAC[REAL_FIELD` &0 < a ==> ( b = c ) /\ ( bb = cc ) /\ ( bbb = ccc ) 
<=> &0 < a
 ==> ( b * ( &2 * a) pow 2 = c * ( &2 * a ) pow 2 ) /\
( bb * ( &2 * a) pow 2 = cc * ( &2 * a ) pow 2 ) /\
( bbb * ( &2 * a) pow 2 = ccc * ( &2 * a ) pow 2 ) `] THEN 
ONCE_REWRITE_TAC[REAL_ARITH` &0 < a <=> &0 < &2 * a `] THEN 
SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
  REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c * 
b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN 
SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
  REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
  REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN 
SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2 
  * d = b * bb * d `] THEN 
SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
  a * b / &2 `] THEN SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
  REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c * 
b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN 
SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
  REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
  REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN 
SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2 
  * d = b * bb * d `] THEN 
SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
  a * b / &2 `] THEN 
DISCH_TAC THEN REWRITE_TAC[chi; rho_ij';
 delta] THEN 
REAL_ARITH_TAC);;

let AFFINE_HULL_3 = 
prove
 (`affine hull {a,b,c} =
    { u % a + v % b + w % c | u + v + w = &1}`,

  SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN
  SIMP_TAC[AFFINE_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
  REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
              VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
  REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);;
let AFFINE_HULL_4 = 
prove
 (`affine hull {a,b,c,d} =
    { u % a + v % b + w % c + z % d | u + v + w + z = &1}`,

  SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN
  SIMP_TAC[AFFINE_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
  REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
              VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
  REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);;

let PROVE_EXISTS_CIR_OF_FOUR_POINTS = 
prove(`!(v1:real^3) v2 v3 v4.
         CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
         ==> (? p. p IN affine hull {v1, v2, v3, v4} /\
             (?r. !v. v IN {v1, v2, v3, v4}
                      ==> r = dist (p, v))) `,

NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM]  (GEN `p:real^3` PROVE_DIST_FROM_V1)) THEN 
NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM]  (GEN `p:real^3` PROVE_EQ_DIST_FROM4 )) THEN 
REPEAT GEN_TAC THEN REPEAT LET_TAC THEN ABBREV_TAC `rr = &1 / &2 *
       rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) ` THEN 
REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN 
NHANH (SPEC_ALL REAL_POS_NZ) THEN ASM_SIMP_TAC[] THEN 
NHANH (NOT_0_IMP_SUM_CHI_1 ) THEN ASM_SIMP_TAC[] THEN 
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
  REAL_ARITH ` &1 / a * b = b / a `] THEN 
REWRITE_TAC[FORALL_IN_CLAUSES; MESON[]`(? r. (r:real) = a /\
  r = b /\ r = c /\ r = d ) <=> a = b /\ a = c /\ a = d `] THEN 
REWRITE_TAC[MESON[]` (! x. x = a ==> P a ) <=> P a `] THEN DISCH_TAC THEN 
EXISTS_TAC ` chi11 / (&2 * delta x12 x13 x14 x23 x24 x34) % (v1:real^3) +
      chi22 / (&2 * delta x12 x13 x14 x23 x24 x34) % v2 +
      chi33 / (&2 * delta x12 x13 x14 x23 x24 x34) % v3 +
      chi44 / (&2 * delta x12 x13 x14 x23 x24 x34) % v4 ` THEN 
CONJ_TAC THENL [REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM] THEN 
FIRST_X_ASSUM MP_TAC THEN MESON_TAC[NOT_0_IMP_SUM_CHI_1 ]; 
FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[dist3; DIST_POS_LE; EQ_POW2_COND]]);;











let IMP_PROPERTIES_OF_CIR4 = 
prove(`!(v1:real^3) v2 v3 v4.
         CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
         ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
             (?r. !v. v IN {v1, v2, v3, v4}
                      ==> r = dist (circumcenter {v1, v2, v3, v4},v))`,

NHANH (SPEC_ALL PROVE_EXISTS_CIR_OF_FOUR_POINTS ) THEN REWRITE_TAC[circumcenter; IN]
THEN MESON_TAC[EXISTS_THM]);;



let DIST_EQ_IMP_ORTHOGONAL = 
prove(` dist (pp,v2) = dist (pp,v1) /\
  dist (p,v2) = dist (p,v1) ==>
  (pp - p ) dot (v2 - v1 ) = &0 `,

REWRITE_TAC[MONG7_ROI; DOT_LSUB] THEN REAL_ARITH_TAC);;


let IMP_OTHO4 = 
prove(` n dot (v2 - v1) = &0 /\
  n dot (v3 - v1) = &0 /\
  n dot (v4 - v1) = &0 /\
  x IN affine hull {v1,v2,v3,v4} /\
  y IN affine hull {v1,v2,v3,v4} ==>
  n dot (x - y ) = &0 `,

REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM] THEN STRIP_TAC THEN 
DOWN_TAC THEN IMP_TAC THEN SIMP_TAC[REAL_ARITH`a + b = c <=> a = c - b `] THEN 
PHA THEN REWRITE_TAC[VECTOR_ARITH` ((&1 - (v' + w' + z')) % v1 + v' % v2 +
 w' % v3 + z' % v4) - ((&1 - (v + w + z)) % v1 + v % v2 + w % v3 + z % v4)  =
  ( v' - v ) % ( v2 - v1 ) + ( w' - w ) % ( v3 - v1 ) +
  ( z' - z ) % ( v4 - v1 ) `] THEN 
SIMP_TAC[DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;




let UNIQUE_EXISISTING_PROPERTY_C4 = 
prove(`!(v1:real^3) v2 v3 v4.
         CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
         ==>   (!p. p IN affine hull {v1, v2, v3, v4} /\
                  (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p,v))
                  ==> p = circumcenter {v1, v2, v3, v4}) `,

NHANH (SPEC_ALL IMP_PROPERTIES_OF_CIR4 ) THEN 
REPEAT GEN_TAC THEN 
ABBREV_TAC ` pp = circumcenter {(v1:real^3), v2, v3, v4}` THEN 
REPEAT STRIP_TAC THEN 
DOWN_TAC THEN 
REWRITE_TAC[FORALL_IN_CLAUSES] THEN 
REWRITE_TAC[MESON[]` r = a /\ r = b /\ r = c /\ r = d <=> r = a /\ b = a /\ c = a 
  /\ d = a `] THEN 
PHA THEN 
NHANH (MESON[DIST_EQ_IMP_ORTHOGONAL ]`dist (pp,v2) = dist (pp,v1) /\
 dist (pp,v3) = dist (pp,v1) /\
 dist (pp,v4) = dist (pp,v1) /\a11/\a2/\
 dist (p,v2) = dist (p,v1) /\
 dist (p,v3) = dist (p,v1) /\
 dist (p,v4) = dist (p,v1) ==>
  ( p - pp) dot ( v2 - v1 ) = &0 /\
  ( p - pp ) dot ( v3 - v1 ) = &0 /\
  ( p - pp ) dot ( v4 - v1 ) = &0 `) THEN 
ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN 
REWRITE_TAC[GSYM DOT_EQ_0] THEN MESON_TAC[IMP_OTHO4 ]);;



let PROVE_IN_AFFINE_HULL_4 = 
prove(
`~(delta x12 x13 x14 x23 x24 x34 = &0)
 ==> &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
     (chi x12 x13 x14 x23 x24 x34 % v1 +
      chi x12 x24 x23 x14 x13 x34 % v2 +
      chi x34 x13 x23 x14 x24 x12 % v3 +
      chi x34 x24 x14 x23 x13 x12 % v4) IN
     affine hull {(v1:real^3), v2, v3, v4}`,

REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM; VECTOR_ADD_LDISTRIB;
  VECTOR_MUL_ASSOC; REAL_ARITH ` ( &1 / a ) * b = b/a `]
 THEN MESON_TAC[NOT_0_IMP_SUM_CHI_1]);;


(* VBVYGGT , le 85 *)



MESON[POW_2_SQRT; DIST_POS_LE]` dist (x,y) pow 2 = r ==> dist (x,y) = sqrt ( r ) `;;

(* LEMMA 85 *)
let VBVYGGT = 
prove(`!(v1:real^3) v2 v3 v4.
         CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
         ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
             (?r. !v. v IN {v1, v2, v3, v4}
                      ==> r = dist (circumcenter {v1, v2, v3, v4},v)) /\
             (!p. p IN affine hull {v1, v2, v3, v4} /\
                  (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p,v))
                  ==> p = circumcenter {v1, v2, v3, v4}) /\
             (let x12 = dist (v1,v2) pow 2 in
              let x13 = dist (v1,v3) pow 2 in
              let x14 = dist (v1,v4) pow 2 in
              let x23 = dist (v2,v3) pow 2 in
              let x24 = dist (v2,v4) pow 2 in
              let x34 = dist (v3,v4) pow 2 in
              let chi11 = chi x12 x13 x14 x23 x24 x34 in
              let chi22 = chi x12 x24 x23 x14 x13 x34 in
              let chi33 = chi x34 x13 x23 x14 x24 x12 in
              let chi44 = chi x34 x24 x14 x23 x13 x12 in
              circumcenter {v1, v2, v3, v4} =
              &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
              (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)) `,

NHANH (SPEC_ALL UNIQUE_EXISISTING_PROPERTY_C4 ) THEN 
NHANH (SPEC_ALL IMP_PROPERTIES_OF_CIR4 ) THEN 
REWRITE_TAC[MESON[]` (a /\ b1/\b2) /\ b ==> b1 /\b2/\ b/\ d <=> a /\ b1 /\b2/\b==>d `] THEN 
NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] ( GEN `p: real^3 `PROVE_DIST_FROM_V1)) THEN 
NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] ( GEN `p: real^3 ` PROVE_EQ_DIST_FROM4)) THEN 
REPEAT GEN_TAC THEN REPEAT LET_TAC THEN ABBREV_TAC `rr = &1 / &2 *
       rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) ` THEN 
REWRITE_TAC[MESON[]` (! x. x = a ==> P x ) <=> P a `] THEN 
REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN 
NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 )`) THEN 
NHANH (PROVE_IN_AFFINE_HULL_4 ) THEN 
UNDISCH_TAC ` dist ((v1:real^3),v2) pow 2 = x12` THEN 
UNDISCH_TAC ` dist ((v1:real^3),v3) pow 2 = x13` THEN 
UNDISCH_TAC ` dist ((v1:real^3),v4) pow 2 = x14` THEN 
UNDISCH_TAC ` dist ((v2:real^3),v3) pow 2 = x23` THEN 
UNDISCH_TAC ` dist ((v2:real^3),v4) pow 2 = x24` THEN 
UNDISCH_TAC ` dist ((v3:real^3),v4) pow 2 = x34` THEN 
UNDISCH_TAC ` chi x12 x13 x14 x23 x24 x34 = chi11 ` THEN 
UNDISCH_TAC ` chi x12 x24 x23 x14 x13 x34 = chi22 ` THEN 
UNDISCH_TAC ` chi x34 x13 x23 x14 x24 x12 = chi33` THEN 
UNDISCH_TAC ` chi x34 x24 x14 x23 x13 x12 = chi44` THEN 
REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN 
ABBREV_TAC ` w =  &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
     (chi11 % (v1:real^3) + chi22 % v2 + chi33 % v3 + chi44 % v4)` THEN 
REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `]
THEN REPLICATE_TAC 13 DISCH_TAC THEN 
REWRITE_TAC[FORALL_IN_CLAUSES;dist3] THEN PHA THEN 
NHANH (MESON[POW_2_SQRT; DIST_POS_LE]` dist (x,y) pow 2 = r
 ==> dist (x,y) = sqrt ( r ) `) THEN MESON_TAC[]);;
let NOT_COPLANAR_IMP_EXISTS_CIR = 
prove(`! (v1:real^3) v2 v3 v4.
       CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
       ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
           (?r. !v. v IN {v1, v2, v3, v4}
                    ==> r = dist (circumcenter {v1, v2, v3, v4},v)) `,

MESON_TAC[VBVYGGT]);;
let THREE_POINTS_COP = 
prove(` ! v1 v2 (v3:real^3). coplanar_alt {v1,v2,v3} `,

MESON_TAC[DIMINDEX_3; ARITH_RULE` 2 <= 3 `; COPLANAR_3]);;
let PER_SET4 = SET_RULE ` {a,b,c,d} = {b,a,c,d} /\
  {a,b,c,d} = {c,b,a,d} /\
  {a,b,c,d} = {d,b,c,a} `;;

let NOT_COPLANAR_IMP_CARD4 = 
prove(` ~ coplanar_alt {(v1:real^3), v2, v3, v4} 
==> CARD {v1, v2, v3, v4} = 4 `,
 REWRITE_TAC[CARD4; IN_SET3] THEN 
MP_TAC (GEN_ALL THREE_POINTS_COP ) THEN 
MESON_TAC[PER_SET4; SET_RULE` {a,a,b,c} = {a,b,c} `]);;

let NOT_COPLANAR_IMP_EXISTS_CIR2 = MESON[NOT_COPLANAR_IMP_EXISTS_CIR ; 
NOT_COPLANAR_IMP_CARD4 ]` ! (v1:real^3) v2 v3 v4. ~ coplanar_alt {v1, v2, v3, v4}
       ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
           (?r. !v. v IN {v1, v2, v3, v4}
                    ==> r = dist (circumcenter {v1, v2, v3, v4},v)) `;;

let NOT_COPLANAR_IMP_RADV_PROPERTIES = 
prove(` ~coplanar_alt {(v1:real^3), v2, v3, v4} ==>
  (! w. {v1, v2, v3, v4} w ==> radV {v1, v2, v3, v4} 
    = dist (circumcenter {v1,v2,v3,v4} ,w) ) `,

NHANH (SPEC_ALL NOT_COPLANAR_IMP_EXISTS_CIR2) THEN 
REWRITE_TAC[IN; radV] THEN MESON_TAC[EXISTS_THM]);;
let ZJEWPAP = ` ! v1 v2 v3 (v4:real^3).
  let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar_alt s 
  ==> radV {v1,v2,v3}  <= radV s  `;;

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

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

MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN 
REWRITE_TAC[UPS_X_EQ_ZERO_COND; REAL_ARITH` a <= b <=> a = b \/ a < b `] THEN 
REWRITE_TAC[dist3] THEN MESON_TAC[REAL_ARITH` ~( a = b /\ a < b ) `]);;

let ETA_Y_POW2_EQ = 
prove(`(dist (v1,v2) pow 2 * dist (v1,v3) pow 2 * dist (v2,v3) pow 2) /
      ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) =
( eta_y (dist3 v2 v3) (dist3 v1 v3) (dist3 v1 v2)) pow 2 `,

REWRITE_TAC[eta_y;dist3; eta_x] THEN LET_TR THEN 
REWRITE_TAC[GSYM REAL_POW_2; GSYM dist3 ] THEN 
SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `; 
REAL_ARITH ` a * b * c = c * b * a `] THEN 
MESON_TAC[SQRT_WORKS; REAL_LE_SQUARE_POW; REAL_LE_MUL;
  REAL_LE_DIV; dist3 ; ZERO_LE_UPS_X; UPS_X_SYM]);;

let ETA_Y_POS_LE = 
prove(` &0 <= eta_y (dist3 v1 v2) (dist3 v1 v3) (dist3 v2 v3) `,

REWRITE_TAC[eta_y; eta_x] THEN LET_TR THEN REWRITE_TAC[GSYM REAL_POW_2] THEN 
MESON_TAC[REAL_LE_POW_2; REAL_LE_MUL; ZERO_LE_UPS_X; REAL_LE_DIV;
  SQRT_POS_LE]);;

(* lemma 87 *)
let ZJEWPAP = 
prove(` ! v1 v2 v3 (v4:real^3).
  let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar_alt s 
  ==> radV {v1,v2,v3}  <= radV s  `,

LET_TR THEN 
NHANH (MESON[COLLINEAR_IMP_COPLANAR ]`~coplanar_alt {v1, v2, v3, v4}
  ==> ~ collinear {(v1:real^3),v2,v3} `) THEN 
SIMP_TAC[NOT_COLL_IMP_RADV_EQ_ETA_Y] THEN 
REWRITE_TAC[MESON[]` a /\ b /\ c <=> (a/\b)/\c`] THEN 
NHANH (SPEC_ALL VBVYGGT) THEN 
REPEAT GEN_TAC THEN 
NHANH (NOT_COPLANAR_IMP_RADV_PROPERTIES) THEN 
ABBREV_TAC ` pp = circumcenter {(v1:real^3), v2, v3, v4}` THEN 
MP_TAC (SPECL [`pp :real^3`; ` v1: real^3`; `v2:real^3`; ` v3:real^3`] DELTA_POS_4POINTS ) THEN 
REWRITE_TAC[REWRITE_RULE[IN] FORALL_IN_CLAUSES; 
   FORALL_IN_CLAUSES ] THEN 
REWRITE_TAC[MESON[]` ( a ==> b ==> c <=> a /\ b ==> c ) /\
  ( (a /\ b ) /\ c <=> a /\ b /\ c ) `] THEN 
REPEAT STRIP_TAC THEN 
UNDISCH_TAC ` &0 <=
      delta (dist ((pp:real^3),v1) pow 2) (dist (pp,v2) pow 2) (dist (pp,v3) pow 2)
      (dist (v1,v2) pow 2)
      (dist (v1,v3) pow 2)
      (dist (v2,v3) pow 2)` THEN 
ABBREV_TAC `p1 = dist ((pp:real^3),v1)` THEN 
ABBREV_TAC `p2 = dist ((pp:real^3),v2)` THEN 
ABBREV_TAC `p3 = dist ((pp:real^3),v3)` THEN 
 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC 
(MESON[]` a ==> b ==> a `)) THEN 
EXPAND_TAC "p1" THEN 
EXPAND_TAC "p2" THEN 
EXPAND_TAC "p3" THEN 
FIRST_X_ASSUM MP_TAC THEN 
REWRITE_TAC[NOT_COL_EQ_UPS_X_POS ] THEN 
REWRITE_TAC[NOT_COL_EQ_UPS_X_POS; DELTA_RRR_INTERPRETE] THEN 
SIMP_TAC[REAL_FIELD` &0 < a ==> -- b * c + r * a = a * ( r - ( b * c )  / a ) `] THEN 
SIMP_TAC[ETA_Y_POW2_EQ; REAL_LE_MUL_EQ] THEN 
UNDISCH_TAC ` radV {(v1:real^3), v2, v3, v4} = p1 ` THEN 
SIMP_TAC[] THEN 
EXPAND_TAC "p1" THEN 
UNDISCH_TAC `r = dist ((pp: real^3),v4)` THEN 
SIMP_TAC[] THEN 
REPLICATE_TAC 3 REMOVE_TAC THEN 
SIMP_TAC[ETA_Y_SYYM; REAL_ARITH` &0 <= a - b <=> b <= a `] THEN 
MESON_TAC[DIST_POS_LE; POW2_COND; ETA_Y_POS_LE ]);;




let NOT_EQ_BASIS_IMP_OTHORGANAL = MESON[DOT_BASIS_BASIS_UNEQUAL]
` ! i j. ~( i = j ) ==> basis i dot basis j = &0 `;;

let BASIS_DIS_OTHORGONAL = 
MESON[ARITH_RULE` ~( 1 = 2 \/ 1 = 3 \/ 2 = 3 ) `; NOT_EQ_BASIS_IMP_OTHORGANAL]
` basis 1 dot basis 2 = &0 /\
  basis 1 dot basis 3 = &0 /\
  basis 2 dot basis 3 = &0 ` ;;

let NORM_BASIS_VEC3 = 
prove(` ! i. i = 1 \/ i = 2 \/ i = 3 ==> 
norm (( basis i ):real^3 ) = &1 `,

MESON_TAC[DIMINDEX_3; ARITH_RULE` i = 1 \/ i = 2 \/ i = 3 <=>
  1 <= i /\ i <= 3`; NORM_BASIS]);;
let AAA_LEMMA = 
prove(` &0 < a /\
 a <= b /\
 b <= c /\ ll ==> &0 <= b pow 2 - a pow 2 /\ &0 <= c pow 2 - b pow 2 `,

REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN 
MESON_TAC[REAL_LT_IMP_LE; POW2_COND; POS_IMP_POW2; REAL_LE_TRANS]);;
let LLEEMAA = 
prove(` &0 < a /\
     a <= b /\
     b <= c /\
     &0 < a' /\
     a' <= b' /\
     b' <= c' /\
     a <= a' /\
     b <= b' /\
     c <= c' /\ l ==> &0 <= a' pow 2 - a pow 2 /\
  &0 <= b' pow 2 - b pow 2 /\
  &0 <= c' pow 2 - c pow 2 `,

REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN 
MESON_TAC[POS_IMP_POW2; REAL_ARITH` a < b ==> a <= b `;
  REAL_LE_TRANS]);;
let TYUNJLA = 
prove(` !(e1:real^3) e2 e3 a b c a' b' c' t1 t2 t3.
  e1 = basis 1 /\
     e2 = basis 2 /\
     e3 = basis 3 /\
     &0 < a /\
     a <= b /\
     b <= c /\
     &0 < a' /\
     a' <= b' /\
     b' <= c' /\
     a <= a' /\
     b <= b' /\
     c <= c' /\
     (!x. x IN {t1, t2, t3} ==> &0 < x) /\
     t1 + t2 + t3 < &1 /\
     v =
     ((t1 + t2 + t3) * a) % e1 +
     ((t2 + t3) * sqrt (b pow 2 - a pow 2)) % e2 +
     (t3 * sqrt (c pow 2 - b pow 2)) % e3 /\
  v' = ((t1 + t2 + t3) * a') % e1 +
     ((t2 + t3) * sqrt (b' pow 2 - a' pow 2)) % e2 +
     (t3 * sqrt (c' pow 2 - b' pow 2)) % e3 ==>
  norm v <= norm v' `,

REPEAT STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN 
FIRST_X_ASSUM MP_TAC THEN 
SIMP_TAC[POW2_COND; NORM_POS_LE; NORM_POW_2; DOT_LADD; DOT_RADD;
DOT_LMUL; DOT_RMUL] THEN ASM_SIMP_TAC[] THEN 
SIMP_TAC[GSYM NORM_POW_2; NORM_BASIS_VEC3 ] THEN 
SIMP_TAC[BASIS_DIS_OTHORGONAL; MESON[DOT_SYM; BASIS_DIS_OTHORGONAL]
  ` basis 2 dot basis 1 = &0 /\ basis 3 dot basis 1 = &0 /\
  basis 3 dot basis 2 = &0 `; ZERO_NEUTRAL] THEN 
REWRITE_TAC[REAL_ARITH` (a * x ) * ( b * x ) * c = a * b * c * x pow 2 `] THEN 
REPEAT STRIP_TAC THEN DOWN_TAC THEN 
NHANH (AAA_LEMMA) THEN PHA THEN 
NHANH (MESON[AAA_LEMMA]` &0 < a /\ a <= b /\ b <= c /\ aa <= a /\ l ==>
  &0 <= b pow 2 - a pow 2 /\ &0 <= c pow 2 - b pow 2 `) THEN 
SIMP_TAC[SQRT_WORKS] THEN 
ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `] THEN 
REWRITE_TAC[REAL_ARITH` ((t1 + t2 + t3) * (t1 + t2 + t3) * &1 pow 2 * a' pow 2 +
      (t2 + t3) * (t2 + t3) * &1 pow 2 * (b' pow 2 - a' pow 2) +
      t3 * t3 * &1 pow 2 * (c' pow 2 - b' pow 2)) -
     ((t1 + t2 + t3) * (t1 + t2 + t3) * &1 pow 2 * a pow 2 +
      (t2 + t3) * (t2 + t3) * &1 pow 2 * (b pow 2 - a pow 2) +
      t3 * t3 * &1 pow 2 * (c pow 2 - b pow 2)) = 
  t1 * ( t1 + &2 * t2 + &2 * t3 ) * ( a' pow 2 - a pow 2 ) +
  t2 * (t2 + &2 * t3 ) * ( b' pow 2 - b pow 2 ) +
  t3 pow 2 * ( c' pow 2 - c pow 2 ) `] THEN 
REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN 
PHA THEN NHANH (LLEEMAA) THEN STRIP_TAC THEN 
UNDISCH_TAC ` (!x. x IN {t1, t2, t3} ==> &0 < x)` THEN 
REPLICATE_TAC 3 ( FIRST_X_ASSUM MP_TAC) THEN 
REWRITE_TAC[FORALL_IN_CLAUSES] THEN PHA THEN 
NHANH (REAL_ARITH` &0 < t1 /\ &0 < t2 /\ &0 < t3 ==>
  &0 <= t1 /\ &0 <= t2 /\ &0 <= t1 + &2 * t2 + &2 * t3 /\
  &0 <= t2 + &2 * t3 `) THEN 
MESON_TAC[REAL_LE_ADD; REAL_LE_MUL; REAL_LE_POW_2]);;
let LEMMA83 = TYUNJLA ;;

let DELTA_TRIPLE_SUB_H_EXPAND = 
prove(`
delta (a01 - h) (a02 - h) (a03 - h) x12 x13 x23 = 
  delta a01 a02 a03 x12 x13 x23 - h * ups_x x12 x13 x23 `,

REWRITE_TAC[delta;ups_x] THEN REAL_ARITH_TAC);;
let PROVE_EXISTS_H_DELTA_0 = 
prove(`&0 < ups_x x12 x13 x23 /\ &0 <= delta a01 a02 a03 x12 x13 x23
 ==> (?h. &0 <= h /\ h = ( delta a01 a02 a03 x12 x13 x23 ) / ups_x x12 x13 x23 /\
 delta (a01 - h) (a02 - h) (a03 - h) x12 x13 x23 = &0 )`,

REWRITE_TAC[DELTA_TRIPLE_SUB_H_EXPAND] THEN 
DISCH_TAC THEN 
EXISTS_TAC`( delta a01 a02 a03 x12 x13 x23 ) / ups_x x12 x13 x23` THEN 
ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_DIV] THEN 
FIRST_X_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD);;
let FIRST_POINT_IN_AFF3 = 
prove(` ! w v1 v2. w IN aff {w,v1,v2} `,

REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN 
EXISTS_TAC ` &1 ` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN 
REWRITE_TAC[ZERO_NEUTRAL] THEN CONV_TAC VECTOR_ARITH);;
let THREE_GEN_POINTS_IN_AFF3 = MESON[PER_SET3; FIRST_POINT_IN_AFF3 ]` a IN aff {a,b,c} /\
  b IN aff {a,b,c} /\ c IN aff {a,b,c} `;;

let PROVE_THE_HYPOTHESI_FOR_74 = 
prove(` (let s = {v1, v2, v3, v4} in
         CARD s = 4 /\

         ~coplanar_alt s /\
         eta_y (dist3 v1 v2 ) (dist3 v1 v3) (dist3 v2 v3) <= r )
==> ( let x12 = dist3 v1 v2 pow 2 in
     let x13 = dist3 v1 v3 pow 2 in
     let x23 = dist3 v2 v3 pow 2 in
     CARD {v1, v2, v3, v4} = 4 /\

     ~coplanar_alt {v1, v2, v3, v4} /\
     &0 <= r pow 2 /\
     &0 <= r pow 2 /\
     &0 <= r pow 2 /\
     delta (r pow 2) (r pow 2) (r pow 2) x12 x13 x23 >= &0 ) `,

REPEAT LET_TAC THEN 
SIMP_TAC[REAL_LE_POW_2] THEN 
REWRITE_TAC[DELTA_RRR_INTERPRETE] THEN 
EXPAND_TAC "s" THEN 
NHANH (MESON[COLLINEAR_IMP_COPLANAR]` ~ coplanar_alt {v1, v2, v3, v} ==>
  ~ collinear {v1, v2, (v3:real^3)} `) THEN 
REWRITE_TAC[NOT_COL_EQ_UPS_X_POS] THEN 
EXPAND_TAC "x12" THEN 
EXPAND_TAC "x13" THEN 
EXPAND_TAC "x23" THEN 
REWRITE_TAC[dist3] THEN 
SIMP_TAC[REAL_FIELD` &0 < a ==> -- x * y + r * a = a * ( r - (x * y ) / a )`] THEN 
SIMP_TAC[ETA_Y_POW2_EQ;dist3; ETA_Y_SYYM] THEN 
MP_TAC ETA_Y_POS_LE THEN 
DAO THEN PHA THEN 
REWRITE_TAC[dist3] THEN DAO THEN 
NHANH (MESON[POS_IMP_POW2]` a <= b /\ &0 <= a ==> 
  a pow 2 <= b pow 2 `) THEN 
ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `] THEN 
REWRITE_TAC[REAL_ARITH` a >= &0 <=> &0 <= a `] THEN 
SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_MUL]);;

let INSERT_SUBSET = SET_RULE` {} SUBSET s /\
  ( ( a INSERT s ) SUBSET ss <=> a IN ss /\ s SUBSET  ss ) `;;


let IMP_TAC = REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `];;

let IMP_OTHORGONAL_AFF3 = 
prove(`!v1 v2 v3 u.
     u dot (v1 - v2) = &0 /\ u dot (v1 - v3) = &0
     ==> (!x y. {x, y} SUBSET aff {v1, v2, v3} ==> u dot (x - y) = &0)`,

REWRITE_TAC[aff; AFFINE_HULL_3; INSERT_SUBSET; IN_ELIM_THM] THEN 
REPEAT STRIP_TAC THEN DOWN_TAC THEN 
REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN 
SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN 
REWRITE_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 ASM_SIMP_TAC[DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;

(* MONG7_ROI *)

let DIST_EQ_IMP_OTHORGONAL = 
prove(` ! a b p q. dist (p,a) = dist (p,b) /\ dist (q,a) = dist(q,b) 
==> ( p - q ) dot ( a - b ) = &0 `,

REWRITE_TAC[MONG7_ROI; DOT_LSUB] THEN REAL_ARITH_TAC);;
let NOT_COPLANAR_IMP_NOT_COLLINEAR =
  MATCH_MP (MESON[]` (a ==> b) ==> ~ b ==> ~ a `) (SPEC_ALL COLLINEAR_IMP_COPLANAR);;

(* lemma 89 *)
let PVLJZLA = 
prove( `! (v1:real^3) v2 v3 v4.
     let s = {v1, v2, v3, v4} in
     ~coplanar_alt s
     ==> (circumcenter s IN conv0 s <=>
          orientation s v1 (\x. &0 < x) /\
          orientation s v2 (\x. &0 < x) /\
          orientation s v3 (\x. &0 < x) /\
          orientation s v4 (\x. &0 < x))`,

REWRITE_TAC[orientation; affsign] THEN 
REPEAT GEN_TAC THEN 
LET_TR THEN 
REWRITE_TAC[lin_combo] THEN 
REWRITE_TAC[SET_RULE` s DIFF {a} UNION {a} = s UNION {a} `;
  SET_RULE` {a,b,c,d} UNION {a} = {a,b,c,d} /\
  {a,b,c,d} UNION {b} = {a,b,c,d} /\
  {a,b,c,d} UNION {c} = {a,b,c,d} /\
  {a,b,c,d} UNION {d} = {a,b,c,d}`] THEN 
REWRITE_TAC[MESON[]`a = b /\ c /\ d <=> c /\ d /\ b = a `] THEN 
REWRITE_TAC[SET_RULE` (!w. {v1} w ==> &0 < f w) /\
           sum {v1, v2, v3, v4} f = &1 /\ l
  <=> (!w. w IN {v1,v2,v3,v4} ==> {v1} w ==> &0 < f w) /\
  sum {v1, v2, v3, v4} f = &1 /\ l `;
  SET_RULE` (!w. {v2} w ==> &0 < f w) /\
           sum {v1, v2, v3, v4} f = &1 /\ l
  <=> (!w. w IN {v1,v2,v3,v4} ==> {v2} w ==> &0 < f w) /\
  sum {v1, v2, v3, v4} f = &1 /\ l `;
  SET_RULE` (!w. {v2} w ==> &0 < f w) /\
           sum {v1, v2, v3, v4} f = &1 /\ l
  <=> (!w. w IN {v1,v2,v3,v4} ==> {v2} w ==> &0 < f w) /\
  sum {v1, v2, v3, v4} f = &1 /\ l `;
  SET_RULE` (!w. {v3} w ==> &0 < f w) /\
           sum {v1, v2, v3, v4} f = &1 /\ l
  <=> (!w. w IN {v1,v2,v3,v4} ==> {v3} w ==> &0 < f w) /\
  sum {v1, v2, v3, v4} f = &1 /\ l `;
  SET_RULE` (!w. {v4} w ==> &0 < f w) /\
           sum {v1, v2, v3, v4} f = &1 /\ l
  <=> (!w. w IN {v1,v2,v3,v4} ==> {v4} w ==> &0 < f w) /\
  sum {v1, v2, v3, v4} f = &1 /\ l `] THEN 
 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
            REAL_ARITH `&0 < x /\ &0 < y  ==> &0 < x + y`;
            REAL_ARITH ` &0 < x ==> &0 < x / &2`;
            FINITE_INSERT; CONJUNCT1 FINITE_RULES
; RIGHT_EXISTS_AND_THM]  THEN 
NHANH (NOT_COPLANAR_IMP_CARD4) THEN 
SIMP_TAC[IN_ACT_SING; CARD4; IN_SET3; DE_MORGAN_THM] THEN 
REWRITE_TAC[REAL_ARITH` a - b = c <=> a = b + c `; ZERO_NEUTRAL;
  VECTOR_ARITH`(a:real^N) - b = c <=> a = b + c `; VECTOR_ARITH` x +
  vec 0 = x `] THEN 
REWRITE_TAC[CONV0_4; IN_ELIM_THM] THEN 
NHANH (SPEC ` circumcenter {(v1:real^3), v2, v3, v4} ` ( GEN `v:real^3` (SPEC_ALL COEFS_4))) THEN 
STRIP_TAC THEN 
EQ_TAC THENL [
MESON_TAC[]; 
UNDISCH_TAC ` !ta tb tc td.
          circumcenter {v1, v2, v3, v4} =
          ta % v1 + tb % v2 + tc % v3 + td % v4 /\
          ta + tb + tc + td = &1
          ==> ta = COEF4_1 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
              tb = COEF4_2 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
              tc = COEF4_3 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
              td = COEF4_4 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4})` THEN 
REWRITE_TAC[MESON[]`&0 < v /\ ( ? b . P v b ) <=>
  (? b. &0 < v /\ P v b ) `] THEN 
REWRITE_TAC[MESON[]` &1 = a /\ aa = b <=> a = &1 /\ b = aa `] THEN 
ABBREV_TAC ` (vv:real^3) = circumcenter {v1, v2, v3, v4} ` THEN 
ABBREV_TAC ` a1 = COEF4_1 v1 v2 v3 v4 vv ` THEN 
ABBREV_TAC ` a2 = COEF4_2 v1 v2 v3 v4 vv ` THEN 
ABBREV_TAC ` a3 = COEF4_3 v1 v2 v3 v4 vv ` THEN 
ABBREV_TAC ` a4 = COEF4_4 v1 v2 v3 v4 vv ` THEN PHA THEN 
IMP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN 
REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN PHA THEN 
NHANH (MESON[]`(!ta tb tc td.
      vv = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
      ==> ta = a1 /\ tb = a2 /\ tc = a3 /\ td = a4) /\
 a111  /\
 v + v' + v'' + v''' = &1 /\
 v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv /\
 (?v v' v'' v'''.
      &0 < v' /\
      v + v' + v'' + v''' = &1 /\
      v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) /\
 (?v v' v'' v'''.
      &0 < v'' /\
      v + v' + v'' + v''' = &1 /\
      v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) /\
 (?v v' v'' v'''.
      &0 < v''' /\
      v + v' + v'' + v''' = &1 /\
      v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) ==>
  &0 < v' /\ &0 < v'' /\ &0 < v''' `) THEN MESON_TAC[]]);;



let IMP_IN_AFF_LT = 
prove(`CARD {v1, v2, v3, v4} = 4 ==> ( (?v v' v'' v'''.
           v < &0 /\
           &1 = v + v' + v'' + v''' /\ vv =
           v % v1 + v' % v2 + v'' % v3 + v''' % v4) <=>
  vv IN aff_lt {v2,v3,v4} {v1} ) `,

REWRITE_TAC[CARD4; IN_SET3; DE_MORGAN_THM] THEN SIMP_TAC[AFF_GES_GTS; IN_ELIM_THM]
THEN REMOVE_TAC THEN 
MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
  VECTOR_ARITH` a + b + c + d = d + a + b + (c:real^N)`]);;

let SQRT4_EQ2 = 
prove(` sqrt ( &4 ) = &2 `,

REWRITE_TAC[REAL_ARITH` &4 = &2 pow 2 `] THEN 
MESON_TAC[POW_2_SQRT; REAL_ARITH` &0 <= &2 `]);;

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);;


(* lemma 84 *)
let SHOGYBS = 
prove(` ! x1 x2 x3 (x4:real^3).
  ~coplanar_alt {x1,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
  &0 <= rho_ij' x12 x13 x14 x23 x24 x34  `,

ONCE_REWRITE_TAC[SET_RULE` {v1,v2,v3,v4} =  {v2,v3,v4,v1} `] THEN 
NHANH (NOT_COPLANAR_IMP_NOT_COLLINEAR) THEN 
ONCE_REWRITE_TAC[GSYM (SET_RULE` {v1,v2,v3,v4} =  {v2,v3,v4,v1} `)] THEN 
REWRITE_TAC[NOT_COL_EQ_UPS_X_POS] THEN REPEAT GEN_TAC THEN 
MP_TAC (SPEC_ALL DELTA_POS_4POINTS) THEN 
REPEAT LET_TAC THEN MP_TAC (SPEC_ALL RHUFIIB) THEN DOWN_TAC THEN 
NHANH (MESON[REAL_LE_POW_2]` a pow 2 = b   ==> &0 <= b `) THEN DAO THEN 
SIMP_TAC[UPS_X_SYM] THEN 
REWRITE_TAC[MESON[REAL_FIELD` &0 < a ==> (b * a = c <=> b = c / a )`]`
  &0 < a /\a1 /\a2/\ b * a = c /\l <=>  &0 < a /\a1 /\a2/\ b = c / a /\ l `] THEN 
MP_TAC (REAL_ARITH` &0 <= &4 `) THEN PHA THEN 
NHANH (MESON[REAL_LT_IMP_LE; REAL_LE_DIV;
  REAL_LE_MUL; REAL_LE_ADD; REAL_LE_POW_2]`  &0 <= &4 /\
 &0 < ups_x x23 x24 x34 /\a1/\
 &0 <= delta x12 x13 x14 x23 x24 x34 /\ a2 /\
 &0 <= x34 /\a3 /\ &0 <= x24 /\a4 /\ &0 <= x23 /\a5/\
 &0 <= x14 /\a6 /\ &0 <= x13 /\a7 /\a8 /\ &0 <= x12 ==> 
  &0 <= &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `) THEN 
ABBREV_TAC ` aaa = &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 ` THEN STRIP_TAC THEN 
FIRST_X_ASSUM MP_TAC THEN UNDISCH_TAC ` rho_ij' x12 x13 x14 x23 x24 x34 =
      (chi x12 x13 x14 x23 x24 x34 pow 2 + aaa) / ups_x x23 x24 x34 ` THEN 
UNDISCH_TAC`&0 < ups_x x23 x24 x34` THEN MESON_TAC[REAL_LT_IMP_LE; REAL_LE_DIV;
  REAL_LE_MUL; REAL_LE_ADD; REAL_LE_POW_2]);;

(* le 86 . GDRQXLG *)


let GDRQXLG = 
prove(` ! v1 v2 v3 (v4:real^3).
  let s = {v1, v2, v3, v4} in
let x12 = dist (v1,v2) pow 2 in
                    let x13 = dist (v1,v3) pow 2 in
                    let x14 = dist (v1,v4) pow 2 in
                    let x23 = dist (v2,v3) pow 2 in
                    let x24 = dist (v2,v4) pow 2 in
                    let x34 = dist (v3,v4) pow 2 in
     CARD s = 4 /\ ~coplanar_alt s
     ==> radV s =
        sqrt ( rho_ij' x12 x13 x14 x23 x24 x34) /
         (&2 * sqrt (delta x12 x13 x14 x23 x24 x34))`,

REPEAT GEN_TAC THEN REPEAT LET_TAC THEN EXPAND_TAC "s" THEN 
NHANH (NOT_COPLANAR_IMP_RADV_PROPERTIES) THEN 
NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_DIST_FROM_V1  )) THEN 
NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_EQ_DIST_FROM4 ) ) THEN 
REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN 
NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 )`) THEN 
NHANH (PROVE_IN_AFFINE_HULL_4 ) THEN LET_TR THEN 
REWRITE_TAC[MESON[]`(!x. x = a ==> p x) <=> p a `] THEN 
ABBREV_TAC `taa = (&1 /    (&2 *
     delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
     (dist (v2,v3) pow 2)
     (dist (v2,v4) pow 2)
     (dist (v3,v4) pow 2)) %
    (chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
     (dist (v2,v3) pow 2)
     (dist (v2,v4) pow 2)
     (dist (v3,v4) pow 2) %
     (v1:real^3) +
     chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
     (dist (v1,v4) pow 2)
     (dist (v1,v3) pow 2)
     (dist (v3,v4) pow 2) %
     v2 +
     chi (dist (v3,v4) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2)
     (dist (v1,v4) pow 2)
     (dist (v2,v4) pow 2)
     (dist (v1,v2) pow 2) %
     v3 +
     chi (dist (v3,v4) pow 2) (dist (v2,v4) pow 2) (dist (v1,v4) pow 2)
     (dist (v2,v3) pow 2)
     (dist (v1,v3) pow 2)
     (dist (v1,v2) pow 2) %
     v4)) ` THEN 
REWRITE_TAC[ POS_EQ_NOT_COPLANANR] THEN NGOAC THEN 
NHANH (SPEC_ALL UNIQUE_EXISISTING_PROPERTY_C4 ) THEN 
REWRITE_TAC[FORALL_IN_CLAUSES] THEN ABBREV_TAC ` abc = &1 / &2 *
 rho_ij' (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
 (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2) /
 (&2 *
  delta (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
  (dist (v2,v3) pow 2)
  (dist (v2,v4) pow 2)
  (dist (v3,v4) pow 2)) ` THEN REWRITE_TAC[dist3] THEN 
NHANH (MESON[POW_2_SQRT; DIST_POS_LE]` dist (taa,v2) pow 2 = a ==>
  dist(taa,v2) = sqrt a `) THEN PHA THEN 
NHANH (MESON[]`(!p. p IN affine hull {v1, v2, v3, v4} /\
      (?r. r = dist (p,v1) /\
           r = dist (p,v2) /\
           r = dist (p,v3) /\
           r = dist (p,v4))
      ==> p = circumcenter {v1, v2, v3, v4}) /\ a11 /\
 taa IN affine hull {v1, v2, v3, v4} /\
 dist (taa,v2) pow 2 = abc /\
 dist (taa,v2) = sqrt abc /\
 dist (taa,v3) pow 2 = abc /\
 dist (taa,v3) = sqrt abc /\
 dist (taa,v4) pow 2 = abc /\
 dist (taa,v4) = sqrt abc /\
 dist (taa,v1) pow 2 = abc /\
 dist (taa,v1) = sqrt abc /\ lll ==> taa = circumcenter {v1, v2, v3, v4} `) THEN 
NHANH (SET_RULE ` (!w. {v1, v2, v3, v4} w ==> P w ) ==> P v1 `) THEN PHA THEN 
REWRITE_TAC[MESON[]` a = dist (aa,b) /\ ta = aa <=> ta = aa  /\ a = dist (ta,b) `] THEN 
NHANH (MESON[]` a = b /\ a1 /\ a2 /\ c = a ==> c = b `) THEN NHANH (SPEC_ALL SHOGYBS) THEN 
MP_TAC (SPECL [`v1:real^3`;` v2:real^3`;`v3:real^3`;`v4:real^3`] 
DELTA_POS_4POINTS) THEN REPEAT LET_TAC THEN IMP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN 
REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN 
REWRITE_TAC[MESON[]` a = b ==> a = c <=> a = b ==> c = b `] THEN REPEAT STRIP_TAC THEN 
UNDISCH_TAC ` &1 / &2 *      rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) =
      abc ` THEN UNDISCH_TAC ` &0 <= rho_ij' x12 x13 x14 x23 x24 x34 ` THEN 
ABBREV_TAC ` edl = delta x12 x13 x14 x23 x24 x34 ` THEN UNDISCH_TAC` &0 <= edl ` THEN 
SIMP_TAC[REAL_ARITH` &0 <= &4 `; GSYM SQRT_MUL; GSYM SQRT4_EQ2] THEN 
SIMP_TAC[REAL_ARITH` &0 <= &4 `; REAL_LE_MUL;  GSYM SQRT_DIV] THEN 
REWRITE_TAC[SQRT4_EQ2] THEN MESON_TAC[REAL_FIELD` &1 / &2 * x34 / (&2 * edl) =  x34 / (&4 * edl)`]);;


end;;  (* end of module *)