2 (* called azim(x) in text *)
4 let define_latex (a,b,c) =
7 let azimdart = define `azimdart (V,E) (v,w) =
8 azim (vec 0) v w (sigma_fan (vec 0) V E v w)`;;
11 let cyclic_fan = `cyclic_fan (V,E,F1) =
13 face_set (hyp_of_fano(V,E)) F1 /\
14 (!x. (F1 x) ==> azimdart (V,E) x <= pi)