fact: Record minimal_counter_example : Prop := MinimalCounterExample { minimal_counter_example_is_planar_bridgeless_plain_precubic :> planar_bridgeless_plain_precubic G; minimal_counter_example_is_noncolorable : ~ four_colorable G; minimal_counter_example_is_minimal : forall G', planar_bridgeless_plain_precubic G' -> #|G'| < #|G| -> four_colorable G' }.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)