let add_to_load_path path = if mem path !load_path then () else load_path := path :: !load_path;; let formal_ineqs_dir = flyspeck_dir ^ "/../formal_ineqs";; add_to_load_path formal_ineqs_dir;; needs "arith_options.hl";; Arith_options.base := 100;; Arith_options.cached := false;; needs "arith/nat.hl";;