proposition: Lemma embed_patch : patch embdd embr embd_ring embr_ring.
proof: Proof. split. - exact: embdd_inj. - exact: embr_inj. - exact: scycle_embd_ring. - exact: ucycle_embr_ring. - exact: map_embr_ring. - move=> x; rewrite codom_embr !inE. apply/imageP/norP=> [[u bGd_u ->] | [/negbNE/imageP[u _ ->]]]. by rewrite codom_f // (mem_map embdd_inj). by rewrite (mem_map embdd_inj); exists u. - exact: embddE. - exact: embddN. - by []. move=> w; rewrite inE /= -(mem_map embr_inj) map_embr_ring /embr /= /embr_node. by case: pickP => //= u /andP[bGd_u /eqP->]; rewrite mem_rev map_f. 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)