proposition: Lemma embed_closure : Kempe_closed embed_cotrace.
proof: Proof. apply: Kempe_map; split; [ split | exact: planar_embr ]. split; first exact: plain_embr. by apply/subsetP=> w; rewrite inE /= mem_rotr; apply: (subsetP cubic_embr w). by rewrite rotr_ucycle; apply: ucycle_embr_ring. 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)