proposition: Lemma fcard_adj_perimeter x : x \notin ac -> #|predI (cface x) [preim edge of fband rc]| = 2.
proof: Proof. case/negbNE/hasP=> y rc_y xFy. rewrite (cardD1 y) (cardD1 (edge (node y))) !inE xFy cface1r nodeK xFy e2c. have rc_ny: node y \in rc by rewrite -(fclosed1 rcN). case: eqP => [eny_y | _]. by have/norP[]:= edge_perimeter (node y); rewrite eny_y !negbK. have rcFey: edge y \in fband rc. apply/hasP; exists (face (edge y)); last exact: fconnect1. by rewrite (fclosed1 rcN) edgeK. rewrite rcFey (subsetP (ring_fband _)) //=; apply/eqP/existsP=> [[z]]. case/and4P=> eny'z y'z; rewrite {x xFy}(same_cface xFy) => yFz /= rcFez. have bc_z: z \in bc by apply: contra y'z => /(scycle_cface UNrc rc_y)->. have bc_ez: edge z \in bc. apply: contra eny'z => /= rc_ez; apply/eqP/(scycle_cface URerc). - by rewrite -[z]e2c map_f. - exact: map_f. by rewrite cfaceC cface1 nodeK. have/norP[]:= chordless_perimeter bc_z bc_ez. by rewrite !negbK; split=> //; apply/hasP; exists y; rewrite // cfaceC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring patch) fourcolor(snip revsnip kempe birkhoff contract)