proposition: Lemma mem_cap_rect r1 r2 p : cap_rect r1 r2 p <-> r1 p /\ r2 p.
proof: Proof. by case: p r1 r2 => x y [w1 h1] [w2 h2] /=; rewrite !mem_cap_interval; tauto. Qed.
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)