proposition: Lemma red_pcons_fit pc j : part_update pc j -> forall r pl pr, zvalid pl (pc r pr) -> forall qa, fitqa r qa -> red_pcons pc r pr -> arity (j G (zorg pl)) = qa.
proof: Proof. move: j => df Dpcj r pl pr p_ok qa Eqa pc_red; apply: (fitqa_popqa Eqa). have:= zvalid_fit p_ok; rewrite fitp_catrev => /andP[_ fit_pc_r]. set y := iter _ _ x0 in fit_pc_r *. have Ey: arity y = nhub by rewrite /y arity_iter_face. case: (Dpcj r pr) => Epr /(_ G y fit_pc_r)[-> fit_pc]. rewrite orbC -implybE; apply/implyP => Ery. set p0r1 := cat_part (pc (popqa r) pr) p0r. suffices fit_p0r1: exact_fitp y (take_part nhub p0r1). by apply: contraR (not_red_rec Ey fit_p0r1); rewrite /p0r1; case: (r) pc_red. have[[_ x0p0r] Ep0r1] := (andP fit_p0r, cat_take_drop_part nhub p0r1). apply/andP; split. move/eqP: (congr1 size_part Ep0r1); rewrite size_cat_part Ey eq_sym. by rewrite size_drop_part size_cat_part Ep0r addnK addnC eqn_add2r. suffices: fitp y p0r1 by rewrite -{1}Ep0r1 fitp_cat => /andP[]. rewrite fitp_cat fit_pc // -iterD addnC. have [-> _] := Dpcj (popqa r) pr; rewrite -{}Epr -(size_rev_part pl). rewrite -size_cat_part -catrev_part_eq p_ok size_cat_part Ep0r -nFx0. by rewrite iterD !iter_face_arity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)