proposition: Lemma exact_fitp_pcons_ (x : G) : exact_fitp x (pcons_ (arity x)).
proof: Proof. by rewrite /exact_fitp fitp_pcons_; elim (arity x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)