proposition: Lemma red_popl_fan3l_fit pl pr : zvalid pl pr -> forall qa, fitqa (get_fan3l pl) qa -> red_popl_fan3l pl pr -> arity (zdart (Zpart Zfan3l pl pr)) = qa.
proof: Proof. case: pl => // [h f1 f2 f3] pl; rewrite /zvalid /= => Ep0r2. move/zvalid_fit: Ep0r2 (Ep0r2); rewrite fitp_catrev /= => /and3P[_ Dn _]. rewrite /zmove /= Dnf (Dfn Dn) /= ?faceK arity_face. exact: (red_pcons_fit (updateP8f1 _ _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)