proposition: Lemma min_arity : 4 < arity x.
proof: Proof. rewrite /= -size_spoke_ring ltnNge; apply: contraL isT => r_le4 /=. have [y dFCy | dCF_0] := pickP [pred y | y \in diskFC r]. rewrite -(Birkhoff _ scycRr) 1?ltnW // eqn_leq andbC ltnNge r_le4 /=. apply/(nontrivial0P _); split; last by exists y. by exists x; rewrite diskF_spoke_ring. case: noncolG; exists (fun y => if cface x y then Color0 else let i := find (cface y) r in if (i == 2) && (size r == 3) then Color3 else if pred2 0 2 i then Color1 else Color2). split=> y /=; last by rewrite -cface1r -(eq_find (cface1 y)) eqxx. set i1 := find (cface y) r; set i2 := find (cface (edge y)) r. case xFy: (cface x y). by rewrite (same_cface xFy) bridgeless_cface //; do 2?case: ifP. case xFey: (cface x (edge y)); first by do 2?case: ifP. have rFy: y \in fband r. apply: contraFT (dCF_0 y) => rF'y; rewrite !inE rF'y. by rewrite -diskF_spoke_ring !inE rF'y /= in xFy; rewrite xFy. have rFey: edge y \in fband r. apply: contraFT (dCF_0 (edge y)) => rF'ey; rewrite !inE rF'ey. by rewrite -diskF_spoke_ring !inE rF'ey /= in xFey; rewrite xFey. pose z1 := nth x r i1; pose z2 := nth x r i2. have z1Az2: adj z1 z2. by apply/adjP; exists y; first rewrite cfaceC; apply: nth_find. have [lti1r lti2r]: i1 < size r /\ i2 < size r by rewrite -!has_find. have [rz1 rz2]: z1 \in r /\ z2 \in r by rewrite !mem_nth. have [cycRr /simple_uniq Ur] := andP scycRr. have{rz1}:= pred0P (subsetP chordless_spoke_ring _ rz1) z2. rewrite !inE {}z1Az2 {}rz2 andbT (eq_sym z2) (canF_eq (prev_next Ur)) /=. have eq_nth_prev i j (lti : i < size r) (ltj : j < size r): (nth x r j == prev r (nth x r i)) = (j == (if i == 0 then size r else i).-1). - suff <-: index (prev r (nth x r i)) r = (if i == 0 then size r else i).-1. by rewrite -(nth_uniq x _ _ Ur) ?nth_index ?index_mem // mem_prev ?mem_nth. rewrite prev_nth mem_nth //; case Dr: r => // [x0 r1] in Ur lti *. rewrite index_uniq ?ltnS ?index_size //; have /=/andP[r1'x0 Ur1] := Ur. case: i => [|i] /= in lti *; last by rewrite index_uniq. by apply/eqP; rewrite eqn_leq index_size leqNgt index_mem. rewrite !{}eq_nth_prev {z1 z2}//. case Dn: (size r) r_le4 lti1r lti2r => [|[|n]] //. by case: r cycRr Dn => [|x0 []] //=; rewrite /rlink cfaceC bridgeless_cface. by case: i1 i2 n {Dn} => [|[|[|[|i1]]]] [|[|[|[|i2]]]] [|[|[|n]]]. 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)