proposition: Lemma mem_rev_ring x : (x \in rev_ring r) = (edge x \in r).
proof: Proof. by rewrite -{1}[x]ee mem_rev (mem_map edgeI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry patch sew snip color chromogram) fourcolor(coloring kempe)