proposition: Lemma meet_sep_rect z1 z2 : meet (sep_rect z1 z2) (sep_rect z2 z1) -> forall rr : rectangle, rr z1 -> rr z2.
proof: Proof. case: z1 z2 => x1 y1 [x2 y2] [[x y] [[x12x y12y] [x21x y21y]]] [[? ?] [? ?]] /=. by rewrite (meet_sep_interval x12x x21x) (meet_sep_interval y12y y21y). 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)