proposition: Lemma gmring_cycle i : scycle rlink (gmring i).
proof: Proof. have Dri := val_gmring i; have Uri: simple (gmring i). apply: map_uniq (end0g \o val) _ _; congr (uniq _): (mring_simple (cm i)). rewrite -Dri -!map_comp; apply: eq_map => u /=; apply/eqP. by rewrite -cface_end0g connect_root. rewrite /scycle cycle_from_next ?simple_uniq // => u. rewrite -(mem_map val_inj) Dri => /(next_cycle (mring_cycle (cm i))). rewrite -Dri (next_map val_inj) ?simple_uniq //= -end0g_face. by rewrite -end0g_node gnode_face /rlink cface_end0g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph order ssralg ssrnum ssrint) fourcolor(hypermap geometry color coloring patch snip grid) fourcolor(matte)