proposition: Lemma ltn_garea_subrect p (r s : grect) : subpred r s -> predD s r p -> (garea r < garea s)%N.
proof: Proof. move=> sub_r_s; rewrite /= -!size_enum_grect -!mem_enum_grect ltnNge. apply: contraL => /uniq_min_size[|q|_ ->]; rewrite ?andNb ?enum_grect_uniq //. by rewrite !mem_enum_grect => /sub_r_s. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)