proposition: Lemma red_popl_hat_fit pl pr : zvalid pl pr -> forall qa, fitqa (get_hat pl) qa -> red_popl_hat pl pr -> arity (edge (iter 2 face (node (zorg pl)))) = qa.
proof: Proof. case: pl => //= [s h | h f1 | h f1 f2 | h f1 f2 f3] pl; rewrite Dnf /zvalid /=. - exact: (red_pcons_fit (updatePh _)). - exact: (red_pcons_fit (updateP6h _)). - exact: (red_pcons_fit (updateP7h _ _)). exact: (red_pcons_fit (updateP8h _ _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)