proposition: Lemma minimal_counter_example_is_connected : forall G, minimal_counter_example G -> connected G.
proof: Proof. move=> G cexG; apply/idPn => cc'G. apply: (minimal_counter_example_is_noncolorable cexG). case: (pickP G) => [z _| no_z]; last first. by exists (fun _ => Color0); split=> x; have:= no_z x. have ppG := patch_gcomp z; have minG := minimal_counter_example_is_minimal cexG. have: planar G := cexG; rewrite (planar_patch ppG) => /andP[planarGd planarGr]. have [bridge'Gd bridge'Gr] := patch_bridgeless ppG cexG. have: plain G := cexG; rewrite (plain_patch ppG) => /andP[plainGd plainGr]. have: cubic G := cexG; rewrite (cubic_patch ppG) => /andP[cubicGd cubicGr]. move/cubic_precubic in cubicGd; move/cubic_precubic in cubicGr. apply/(colorable_patch ppG); exists nil. have [//||k colk] := minG (gcomp_disk z); last by exists k. rewrite card_sub (ltn_leqif (subset_leqif_card (subset_predT _))). apply: contra cc'G => /predT_subset allGz; rewrite -(n_comp_connect glinkC z). exact/eqP/esym/eq_n_comp_r. have [//||k colk] := minG (gcomp_rem z); last by exists k. rewrite card_sub (ltn_leqif (subset_leqif_card (subset_predT _))). by apply/negP=> /predT_subset/(_ z); rewrite !inE connect0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)