proposition: Lemma red_popl_fan2r_fit pl pr : zvalid pl pr -> forall qa : qarity, fitqa (get_fan2r pl) qa -> red_popl_fan2r pl pr -> arity (zdart (Zpart Zfan2r pl pr)) = qa.
proof: Proof. case: pl => // h f1 f2 => [|f3] pl; rewrite /zvalid /= /zmove /= Dnf. exact: (red_pcons_fit (updateP7f2 _ _)). exact: (red_pcons_fit (updateP8f2 _ _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)