proposition: Lemma adjP {x y} : reflect (exists2 z, cface x z & rlink z y) (adj x y).
proof: Proof. apply: (iffP hasP) => [] [z xFz zRy]; by exists z; rewrite // -fconnect_orbit in xFz *. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)