proposition: Lemma mem_sep_rect z1 z2 : sep_rect z1 z2 z2.
proof: Proof. by case: z1 z2 => [x1 y1] [x2 y2]; split; apply: mem_sep_interval. 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)