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