fact: Definition tight_fitp x (up : prange * _) := let (u, p) := up in u (arity x) && fitp x p.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)