proposition: Lemma sewr_rev_sewd : map sewr bGr = rev (map sewd bGd).
proof: Proof. apply: canRL (@revK _) _; rewrite -map_rev. have [_ /simple_uniq Ubd] := andP cycEbGd. move: (@sewr_hdr) sz_bG; rewrite /hdr -(size_rev bGr). elim: bGd (rev bGr) Ubd => [|xd pd IHp] [|xr pr] //= /andP[p'xd Upd] Edr [szp]. rewrite -(Edr xr) ?mem_head // eqxx /= {}IHp // => yr0 yd p_yd. by rewrite -(Edr yr0) 1?mem_behead //; case: eqP p'xd => // -> /negP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color patch)