proposition: Lemma proper_chord_ring : proper_ring cr1.
proof: Proof. rewrite Dcr1; have [[|z p] -> //=] := Dr2. by apply: contraTneq dEex => ->; rewrite inE /= rx2. 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)