proposition: Lemma diskF_spoke_ring y : (y \in diskF r) = cface x y.
proof: Proof. apply/andP/idP=> [[/= rF'y /hasP[z rz n'zDy]] | xFy]; last first. split; last first. rewrite /= -{1}[y]edgeK -(fclosed1 (diskN_node r)) diskN_E inE /= Er. by rewrite edgeK xFy. apply/hasP=> -[z]; rewrite Er => xFnz. rewrite -[z]nodeK -cface1r -(same_cface xFy) (same_cface xFnz). by rewrite bridgeless_cface. case/connectP: n'zDy rF'y; set z0 := finv node z. have rfz0: face z0 \in r. by rewrite -(ee z0) Er edgeK -(nnn z0) (f_finv nodeI) cface1r nodeK -Er. case=> [|z1 q] /= z0Dq ->{y}. by case/hasP; exists (face z0); last exact: fconnect1. case/andP: z0Dq => /andP[_ /clinkP[z0nz1 | fz0z1]] z1Dq; last first. case: q z1Dq => [|z2 q]; last by rewrite /dlink /= -fz0z1 rfz0. by rewrite (subsetP (ring_fband r)) // -fz0z1. move: rz z1Dq; rewrite Er {z z0 z0nz1 rfz0}(canRL (f_finv nodeI) z0nz1) nnn. elim: q z1 => //= z q IHq y xFy /andP[/andP[_ /clinkP[ynz | fyz]]]. have rz: z \in r by rewrite Er -ynz. case: q {IHq} => [|z1 q]; last by rewrite /dlink /= rz. by rewrite (subsetP (ring_fband r)). by apply: IHq; rewrite -fyz -cface1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)