proposition: Lemma fcard_adj_max y : ~~ cface x y -> fcard face (predI (adj y) (adj x)) <= 2.
proof: Proof. move=> xA'y; case xAy: (adj01 x y). by rewrite /adj01 (negPf xA'y) in xAy; rewrite (fcard_adj_adj xAy). rewrite {xA'y}leqNgt /(fcard _ _); set axy := predI _ _; apply/negP => axy_gt2. have{axy_gt2} []: {e | 2 < size e & all axy e /\ uniq e}. exists (enum axy); [by rewrite -cardE | split; last exact: enum_uniq]. by apply/allP=> z; rewrite mem_enum. case=> [|z1 [|z2 [|z3 e]]] //= _ [/and4P]; rewrite !inE !negb_or. case=> /and3P[Dz1 yAz1 xAz1] /and3P[Dz2 yAz2 xAz2] /and3P[Dz3 yAz3 xAz3] _. case/and3P=> /and3P[z2'1 z3'1 _] /andP[z3'2 _] _ {axy e}. have{xAy} cross_adj z t: z != t -> froots face z -> froots face t -> adj x z -> adj x t -> adj y z -> adj y t -> adj z t. - move=> /negPf t'z /eqP Dz /eqP Dt xAz xAt yAz /adjP[u yFu uRt]. rewrite -(adjFr uRt) in xAt; rewrite (adjF yFu) adjC // -[u]ee in yAz. move: (adj12_edge xAt xAz yAz). rewrite ee orbC /adj01 -(adjFr yFu) cfaceC -(same_cface yFu) cfaceC. rewrite -/(adj01 x y) xAy cfaceC (same_cface uRt) cfaceC. by rewrite (sameP (rootP cfaceC) eqP) Dz Dt t'z (adjFr uRt). have []: [/\ adj z1 z2, adj z1 z3 & adj z2 z3] by split; apply: cross_adj. move: {y Dz1 Dz2 Dz3 yAz1 yAz2 yAz3 z2'1 z3'1 z3'2 cross_adj} xAz1 xAz2 xAz3. rewrite -!fband_spoke_ring => /hasP[t1 rt1 zFt1] /hasP[t2 rt2 zFt2]. move=> /hasP[t3 rt3 zFt3]. rewrite !(adjF zFt1) (adjF zFt2) (adjFr zFt2) !(adjFr zFt3). move {z1 z2 z3 zFt1 zFt2 zFt3} => t1At2 t1At3 t2At3. have [cycRr /simple_uniq Ur] := andP scycRr. have Ar_xor u v: adj u v -> u \in r -> v \in r -> next r u <> next r v /\ (next r u = v \/ next r v = u). - move=> uAv ru rv; split=> [eq_ruv | ]. have /idP[] := adj_no_cface bridge'G uAv. by rewrite (can_inj (prev_next Ur) eq_ruv). apply/pred2P; apply: contraFT (pred0P (subsetP chordless_spoke_ring _ ru) v). by rewrite !inE uAv rv -(canF_eq (prev_next Ur)) eq_sym negb_or andbT. have{t1At2} [rt2'1 rt1V2] := Ar_xor t1 t2 t1At2 rt1 rt2. have{t1At3} [rt3'1 rt1V3] := Ar_xor t1 t3 t1At3 rt1 rt3. have{Ar_xor t2At3} [rt3'2 rt2V3] := Ar_xor t2 t3 t2At3 rt2 rt3. have [i r1 Dr1] := rot_to rt1. move: min_arity (cycle_next Ur) (Ur). rewrite -size_spoke_ring -(size_rot i) -(rot_cycle i) -(rot_uniq i) {i}Dr1. case: r1 => [|u2 [|u3 [|u4 r1]]] //= _ /and4P[/eqP <- /eqP <- /eqP <- _]. rewrite !negb_or => /andP[/and4P[_ _ /eqP[]]] {u2 u3 u4 r1}. case: rt1V2 rt2V3 rt1V3 rt2'1 rt3'1 rt3'2; first by move=> -> [] -> // [] ->. by move=> Dt1; rewrite Dt1 => [] [-> | Dt2] // [] -> //; rewrite Dt2. 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)