proposition: Lemma sub_cskip_edge u v : ~~ cross_edge -> cedge (val u) (val v) -> cedge u v.
proof: Proof. have [zGz | /norP[z'ez _]] := boolP (glink z z). by rewrite (eq_fconnect (glink_fp_skip_edge zGz)) fconnect_skip. move=> not_zEnz /connectP[p]; move: {2}_.+1 (ltnSn (size p)) => n lt_p_n. elim: n p => [|n IHn] [|y p] // in u lt_p_n *; first by move=> _ /val_inj->. have [-> | z'y] := eqVneq y z => /=/andP[/eqP-Deu]. case: p => [|ez p] /=/ltnW in lt_p_n *; first by have /eqP := z'G' v. case/andP=> /eqP{ez}<- _ /(IHn p (inG' z'ez))/(connect_trans _)-> //. by rewrite cedgeC not_cross_edge_Walkup // -(canRL edgeK Deu). pose w : G' := inG' z'y => _ /(IHn p w)/(connect_trans _)-> {p lt_p_n}//. have [Dfy | z'fy] := eqVneq (face y) z; last first. by rewrite connect1 //= -val_eqE /= Deu !ifN. suffices: cedge (edge u) (node (face w)) by rewrite -cedge1 cedge1r faceK. have z'nfz: node fz != z by rewrite eq_sym -(canF_eq edgeK). by rewrite not_cross_edge_Walkup //= ?Deu Dfy eqxx !ifN. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)