proposition: Lemma mem_enum_grect r p : (p \in enum_grect r) = r p.
proof: Proof. case: r p => [x0 x1 y0 y1] [x y] /=; rewrite -!mem_zspan. by apply/allpairsP/andP=> [[xy [r_x r_y [-> ->]]]|[]]; last exists (x, y). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)