fact: Definition sep_rect z1 z2 := let: Point x1 y1 := z1 in let: Point x2 y2 := z2 in Rectangle (sep_interval x1 x2) (sep_interval y1 y2).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple path fingraph bigop order ssralg) mathcomp(ssrnum ssrint div intdiv) fourcolor(hypermap geometry coloring grid matte) fourcolor(real realplane) Coq(Setoid Morphisms) fourcolor(realsyntax realprop)