proposition: Lemma adjFr y1 y2 : cface y1 y2 -> forall x, adj x y1 = adj x y2.
proof: Proof. move=> y1Fy2 x; apply: {x}eq_has => x. by rewrite /rlink !(cfaceC (edge x)) (same_cface y1Fy2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)