proposition: Lemma decide_colorable : {four_colorable G} + {~ four_colorable G}.
proof: Proof. case: (decide_ring_trace [::] [::]) => [colG | col'G]; [left | right]. by have [k colk _] := colG; exists k. by case=> k colk; case: col'G; exists k. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)