proposition: Lemma cskip_edge_merge {u v} : ~~ cross_edge -> edom (val u) -> cedge u v = edom (val v).
proof: Proof. move=> not_zEnz edom_u; apply/idP/idP => [uEv | edom_v]. apply: contraLR edom_u => edom'v; apply: etrans (edom'v). by apply: (closed_connect eCedom); rewrite cedgeC -same_cskip_edge // cedgeC. without loss uEz: u v {edom_u} edom_v / cedge (val u) z. move=> IHu; have [/IHu->|uEnz|] // := or3P edom_u. rewrite cedgeC; have [/IHu->|vEnz|] // := or3P edom_v. by rewrite sub_cskip_edge // (connect_trans vEnz) // cedgeC. have{edom_v} [vEz|vEnz|] // := or3P edom_v. by rewrite sub_cskip_edge // (connect_trans uEz) // cedgeC. have z'ez: ez != z. apply: contraL uEz => ez_z; have zEz: fcycle edge [:: z] by rewrite /= ez_z. by rewrite cedgeC (fconnect_cycle zEz) inE ?z'G'. have z'nfz: node (face z) != z by rewrite eq_sym -(canF_eq edgeK). have uEnz: cedge u (inG' z'nfz) by rewrite sub_cskip_edge //= cedge1r faceK. rewrite (connect_trans uEnz) // cedge1 cedgeC sub_cskip_edge //=. rewrite faceK eqxx !ifN -?cedge1r // (contraNneq _ not_zEnz) // => fz_z. by rewrite [cross_edge]cedge1r -(canRL faceK fz_z). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)