proposition: Lemma exclude_arity n : (reducibility -> succeeds_in (pcons_ n) (pcons_ n)) -> excluded_arity n.
proof: Proof. move=> succ_p0_n red G x x_ok; have [cexG _] := x_ok. by apply: contraTF (exact_fitp_pcons_ cexG x) => /eqP->; apply: succ_p0_n. 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)