proposition: Lemma wheel_proof x : cnode z x -> face x \notin N.
proof: Proof. Proof using deg2 llG plainG simple. have F := loopless_face _ plainG llG; rewrite cnodeC. move => n_xz; apply: contraTN isT => /NP. have/negPf -> /= : ~~ cnode z (face x). by apply: contraNN (F x); apply: connect_trans. set y := edge _ => n_zy. have E : edge y = face x by rewrite plain_eq. have [xy|xDy] := eqVneq x y. by rewrite -(deg2 (face x)) plain_eq' // {1}xy E. have /simple -/(_ xDy): cnode x y by apply: connect_trans n_zy. by rewrite plain_eq // cnode1r plain_eq' // connect0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)