proposition: Lemma succeed_by_reducibility : the_redpart p -> succeeds_in p0 p.
proof: Proof. by move=> Hp _ G x [cexG nFx]; apply: no_fit_the_redpart. 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)