proposition: Lemma intro_pre_hom_ring x p : path rlink x p -> rlink (h (last x p)) (h x) -> {subset x :: p <= ac} -> simple (map h (x :: p)) -> pre_hom_ring x p.
proof: Proof. move=> xRp Lhp p_ac Uhp; split=> //; rewrite /scycle {}Uhp andbT. rewrite /= rcons_path last_map {}Lhp andbT. move/allP: p_ac; elim: p x xRp => //= y p IHp x /andP[xRy yRp] /andP[ac_x p_ac]. have ac_ex: edge x \in ac by rewrite (closed_connect acF xRy); case/andP: p_ac. by rewrite IHp // /rlink -embed_functor ?cface_ac_h. 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)