fact: Definition contract_ring (G : hypermap) (cc r : seq G) : Prop := [/\ scycle rlink r, proper_ring r & {subset behead r <= insertE cc}].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color coloring patch) fourcolor(snip revsnip birkhoff)