proposition: Lemma red_popr_hat_fit pl pr : zvalid pl pr -> forall qa, fitqa (get_hat pr) qa -> red_popr_hat pr -> arity (Phat G (zorg pl)) = qa.
proof: Proof. case: pr => // [s h | h f1 | h f1 f2 | h f1 f2 f3] pr. - exact: (red_pcons_fit (updatePh s)). - exact: (red_pcons_fit (updateP6h f1)). - exact: (red_pcons_fit (updateP7h f1 f2)). exact: (red_pcons_fit (updateP8h f1 f2 f3)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)