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


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


module Hxhytij = struct


open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;

open Uxckfpe;;
open Sgtrnaf;;




let HXHYTIJ= 
prove_by_refinement(`!s vv ww. is_scs_v39 s /\ BBprime2_v39 s vv /\ BBs_v39 s ww ==> (taustar_v39 s vv < taustar_v39 s ww \/ BBindex_v39 s vv <= BBindex_v39 s ww)`,
[REPEAT STRIP_TAC THEN MP_TAC(REAL_ARITH`(taustar_v39 s vv < taustar_v39 s ww)\/ taustar_v39 s ww <= taustar_v39 s vv`) THEN RESA_TAC THEN SUBGOAL_THEN`BBprime_v39 s ww` ASSUME_TAC; ASM_TAC THEN ASM_REWRITE_TAC[IN;BBprime_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39] THEN REPEAT RESA_TAC; REPLICATE_TAC (7-2)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MRESA1_TAC th`ww':num->real^3`) THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; REPLICATE_TAC (6-2)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MRESA1_TAC th`ww:num->real^3`) THEN ASM_TAC THEN REAL_ARITH_TAC; ASM_TAC THEN ASM_REWRITE_TAC[IN;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39;BBindex_min_v39] THEN REPEAT RESA_TAC THEN SUBGOAL_THEN`(BBindex_v39 s ww) IN IMAGE (BBindex_v39 s) (BBprime_v39 s)` ASSUME_TAC; REWRITE_TAC[IMAGE;IN_ELIM_THM;IN] THEN EXISTS_TAC`ww:num->real^3` THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE (BBindex_v39 s) (BBprime_v39 s))`;`BBindex_v39 s ww`]]);;
end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)