proposition: Lemma edge_perimeter x : (x \in bc) || (edge x \in bc).
proof: Proof. rewrite -negb_and; apply/andP => [] [/= rc_x rc_ex]. have fxx: face x = x. apply: (scycle_cface UNrc) => //; last by rewrite cfaceC fconnect1. by rewrite (fclosed1 rcN) -(canRL edgeK (e2c x)). have cycFx: fcycle face [:: x] by rewrite /= fxx eqxx. have /idPn[] := allP (embeddable_ring embedGc) _ rc_x. by rewrite /good_ring_arity (order_cycle cycFx) // mem_head. 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)