proposition: Lemma embed_cases x : (x \in ac \/ edge x \in ac) \/ node x \in ac \/ node (edge x) \in ac.
proof: Proof. suffices{x} in_bc x: bc x -> (x \in ac \/ edge x \in ac) \/ node x \in ac. by case/orP: (edge_perimeter x) => /in_bc; rewrite ?e2c; tauto. move=> bc_x; have [rc_ex | bc_ex] := boolP (edge x \in rc); last first. by case: (orP (chordless_perimeter bc_x bc_ex)); tauto. have [rc_enx | bc_enx] := boolP (edge (node x) \in rc); last first. rewrite inE /= (fclosed1 rcN) in bc_x. case: (orP (chordless_perimeter bc_x bc_enx)); first tauto. by rewrite (fclosed1 acF) nodeK; tauto. have rc_fx: face x \in rc by rewrite (fclosed1 rcN) -(canRL edgeK (e2c x)). have Dfx: face x = edge (node x). by rewrite (scycle_cface UNrc rc_fx rc_enx) // -cface1 cface1r nodeK. have EfxF: cface (face x) =i [:: x; face x]. by apply: fconnect_cycle; rewrite ?inE /= ?Dfx ?nodeK !eqxx ?orbT. have:= allP (embeddable_ring embedGc) _ rc_fx. rewrite -[good_ring_arity _]mem_seq4 (mem_iota 3 4). by rewrite /order (eq_card EfxF) ltnNge card_size. 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)