proposition: Lemma adj_ecpY u : adj ecpY u = (u \in fband (map icpY [:: node x0; x0])).
proof: Proof. apply/adjP/hasP => [[v] | [v Dv uFv]]. rewrite cface_ecpY !inE /rlink cface1 cfaceC => /pred2P[] ->{v} XRu. exists (icpY x0); first by rewrite map_f // !inE eqxx orbT. by rewrite /= nodeK (negPf x0gt1) in XRu. by exists (icpY (node x0)); rewrite ?map_f // mem_head. exists (node v); last by rewrite /rlink cface1 nodeK cfaceC. move: Dv; rewrite cface_ecpY !inE => /pred2P[] -> /=; rewrite ?eqxx ?orbT //. by rewrite (negPf x0gt1) /= !eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)