proposition: Lemma fband_icpY u : {x | cface u (icpY x)} + {cface ecpY u}.
proof: Proof. have [v uFv] := fband_icpN u. have [[x xFv] | XFv] := fband_icpU v; [left | right]. by exists x; rewrite (same_cface uFv) cface_icpN. by rewrite (same_connect_r cfaceC uFv) cface1 cface_icpN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)