proposition: Lemma succeed_by_hubcap : let n := size_part p in hubcap_cover n hc && hubcap_fit the_redpart (the_drule_fork n) p hc -> succeeds_in p0 p.
proof: Proof. move=> n fit_hc _ G x [cexG pos_x]. exact: (hubcap_fit_bound cexG (no_fit_the_redpart cexG)) fit_hc. 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)