proposition: Lemma adj12_edge y z : adj x y -> adj x z -> adj z (edge y) -> adj01 z y || adj01 x (edge y).
proof: Proof. rewrite -2!fband_spoke_ring => /hasP[y1 ry1 yFy1] /hasP[z1 rz1 zFz1]. case/adjP=> x1 zFx1; rewrite /rlink cfaceC => eyFex1. apply/norP=> [] [/norP[zF'y zA'y] /norP[xF'ey xA'ey]]. rewrite !(same_cface zFz1) in zF'y zFx1; rewrite {z zFz1}(adjF zFz1) in zA'y. pose q := [:: y; edge x1; edge (node z1); node y1]. have scycRq: scycle rlink q. rewrite srcycleI //= eyFex1 cface1r nodeK cfaceC zF'y !ee /= andbT. rewrite (same_cface yFy1) cfaceC (adj_no_cface geoG (adjN y1)) /=. rewrite cface1r nodeK cfaceC zFx1 -(same_cface eyFex1) cfaceC. rewrite !Er in ry1 rz1; rewrite -(same_cface ry1) xF'ey. by rewrite -(same_cface rz1) ry1 cface1 nodeK cfaceC yFy1. apply: (elimF (nontrivial0P _) (Birkhoff _ scycRq) _) => //; split. exists (node (node y1)); rewrite !inE -(fclosed1 (diskN_node q)). rewrite diskN_E !inE eqxx /= !orbT andbT // unfold_in /= orbF. rewrite cfaceC (same_cface yFy1) -{2 4}[y1]edgeK nnn -cface1r. rewrite bridgeless_cface // cfaceC -(same_cface eyFex1) (no_adj_adj xA'ey). rewrite -cface1 cfaceC cface1 nodeK; rewrite adjC // in zA'y. rewrite (no_adj_adj zA'y); first by rewrite adj_no_cface ?adjN. by rewrite (adjF yFy1) adjE. by rewrite Er in ry1; rewrite (adjF ry1) adjC ?adjN. exists (node (node z1)); rewrite !inE -(fclosed1 (diskN_node q)). rewrite -{2}[node z1]ee (diskN_edge_ring geoG) //= ?inE ?eqxx ?orbT //. rewrite unfold_in /= andbT orbF -{1 3}[z1]edgeK nnn -cface1 cfaceC. rewrite (no_adj_adj zA'y (adjE z1)); rewrite !Er in ry1 rz1. rewrite cfaceC -(same_cface eyFex1) (no_adj_adj xA'ey) /=. rewrite -cface1 cfaceC cface1 nodeK bridgeless_cface //. rewrite cfaceC -(same_cface ry1) (same_cface rz1) -{1}[node z1]nodeK -cface1. by rewrite cfaceC bridgeless_cface. by rewrite (adjF rz1) adjC ?adjN. 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)