proposition: Lemma no_fit_the_redpart G : minimal_counter_example G -> forall (x : G) p', the_redpart p' -> ~~ exact_fitp x p'.
proof: Proof. move=> cexG x p1 redp1; apply: (no_fit_redpart cexG) p1 redp1 x => x. move Dq: the_quiz_tree => q. have{q Dq} <-: cfquiz_tree the_configs = q by exact <: Dq. have:= red_check; rewrite /reducibility; move Dcfs: the_configs => cfs red_cfs. apply/negP; case/(qzt_fit_cfquiz cexG)=> [cf ltcf [qz fit_qz [cf_ok [u qz_u]]]]. wlog{x fit_qz} [x fit_qz]: G cexG / exists x : G, fitqz x qz. move=> IH; case: fit_qz; apply: IH; first exact: cexG. exact: minimal_counter_example_mirror. have red_cf: cfreducible (nth cf000 cfs cf). by have:= red_check (leq0n cf); rewrite Dcfs => /(_ ltcf). have embedG := quiz_preembedding cexG cf_ok qz_u fit_qz. exact: not_embed_reducible cexG cf_ok embedG red_cf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph bigop ssralg ssrnum ssrint) fourcolor(hypermap geometry patch coloring birkhoff embed) fourcolor(quiz quiztree part redpart discharge hubcap) fourcolor(cfmap cfcontract cfreducible configurations)