proposition: Lemma adj_kernel_min x : x \notin ac -> exists2 y, y \in ac & cface x (edge y).
proof: Proof. case/negbNE/hasP=> y rc_y xFy; have:= allP (embeddable_ring embedGc) _ rc_y. rewrite -[_ y]mem_seq4 (mem_iota 3 4) andbC => /andP[_]. rewrite /order -(cardID [preim edge of fband rc]). rewrite fcard_adj_perimeter ?(contraL (@ac_bc _)) // !ltnS lt0n. by case/exists_inP=> z; exists (edge z); rewrite // e2c (same_cface xFy). 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)