fact: Definition display_obstacles_and_cells (tr_x tr_y scale : Q) (bottom top : edge) (obstacles : seq edge) (cells : seq cell) : seq string := (List.map (display_edge tr_x tr_y scale) (bottom :: top :: obstacles) ++ "stroke"%string :: display_cell_centers tr_x tr_y scale cells ++ "stroke gsave [1 3] 0 setdash"%string :: List.map (fun c : cell => display_cell 300 400 70 c) cells ++ " stroke grestore "%string :: nil).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL