fact: Fixpoint check_unfit (p : part) (ru : drules) : bool := if ru is r :: ru' then if cmp_part p r is Psubset then true else check_unfit p ru' else false.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry quiztree part discharge)