(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Lemma: DRUQUFE                                                             *)
(* Chapter: Packing                                                           *)
(* Author: Thomas C. Hales                                                    *)
(* Date: Feb 14, 2010                                                         *)
(* ========================================================================== *)

(*
Deprecated Dec 28, 2011. Content moved to pack_concl.hl

The corresponding theorem for `voronoi_open` has been proved by Nguyen Tat Thang.
Hopefully, his proof can be adapted to this context.

The conclusion should be separated into three separate statements for useability.
*)



module type Druqufe_type = sig
  val DRUQUFE_concl : term
end;;



module Druqufe : Druqufe_type = struct

 let DRUQUFE_concl = `!V (v:real^3). packing V /\ saturated V  ==>
     compact (voronoi_closed V v) /\ convex (voronoi_closed V v) /\ measurable (voronoi_closed V v)`;;

end;;