proposition: Lemma scycle_embd_ring : sfcycle edge embd_ring.
proof: Proof. have UbGdF: simple embd_ring. move: (scycle_simple URerc); rewrite -map_embd_ring. elim: embd_ring => //= u q IHq; rewrite !simple_cons !unfold_in has_map. by rewrite (eq_has (cface_embd u)) => /andP[->]. rewrite /scycle UbGdF andbT; have [UbGd Iemb] := (simple_uniq UbGdF, embd_inj). apply: cycle_from_next => //= u; rewrite -(mem_map Iemb) -(inj_eq Iemb). rewrite -next_map // map_embd_ring /embd /= /embd_edge => /mapP[x rc_x ->{u}]. by rewrite e2c inE /= rc_x (next_map edgeI) //= (eqP (next_cycle cycNrc rc_x)). 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)