(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Lemma: CKQOWSA                                                                  *)
(* Chapter: local                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-03-12                                                           *)
(* ========================================================================== *)

flyspeck_needs "general/sphere.hl";;

let tarski_3point_concl = `!v0 v1 v2.   {v0,v1,v2} SUBSET ball_annulus /\
  packing {v0,v1,v2} /\
   dist(v1,v2) <= &2 * h0 /\  ~(v0 IN {v1,v2}) ==>
  (   aff_ge {vec 0} {v0} INTER aff_ge {vec 0 } { v1,v2} = {vec 0})`;;

let tarski_4point_concl = `!v0 v1 v2 v3.  {v0,v1,v2,v3} SUBSET ball_annulus /\
   packing {v0,v1,v2,v3} /\
   dist(v1,v3) <= &2 * h0  /\ dist (v0,v2) <= &2 * h0 /\
   ({v0,v2} INTER {v1,v3} = {}) ==>
   ( aff_ge {vec 0} {v0,v2} INTER aff_ge {vec 0} {v1,v3} = {vec 0})`;;

let CKQOWSA_concl = `!V. packing V /\ V SUBEST ball_annulus ==>
  fan (vec 0,V,ESTD V)`;;