fact: Definition fitc (i : subpart_loc) j k (x : G) := k < arity (i G (iter j face x)).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)