proposition: Lemma not_bad_ring_arity (G : hypermap) (x : G) : bad_ring_arity (arity x).-2 = false -> good_ring_arity x.
proof: Proof. by rewrite /good_ring_arity; move: (arity x); do 7!case=> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)