proposition: Lemma nontrivial_chord_ring : x2 != next r x1 -> (exists y, diskF cr1 y) -> nontrivial_ring 0 cr1 /\ size cr1 < size r.
proof: Proof. rewrite -(next_rot ix Ur) -(size_rot ix r) Dr. have [[|x3 p1] Dp1] := Dr1; rewrite Dp1. by have [p2 ->] := Dr2; rewrite /= !eqxx. move=> _ nt_cr1F; split; last by rewrite size_cat Dcr1 /= !addSnnS leq_addl. have r1x3: x3 \in r1 by rewrite Dp1 mem_behead // mem_head. apply/nontrivial0P; split=> //; exists x3; apply/andP; split=> /=; last first. by rewrite inE /= diskN_chord_ring inE /= diskN_E Dcr2 mem_behead. have r_x3: x3 \in r by rewrite Dr12 !inE r1x3. have:= Ur; rewrite -(rot_uniq ix) Dr Dcr1 Dp1 /= mem_cat orbC inE. apply: contraL; rewrite fband_cons cfaceC (same_cface xFx1). case/orP=> [|/hasP[y r2y]] /(scycle_cface scycRr)->; rewrite ?eqxx //. by rewrite r2y andbF. by rewrite Dr12 !inE r2y orbT. 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)