fact: Fixpoint ctrenum (cp : cprog) : seq (cpmap cp) := match cp with | CpR _ :: cp' => ctrenum cp' | CpY :: cp' => let G := cpmap cp' in if cp' is [::] then [::] else map (icpY G) (node G :: ctrenum cp') | CpH :: cp' => let G := cpmap cp' in face (ecpH G) :: map (icpH G) [:: node G, G : G & ctrenum cp'] | _ => [::] end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)