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





module type Idbezal_type = sig
  val IDBEZAL_concl : term
end;;



module Idbezal : Idbezal_type = struct

 let IDBEZAL_concl = `!V ul k F.  saturated V /\ packing V /\ vor_list V k ul /\ (k < 3) ==>
   (F facet_of voronoi_list V ul <=>
        (?vl. (F = voronoi_list V vl) /\ vor_list V (k+1) vl /\ (truncate_simplex k vl = ul)))`;;

end;;