proposition: Fact sew_map_subproof : cancel3 sew_edge sew_node sew_face.
proof: Proof. case=> [[xd | [xr b'xr]]] /=. case: (in_bGd xd) => [[xr0 b_xd] | b'xd] /=; last first. case: (in_bGd (edge xd)) => [[xr0 b_exd] | b'exd]; rewrite /= ?edgeK //. by rewrite EbGdE1 in b'xd. set exr := edge (hdr xr0 xd); transitivity (sew_node (sew_face_r exr)). rewrite /sewr; case: (in_bGr exr) => [[xd0 b_exr] | _] //=. by case: (in_bGd _) => [[xr1 _] | ] /=; rewrite (bGd_hrd, hdr_hrd). rewrite /sew_face_r (@sewr_bGr xd); last by rewrite EbGrN1 // edgeK bGr_hdr. by rewrite /= -edge_hrd ?bGr_hdr // edgeK hrd_hdr. transitivity (sew_node (sew_face_r (edge xr))). rewrite /sewr; case: (in_bGr (edge xr)) => [[xd0 b_exr] | b'exr] //=. by case: (in_bGd _) => [[xr0 b_exd] | ] /=; rewrite (hdr_hrd, bGd_hrd). have b'fexr: face (edge xr) \notin bGr. by apply: contra b'xr => /EbGrN <-; rewrite cnode1 edgeK. by rewrite /sew_face_r (sewr_Gr b'fexr) /= edgeK (sewr_Gr b'xr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color patch)