proposition: Lemma adjF x1 x2 : cface x1 x2 -> adj x1 =1 adj x2.
proof: Proof. move=> x1Fx2 y; apply: {y}eq_has_r => y. by rewrite -!fconnect_orbit (same_cface x1Fx2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)