proposition: Lemma red_popl_fan1l_fit pl pr : zvalid pl pr -> forall qa, fitqa (get_fan1l pl) qa -> red_popl_fan1l pl pr -> arity (zdart (Zpart Zfan1l pl pr)) = qa.
proof: Proof. case: pl => // [h f1|h f1 f2|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 (updateP6f1 _)). - exact: (red_pcons_fit (updateP7f2 _ _)). exact: (red_pcons_fit (updateP8f3 _ _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)