fact: Definition cap_rect r1 r2 := let: Rectangle w1 h1 := r1 in let: Rectangle w2 h2 := r2 in Rectangle (cap_interval w1 w2) (cap_interval h1 h2).
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)