fact: Definition hub_range := match ahub with | Qa5 => Pr55 | Qa6 => Pr66 | Qa7 => Pr77 | Qa8 => Pr88 | _ => Pr99 end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)