fact: Fixpoint fitp (x : G) (p : part) : bool := let ax := arity (edge x) in let axn n := arity (edge (iter n face (edge x))) in match p with | Pcons s h p' => [&& s (arity (Pspoke G x)), h (arity (Phat G x)) & fitp (face x) p'] | Pcons6 h f1 p' => [&& Pr66 (arity (Pspoke G x)), h (arity (Phat G x)), f1 (arity (Pfan1 G x)) & fitp (face x) p'] | Pcons7 h f1 f2 p' => [&& Pr77 (arity (Pspoke G x)), h (arity (Phat G x)), f1 (arity (Pfan1 G x)), f2 (arity (Pfan2 G x)) & fitp (face x) p'] | Pcons8 h f1 f2 f3 p' => [&& Pr88 (arity (Pspoke G x)), h (arity (Phat G x)), f1 (arity (Pfan1 G x)), f2 (arity (Pfan2 G x)), f3 (arity (Pfan3 G x)) & fitp (face x) p'] | Pnil => true end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)