proposition: Lemma red_pop_fit zp : zpvalid zp -> forall qa, fitqa (zrange zp) qa -> red_pop zp -> arity (zdart zp) = qa.
proof: Proof. case: zp => [[] //= pl pr]; rewrite /zmove /=; try exact: red_popl_spoke_fit. - by rewrite arity_iter_face nFx0 /hub_range /nhub; case ahub => // _ []. - by rewrite Dn2 arity_face; apply: red_popr_spoke_fit. - by rewrite -Dnf !Dn2 arity_face; apply: red_popr_hat_fit. - by rewrite -arity_face nodeK; apply: red_popl_spoke_fit. - by rewrite Dn2 !arity_face; apply: red_popr_spoke_fit. - by rewrite De2 -Dnf !Dn2 !arity_face; apply: red_popr_hat_fit. - exact: red_popl_fan1l_fit. - exact: red_popl_fan2l_fit. - exact: red_popl_fan3l_fit. - exact: red_popl_hat_fit. - exact: red_popl_fan1r_fit. - exact: red_popl_fan2r_fit. exact: red_popl_fan3r_fit. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)