proposition: Lemma disjoint_gmdisk i j : i != j -> [disjoint diskN (gmring i) & diskN (gmring j)].
proof: Proof. apply/contraR=> /exists_inP[/= u mi_u mj_u]; apply/eqP/cmP/hasP. by exists (halfg u); apply: gm_disk_def. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph order ssralg ssrnum ssrint) fourcolor(hypermap geometry color coloring patch snip grid) fourcolor(matte)