proposition: Lemma minimal_counter_example_is_cubic : minimal_counter_example -> cubic G.
proof: Proof. move=> cexG; have F'eG := bridgeless_cface cexG. have plainG : plain G := cexG; have nGle3 := precubic_leq cexG. apply/subsetP => /= x _; apply/idPn=> n3'x. have x'nx: node x != x. by apply: contraFneq (F'eG x) => {2}<-; rewrite cface1r nodeK. have nnx: node (node x) = x. apply: contraNeq n3'x => x'n2x; rewrite [x \in _]eqn_leq nGle3 /order. rewrite (cardD1 x) (cardD1 (node x)) (cardD1 (node (node x))) !inE. by rewrite (inj_eq nodeI) x'nx x'n2x -!cnode1r connect0. pose G' := WalkupE x; pose h' (u : G') := val u. pose unx : G' := sub (node x) x'nx; pose G'' := WalkupE unx. pose h'' (w : G'') := val w; pose h := h' (h'' _). have Ih': injective h' := val_inj; have Ih'': injective h'' := val_inj. have Ih: injective h := inj_comp Ih' Ih''. have hF w1 w2: cface w1 w2 = cface (h w1) (h w2). by apply: etrans (fconnect_skip faceI _ _); apply: (fconnect_skip faceI). have hN w1 w2: cnode w1 w2 = cnode (h w1) (h w2). by apply: etrans (fconnect_skip nodeI _ _); apply: (fconnect_skip nodeI). have hN1 w: h (node w) = node (h w). pose nw' := WalkupI unx (node (h w)); pose nw := WalkupI w nw'. have Dnw': h' nw' = node (h w). by rewrite [h' _]WalkupI_eq -{1}nnx (inj_eq nodeI) eq_sym -if_neg (valP w). have Dnw: h nw = node (h w). rewrite {1}/h [h'' _]WalkupI_eq -(inj_eq Ih') Dnw' (inj_eq nodeI). by rewrite eq_sym -if_neg (valP (h'' w)). by rewrite -Dnw; congr h; symmetry; do 2!apply: (valE_skip nodeI). have ltG''G: #|G''| < #|G| by rewrite ltnW // -!card_S_Walkup. have oE_G'' w: order edge w = #|predD1 (cedge (h'' w)) unx|. rewrite /order -(card_image Ih''); apply: eq_card => u; rewrite inE /=. have [u_nx | nx'u] := altP eqP. by apply/imageP => [[wu _ u_wu]]; case/eqP: (valP wu); rewrite -[RHS]u_nx. set wu : G'' := sub u nx'u; rewrite (mem_image Ih'' _ wu) /=. apply: etrans (eq_fconnect (glink_fp_skip_edge _) w wu) _. by rewrite /glink /= -!val_eqE /= nnx !eqxx /= orbT. exact: (fconnect_skip edgeI w wu). have [|k [kE kF]] := minimal_counter_example_is_minimal cexG _ ltG''G. do ?split; last 1 first. - apply/subsetP => [w _]; rewrite !inE; apply: leq_trans (nGle3 (h w)). rewrite /order -(card_image Ih) subset_leq_card //. by apply/subsetP=> _ /imageP[w' cww' ->]; rewrite -[_ \in _]hN. - by do 2!apply: planar_WalkupE; apply: cexG. - apply/existsP=> [[w]]; rewrite -{1}[w]edgeK cface1r hF hN1. by move: (h _) => y; rewrite -{2}[y]nodeK -cface1r F'eG. apply/subsetP => [w _]; rewrite /order_set /in_mem /= oE_G''; set u := h'' w. have [EuNx | Eu'Nx] := boolP (has (cedge (h' u)) [:: x; node x]); last first. rewrite -(eqnP (predT_subset plainG (h w))) -(card_image Ih'). have [/negPf Eu'x Eu'nx] := norP Eu'Nx; rewrite /= orbF in Eu'nx. apply/eqP; apply: eq_card => y. have [-> {y} | x'y] := eqVneq y x; last first. pose v : G' := sub y x'y; rewrite (mem_image Ih' _ v) !inE. case: eqP => [[ynx] | _]; last exact (same_cskip_edge Eu'Nx). by apply/esym/(contraNF _ Eu'nx) => wEy; rewrite /= -ynx. rewrite [x \in cedge _]Eu'x; apply/imageP=> [[[z x'z] _ /= zx]]. by case/eqP: (x'z). have x'Enx: ~~ (cross_edge x). move: EuNx; rewrite /= orbF /cross_edge !(cedgeC (h' u)). rewrite ![cedge _ _]plain_orbit // !inE (negPf x'nx). apply: contraTneq => nx_ex; rewrite nx_ex plain_eq // (negPf (valP u)). by rewrite orbF orbb -nx_ex (valP w). have:= cardD1 unx (cedge u); rewrite [_ \in _](cskip_edge_merge x'Enx EuNx). rewrite /= connect0 orbT -eqSS -add1n => <-. have:= cardUI (cedge x) (cedge (node x)); rewrite -!/(order _ _) -eqSS. rewrite !(eqnP (predT_subset plainG _)) addn2 eq_sym addnC => <-. rewrite eq_card0 ?add0n => [|y]; last first. apply: contraNF x'Enx => /andP[/same_cedge xEy /= neEy]. by rewrite /cross_edge xEy cedgeC. rewrite (cardD1 x) !inE connect0 eqSS /order -(card_image Ih'). apply/eqP/esym/eq_card => y; rewrite !inE; have [-> | x'y] /= := altP eqP. by apply/imageP=> [[[z x'z] _ /esym/eqP/idPn]]. set v : G' := sub y x'y; rewrite (mem_image Ih' _ v). by apply: (etrans (cskip_edge_merge x'Enx EuNx)); rewrite /= orbF !(cedgeC y). case: (minimal_counter_example_is_noncolorable cexG). pose a' x w := cface x (h w). have a'0P y: a' y =1 pred0 -> pred2 x (node x) y. move=> a'y0; apply/norP => [[x'y nx'y]]; pose uy : G' := sub y x'y. by case/idP: (a'y0 ((sub uy : _ -> G'') nx'y)); apply: connect0. have a'F y z: a' y =1 pred0 -> cface y z -> y = z. move=> a'y0 yFz; suffices: pred2 y (node y) z. by case/pred2P=> // zny; rewrite -[y]nodeK -zny -cface1 cfaceC F'eG in yFz. have: pred2 x (node x) z. by apply a'0P => w; rewrite /a' -(same_cface yFz) -a'y0. by case/pred2P: (a'0P _ a'y0) => -> /pred2P[]-> /=; rewrite ?nnx ?eqxx ?orbT. pose k' y := oapp k (ccons false (y == x)) (pick (a' y)). have kFF w w': cface w w' -> k w = k w'. case/connectP=> p wFp ->{w'}; elim: p w wFp => //= _ p IHp w /andP[/eqP <-]. by move/IHp <-; rewrite (eqcP (kF w)). have k'F y z: cface y z -> k' y = k' z. rewrite /k' => yFz; case: pickP => [w yFw | a'y0]; last first. by rewrite -(a'F y z) //; case: pickP => // w yFw; case/idP: (a'y0 w). rewrite /a' (same_cface yFz) in yFw; case: pickP => [w' zFw' | /(_ w)/idP//]. by apply: kFF; rewrite hF -(same_cface yFw). have k'E y: ~~ (pred2 x (node x) y) -> k' y != k' (edge y). case/norP=> [x'y nx'y]; pose w := (sub (sub y x'y : G') : _ -> G'') nx'y. have Dfey: (face (edge y) = h (face (edge w))). by apply: nodeI; rewrite -hN1 !edgeK. rewrite (k'F (edge y) _ (fconnect1 _ _)) /k'. case: pickP => [w' yFw' | /(_ w)]; last by rewrite /a' connect0. case: pickP => [w'' feyFw'' /= | /(_ (face (edge w)))]; last first. by rewrite /a' Dfey connect0. apply: contraFneq (kE w) => eq_kw; rewrite /= -(eqcP (kF _)); apply/eqP/esym. by apply: (etrans (etrans _ eq_kw)); apply: kFF; rewrite hF // -Dfey cfaceC. exists k'; split=> y; last by apply/eqP/k'F; rewrite cfaceC fconnect1. have [Dy | /k'E/negPf] := boolP (pred2 x (node x) y); last by rewrite eq_sym. have eey := plain_eq cexG y. have [Dey|/k'E/negPf] := boolP (pred2 x (node x) (edge y)); last by rewrite eey. rewrite /k' /= eq_sym; case: pickP => [w yFw /= | a'y0]. suffices cycFy: fcycle face [:: y]. rewrite /a' [cface y _](fconnect_cycle cycFy) ?mem_head // inE in yFw. by case/norP: Dy; rewrite -(eqP yFw) (valP (h'' w)) (valP w). suffices: pred2 y (node y) (face y). rewrite /= andbT orbC [_ == _](contraFF _ (F'eG (node y))) //. by move/eqP=> fn_y; rewrite 2!cface1r nodeK fn_y. have: pred2 x (node x) (face y). by rewrite -eey /= !(canF_eq (canF_sym nodeK)) nnx orbC. by case/pred2P=> ->; case/pred2P: Dy => ->; rewrite /= ?nnx eqxx ?orbT. case: pickP => [w eyFw | a'ey0]. suffices cycFey: fcycle face [:: edge y]. rewrite /a' [cface _ _](fconnect_cycle cycFey) ?mem_head // inE in eyFw. by case/norP: Dey; rewrite -(eqP eyFw) (valP (h'' w)) (valP w). suffices: pred2 (edge y) (node (edge y)) (face (edge y)). rewrite /= andbT orbC [_ == _](contraFF _ (F'eG (node (edge y)))) //. by move/eqP=> fn_ey; rewrite 2!cface1r nodeK fn_ey. have: pred2 x (node x) (face (edge y)). by rewrite /= !(canF_eq (canF_sym nodeK)) nnx orbC. by case/pred2P=> ->; case/pred2P: Dey => ->; rewrite /= ?nnx eqxx ?orbT. apply/eqP; move: Dy => /=; case: eqP => [-> | _]; first by rewrite plain_neq. by move/eqP=> ynx; rewrite (a'F _ x a'ey0) ?eqxx // cface1 ynx nodeK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)