proposition: Lemma adj_icpU : {mono icpU : x y / adj x y}.
proof: Proof. move=> x y; apply/adjP/adjP => [[[||z] xFz zRy] | [z xFz zRy]]. - by rewrite cfaceC cface_ecpU in xFz. - by rewrite /rlink /= cface_ecpU in zRy. - by exists z; rewrite /rlink -cface_icpU. by rewrite /rlink -!cface_icpU in xFz zRy; exists (icpU z). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)