proposition: Lemma fitp_pcons_(x : G) n : fitp x (pcons_ n).
proof: Proof. by elim: n x => [|n IHn] x //=; rewrite !pentaG IHn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)