fact: Definition proper_ring (r : seq G) : bool := match r with | [:: _, _, _ & _] => true | [:: x; y] => edge x != y | _ => false end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry patch sew snip color chromogram) fourcolor(coloring kempe)