fact: Definition diskFC : pred G := [predD [predC diskN] & fband r].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)