fact: Fixpoint hubcap_fit (p : part) (hc : hubcap) : bool := match hc with | Hubcap1 j b hc' => check_dbound2 (hubcap_rot j p) b && hubcap_fit p hc' | Hubcap2 j1 j2 b hc' => check_2dbound2 (hubcap_rot j1 p) (hub_subn j2 j1) b && hubcap_fit p hc' | Hubcap0 => true end.
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)