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





module type Khejkci_type = sig
  val KHEJKCI_concl: term
end;;



module Khejkci : Khejkci_type = struct

 let KHEJKCI_concl = `!V k ul. saturated V /\ packing V /\ vor_list V k ul ==>
   ((voronoi_list V ul)   face_of (voronoi_closed V (HD ul)) )`;;

end;;