(* ========================================================================== *)
(* 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;;