proposition: Lemma gr_properP (r : grect) : reflect (exists p, r p) (gr_proper r).
proof: Proof. rewrite /gr_proper -size_enum_grect -count_predT -has_count. by apply (iffP hasP) => -[p r_p]; exists p; rewrite ?mem_enum_grect in r_p *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)