fact: Definition bad_ring_arity a := match a with 0 | _.+4.+1 => true | _ => false end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)