proposition: Lemma connected_ecpN : connected ecpN.
proof: Proof. apply/eqP/esym; rewrite -(n_comp_connect (@glinkC ecpN) ecpN). have GXe: gcomp ecpN (edge ecpN) by rewrite connect1 ?glinkE. have Gx0: gcomp ecpN (icpN x0) by rewrite connect1 ?glinkF. have Gfex0: gcomp ecpN (icpN (face (edge x0))). by rewrite (same_connect1r glinkC (glinkN _)) in GXe. have Gnx0: gcomp ecpN (icpN (node x0)). case x0gt2: (long_cpring x0); last by move/eqP: x0gt2 => <-. by rewrite (same_connect1 glinkC (glinkN _)) /= x0gt2. apply: eq_n_comp_r => [[||x]]; rewrite !inE ?connect0 //. have [p] := connected_clink x x0 ccG. elim: p x => [|y p IHp] x /= => [_ <- // | /andP[xCy yCp] /(IHp y yCp) Gy]. have{p IHp yCp xCy} [xny | fxy] := clinkP xCy. rewrite (same_connect1r glinkC (glinkN _)) /= -xny in Gy. case: eqP Gy => [yx0 | _]; first by rewrite xny yx0. by case: eqP => // /(canRL nodeK)->. rewrite (same_connect1r (@glinkC ecpN) (glinkF _)) /= fxy. by do 2!case: ifP => // _; apply: connect0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)