proposition: Lemma connected_ecpU : connected ecpU.
proof: Proof. apply/eqP/esym; rewrite -(n_comp_connect (@glinkC ecpU) ecpU). have GXe: gcomp ecpU (edge ecpU) by apply: connect1; apply: glinkE. have Gnnx0: gcomp ecpU (icpU (node (node x0))). by rewrite 2!(same_connect1 glinkC (glinkN _)) /=. apply: eq_n_comp_r => [[||x]]; rewrite !inE ?connect0 //. have [p] := connected_clink x (node (node x0)) ccG. elim: p x => [|y p IHp] x /= => [_ <- // | /andP[xCy yCp] /(IHp _ yCp) Gy]. have{p IHp yCp xCy} [xny | fxy] := clinkP xCy. rewrite (same_connect1r glinkC (glinkN _)) /= -xny in Gy. by case: eqP Gy => // ynx0 _; rewrite xny ynx0. by rewrite (same_connect1r (@glinkC ecpU) (glinkF _)) /= fxy; case: ifP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)