proposition: Lemma adj_kernel_max x : x \notin ac -> #|predI (cface x) [preim edge of ac]| <= 4.
proof: Proof. case/negbNE/hasP=> y rc_y xFy; have:= allP (embeddable_ring embedGc) _ rc_y. rewrite -[_ y]mem_seq4 (mem_iota 3 4) => /andP[_]. rewrite /order -(cardID [preim edge of fband rc]). rewrite fcard_adj_perimeter ?(contraL (@ac_bc _)) //. by congr (_ <= 4); apply: eq_card => z; rewrite !inE (same_cface xFy) andbC. 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)