proposition: Lemma colorable_from_ring et : ring_trace bGd et -> ring_trace bGrd (rev et) -> four_colorable G.
proof: Proof. case/rev_ring_cotrace=> kr col_kr Det tr_etr. apply/(colorable_patch ppGr); exists (rev et) => //; exists kr => //. by rewrite revK Det map_rotr -trace_rot rotrK. 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)