proposition: Lemma red_popl_spoke_fit pl pr : zvalid pl pr -> forall qa, fitqa (get_spoke pl) qa -> red_popl_spoke pl pr -> arity (node (zorg pl)) = qa.
proof: Proof. by case: pl => // [s h|h f1|h f1 f2|h f1 f2 f3] pl; rewrite /zvalid /= Dnf; do [ apply: (red_pcons_fit (updatePs h)) | move/zvalid_fit; rewrite fitp_catrev /= => /and3P[_ /eqP-> _] []]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)