proposition: Lemma no_fit_redpart p : redpart p -> forall x : G, ~~ exact_fitp x p.
proof: Proof. case/andP; move: (qarity_of_nat _) (_ * _) => ahub d /eqP-Ep red_p x. apply: contraL red_p => fit_p; do [have [/eqP<- _] := andP fit_p] in Ep. by elim: d => //= d /not_red_zpart-IHd in x p Ep fit_p *; apply: IHd Ep. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)