proposition: Lemma sew_map_patch : @patch sew_map _ _ sewd sewr bGd bGr.
proof: Proof. split=> //; first 1 [exact: inj_sewd | exact: inj_sewr | exact: sewr_rev_sewd]. - case=> -[xd | [xr b'xr]]. rewrite -[_ xd]/(sewd xd) !inE codom_f (mem_map inj_sewd) /=. have [[xr0 b_xd] | b'xd] := in_bGd xd. rewrite b_xd; apply/imageP; exists (hdr xr0 xd) => //=. by rewrite (sewr_hdr b_xd). rewrite (negPf b'xd); apply: contraNF b'xd => /imageP[xr _]; rewrite /sewr. by case: (in_bGr xr) => [[xd0 b_xr] | ] //= /inj_sewd->; apply: bGd_hrd. rewrite -[existT _ _ _]/(sewr_r b'xr) !inE -{1}sewr_Gr codom_f. by case: imageP => [[]|]. - by move=> xd b'xd /=; case: (in_bGd xd) => // [[xr0 /=/idPn]]. - move=> xr; rewrite {2}/sewr; case: (in_bGr xr) => [[xd0 b_xr] | ] //=. by case: (in_bGd _) => [[xr0 _] | ] /=; rewrite (hdr_hrd, bGd_hrd). by move=> xr b'xr; rewrite /= (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)