fact: Fixpoint pick_target_drules (r : drules) : drules := if r is p :: r' then let: (u, p') := converse_part p in let tr := pick_target_drules r' in if u nhub then p' :: tr else tr else r.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)