proposition: Lemma fcard_adj_adj y : adj x y -> fcard face (predI (adj y) (adj x)) = 2.
proof: Proof. move=> xAy; have /hasP[y1 ry1 yFy1]: y \in fband r by rewrite fband_spoke_ring. rewrite [fcard _ _](cardD1 (froot face (next r y1))). rewrite (cardD1 (froot face (prev r y1))) !inE !(roots_root cfaceC). have r_xA z: z \in r -> adj x z by rewrite Er => /adjF->; apply: adjN. set z1 := prev r y1; have rz1: z1 \in r by rewrite mem_prev. set z2 := next r y1; have rz2: z2 \in r by rewrite mem_next. rewrite -!(adjFr (connect_root _ _)) !r_xA //=. have [cycRr /simple_uniq Ur] := andP scycRr. rewrite !(adjF yFy1) (rlink_adj (next_cycle cycRr ry1)) adjC //. rewrite (rlink_adj (prev_cycle cycRr ry1)) /= (sameP eqP (rootP cfaceC)). case z1Fz2: (cface z1 z2). case: (rot_to rz1) min_arity (cycle_next Ur) (Ur) => [i r1 Dr]. rewrite -size_spoke_ring -(size_rot i) -(rot_cycle i) -(rot_uniq i) Dr. case: r1 {Dr} => [|y3 [|z3 r3]] // _ /and3P[/= /eqP Dy3 /eqP Dz3 _]. case/andP=> /= /norP[_ /norP[/eqP[]]]; rewrite -Dz3 -Dy3. by rewrite (next_prev Ur); apply: (scycle_cface scycRr). rewrite eq_card0 // => t; apply/and5P=> [] [z1F't z2F't /eqP Dt yAt xAt]. rewrite -Dt !(sameP eqP (rootP cfaceC)) in z1F't z2F't. move: xAt; rewrite -fband_spoke_ring => /hasP[t1 rt1 tFt1]. case/andP: (pred0P (subsetP chordless_spoke_ring _ ry1) t1); split. by rewrite !inE -(adjF yFy1) -(adjFr tFt1). rewrite !inE rt1 andbT; apply/andP; split; apply/eqP => [Dt1]. by rewrite (same_cface tFt1) Dt1 connect0 in z2F't. by rewrite (same_cface tFt1) Dt1 connect0 in z1F't. 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)