proposition: Lemma smerge2_path0 (G : sgraph) (x y : G) (s : seq (smerge2 G x y)) : let s0 := [seq val x | x <- s] in path0 (--) s -> x \notin s0 -> path0 (--) s0.
proof: Proof. hnf; case: s => // u s; elim: s u => // v s /= IHs u /= /andP[uv pth_s]. rewrite !inE !negb_or => /and3P[xDu xDv xNs]. by rewrite smerge2_val_edge ?[_ == x]eq_sym // uv /= IHs // inE (negPf xDv). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)