proposition: Lemma red_popl_fan1r_fit pl pr : zvalid pl pr -> forall qa, fitqa (get_fan1r pl) qa -> red_popl_fan1r pl pr -> arity (zdart (Zpart Zfan1r pl pr)) = qa.
proof: Proof. case: pl => // h f => [|f2|f2 f3] pl; rewrite /zvalid /= /zmove /= Dnf. - exact: (red_pcons_fit (updateP6f1 _)). - exact: (red_pcons_fit (updateP7f1 _ _)). 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)