proposition: Lemma fitqzp_fit zp q : fitqzp zp q -> red_popqzp zp q -> zpvalid zp -> fitq (zdart zp) q.
proof: Proof. elim: q zp => //=. - move=> qa zp Eqa red_zp zp_ok. by apply/eqP; rewrite /= (red_pop_fit zp_ok Eqa red_zp). - move=> qa ql IHq zp; case: ifP => // Eqa fit_ql /andP[red_zp red_ql] zp_ok. have Dqa := red_pop_fit zp_ok Eqa red_zp; rewrite /fitq /= eqseq_cons Dqa. rewrite eqxx andTb; have [<- // | zpLok] := fitqzp_proper fit_ql. move: Eqa; rewrite fitqa_topqa -{qa}Dqa => /andP[_ /eqP Eqa]. by rewrite -zdart_stepLt //; apply: IHq => //; apply zpvalid_stepLt. - move=> qa qr IHq zp; case: ifP => // Eqa fit_qr /andP[red_zp red_qr] zp_ok. have Dqa := red_pop_fit zp_ok Eqa red_zp; rewrite /fitq /= eqseq_cons Dqa. rewrite eqxx andTb; have [<- // | zpRok] := fitqzp_proper fit_qr. move: Eqa; rewrite fitqa_topqa -{qa}Dqa => /andP[_ /eqP Eqa]. by rewrite -zdart_stepRt //; apply: IHq => //; apply zpvalid_stepRt. - move=> qa ql IHql qr IHqr zp; case: ifP => // Eqa. case: ifP => // fit_ql fit_qr /and3P[red_zp red_ql red_qr] zp_ok. rewrite /fitq /= eqseq_cons fitq_cat (red_pop_fit zp_ok Eqa) ?eqxx //=. apply/andP; split. have [<- // | zpLok] := fitqzp_proper fit_ql. by rewrite -zdart_stepL // IHql //; apply: zpvalid_stepL. have [<- // | zpOrk] := fitqzp_proper fit_qr. by rewrite -zdart_stepR // [_ == _]IHqr //; apply: zpvalid_stepR. - move=> qa ql IHq zp; set zpl := zstepL zp. case: ifP => // Eqa fit_ql /andP[red_zp red_ql] zp_ok. rewrite /fitq /= eqseq_cons -arity_face nodeK. rewrite -zdart_stepL // -/zpl; last by case: (zpl) Eqa => [[]]. have{zp_ok} zpLok := zpvalid_stepL zp_ok. rewrite /zpl (red_pop_fit _ Eqa) // eqxx. have [<- // | zpLproper] := fitqzp_proper fit_ql. by rewrite -zdart_stepL // [_ == _]IHq //; apply: zpvalid_stepL. move=> qa ql IHq zp; set zpr := zstepR zp. case: ifP => // Eqa fit_qr /andP[red_zp req_qr] zp_ok. rewrite /fitq /= eqseq_cons -zdart_stepR // -/zpr; last first. by case: (zpr) Eqa => [][]. have{zp_ok} zpRok := zpvalid_stepR zp_ok. rewrite /zpr (red_pop_fit _ Eqa) // eqxx. have [<- // | zpRproper] := fitqzp_proper fit_qr. by rewrite -zdart_stepR // [_ == _]IHq => //; apply: zpvalid_stepR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)