proposition: Lemma fprojP x : x \in fband -> fproj x \in p /\ cface x (fproj x).
proof: Proof. by move=> pFx; rewrite /fproj mem_nth ?nth_find // -has_find. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)