proposition: Lemma wheel_segment x : cnode z x -> cface (inD (face x)) (inD (face (node x))).
proof: Proof. move=> n_z_x. have [xN nxN] : face x \notin N /\ face (node x) \notin N. by split; apply: wheel_proof; rewrite -?cnode1r. pose enx := edge (node x). have enx_fx : enx = finv face x by apply: faceI; rewrite nodeK f_finv. have f_x_enx : cface x enx by rewrite /enx cface1r nodeK. have enxN : enx \in N by apply/NP; rewrite /enx plain_eq // -cnode1r n_z_x. have [o orbit_fx] : exists o, orbit face (face x) = face x :: o ++ [:: enx; x]. { have/(orbit_rot_iter 2 faceI):= (orbit_prefix (arity3 enx)). rewrite !iterS !iter0 !trajectS [traject _ _ 0]/= [drop]lock. rewrite !(rot1_cons,rcons_cat) /= -/cat enx_fx !f_finv // rcons_cat. by move->; eexists. } have subF : {subset [predI cface x & N] <= [:: enx; x] }. { move => v; rewrite !inE => /andP[f_x_v /NP /orP[n_z_v|n_z_ev]]. - rewrite [v == x]rwT // eq_sym; apply: wlog_neg => xDv. have := cycleG xDv f_x_v. by rewrite (connect_trans _ n_z_v) // cnodeC. - rewrite [v == enx]rwT //= enx_fx -(inj_eq faceI) f_finv // eq_sym. have A : cnode x (edge v) by apply: connect_trans n_z_ev; rewrite cnodeC. rewrite -plain_eq' // -cnode1r in A. rewrite cface1r in f_x_v. apply: contraTT A => eqN. exact: cycleG f_x_v. } have subN : {in face x :: o, forall y, y \notin N}. { move=> y Hy; apply: contraTN (orbit_uniq face (face x)) => yN. rewrite orbit_fx -cat_cons cat_uniq [has _ _]rwT //; apply/hasP; exists y => //. apply: subF; rewrite !inE /= yN cface1 fconnect_orbit orbit_fx. by rewrite -cat_cons mem_cat Hy. } pose w := last (face x) o. have [fpath_o face_w] : fpath face (face x) o /\ face w = enx. { have:= cycle_orbit faceI (face x). rewrite orbit_fx /cycle rcons_path cat_path /=. by rewrite -/w andbT => /andP[/and3P[-> /eqP->]]. } have subN' : {in belast (face x) o, forall y, face y \notin N} by apply: fpath_sub_belast fpath_o subN. have wN : w \notin N by apply/subN; rewrite mem_last. apply: (@connect_trans _ _ (inD w)); last first. - rewrite /inD !insubdT. apply: connect1. rewrite /= -[del_node_face_]/(@face del_node) del_node_faceE. rewrite -val_eqE /= /del_node_face face_w enxN. by rewrite /enx -plain_eq' // finv_f. - apply/connectP; exists (map inD o); last by rewrite last_map. apply: homo_fpath_in fpath_o => y y_o. rewrite /inD insubdT => [|fyN]; first exact/subN'. rewrite insubdT => [|yN]; first exact/subN/mem_belast. apply/val_inj; by rewrite del_node_faceE /del_node_face /= (negPf fyN). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)