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




module  Lfjcixp = struct

open Sphere;;
open Fan_defs;;
open Hypermap;;
open Vol1;;
open Fan;;
open Prove_by_refinement;;
open Pack_defs;;
open Collect_geom;;


let LFJCIXP =
prove(`(!y1 y2 y3 y4 y5 y6.
&2 <= y1 /\ y1<= #2.52
/\ &2 <= y2 /\ y2<= #2.52
/\ &2 <= y3 /\ y3<= #2.52
/\ &2 <= y4 /\ y4<= #4.52
/\ y5= &2
/\ y6= &2
==> (y4 <= #3.915 \/ delta (y1 pow 2) (y2 pow 2) (y3 pow 2) (y4 pow 2) (y5 pow 2) (y6 pow 2)< &0))
/\ {v,u,w} SUBSET ball_annulus
/\ packing {v,u,w}
/\ ~(u=w)
/\ norm(v-u)= &2
/\ norm(v-w)= &2
/\ norm (u - w) <= #4.52
==> norm(u-w)<= #3.915
`,

REPEAT STRIP_TAC
THEN MRESAL_TAC Trigonometry.LBEVAKV[`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`][dist;VECTOR_ARITH`a - vec 0= a`;NORM_NEG;NORM_SUB]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[NORM_SUB]
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= a <=> ~(a< &0)`]
THEN MP_TAC(SET_RULE`{v, u, w} SUBSET ball_annulus
==> v IN ball_annulus /\ u IN ball_annulus /\ w IN ball_annulus`)
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[IN_ELIM_THM;DIFF;ball_annulus;ball;cball;REAL_ARITH`~(a< &2)<=> &2<= a`;REAL_ARITH`&2 * #1.26= #2.52`;h0;dist;VECTOR_ARITH`a - vec 0= a`;NORM_NEG;NORM_SUB]
THEN ASM_TAC
THEN DISCH_THEN(LABEL_TAC"YEU")
THEN REPEAT STRIP_TAC
THEN FIND_ASSUM MP_TAC `packing {v,u,w:real^3}`
THEN REWRITE_TAC[packing]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`u:real^3`;`w:real^3`][SET_RULE`{v, u, w} u /\ {v, u, w} w`;dist])
THEN REMOVE_THEN"YEU"(fun th-> MRESA_TAC th[`norm(w:real^3)`;`norm(u:real^3)`;`norm (v:real^3)`;`norm(u-w:real^3)`;`&2`;`&2`]));;



end;;