(* called azim(x) in text *)

let define_latex (a,b,c) = 


let azimdart = define `azimdart (V,E) (v,w) = 
    azim (vec 0) v w (sigma_fan (vec 0) V E v w)`;;


let cyclic_fan =  `cyclic_fan (V,E,F1) = 
    FANO(V,E) /\
    face_set (hyp_of_fano(V,E)) F1 /\
    (!x.  (F1 x) ==> azimdart (V,E) x <= pi) 
    
`;;