proposition: Lemma ring_disk_chord : ~~ chordless bGd -> exists2 r', scycle rlink r' & @nontrivial_ring G 0 r' /\ size r' < size r.
proof: Proof. have Id : injective (snipd : Gd -> G) by apply: inj_snipd. have Dbd : map snipd bGd = r by apply: map_snipd_ring. have Ubd : uniq bGd := ucycle_uniq (ucycle_snipd_ring _ _). case/subsetPn=> xd; rewrite -(mem_map Id) Dbd => rx. case/pred0Pn=> yd /andP[/adjP[zd]]; rewrite [rlink _ _]cface1 -!cface_snipd. rewrite -[snipd (face _)]nodeK -cface1 [node _](congr1 snipd (edgeK zd)) !inE. rewrite -!(inj_eq Id) -(next_map Id Ubd) -(prev_map Id Ubd) -(mem_map Id) {}Dbd. move/snipd: xd rx; move/snipd: yd zd => y [z dNz] x rx /= xFz zRy. rewrite -(canF_eq (prev_next Ur)) -(eq_sym x) => /and3P[x1'y y1'x ry]. have rFz: z \in fband r by apply/hasP; exists x; rewrite // cfaceC. have rFez: edge z \in fband r by apply/hasP; exists y. have dEz: z \in diskE r. rewrite !inE dNz andbT; apply: contra x1'y => rz. rewrite (scycle_cface scycRr rx rz xFz). apply/eqP/(scycle_cface scycRr); rewrite ?mem_next // -(same_cface zRy). exact: (next_cycle cycRr rz). have dEez: edge z \in diskE r by rewrite -(fclosed1 (diskE_edge _ _)). have rF := scycle_fproj scycRr. have rFz_x: fproj r z = x by rewrite -(fproj_cface r xFz) rF. have{rF} rFez_y: fproj r (edge z) = y by rewrite (fproj_cface r zRy) rF. have [|t dFt]:= fcard0P (diskF_face r) _; first by case/andP: nt_r => /subnKC<-. have [dzFt | ] := boolP (t \in diskF (chord_ring z)). exists (chord_ring z); first exact: scycle_chord_ring. by apply: nontrivial_chord_ring; rewrite ?rFz_x ?rFez_y //; exists t. rewrite diskF_chord_ring // inE /= dFt andbT negbK => dezFt. exists (chord_ring (edge z)); first by apply: scycle_chord_ring; rewrite ?ee. by apply: nontrivial_chord_ring; rewrite ?ee ?rFz_x ?rFez_y //; exists t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry patch sew snip color chromogram) fourcolor(coloring kempe)