proposition: Lemma smerge2_ucycle (G : sgraph) (x y : G) (s : seq (smerge2 G x y)) : let s0 := [seq val x | x <- s] in ucycle (--) s -> x \notin s0 -> ucycle (--) s0.
proof: Proof. hnf; case: s => // z s; rewrite /ucycle/cycle/= => /and3P[pth_s zNs uniq_s xNs]. rewrite map_inj_uniq ?uniq_s ?andbT; last exact: val_inj. rewrite mem_map // zNs andbT -map_rcons. apply: (@smerge2_path0 G x y (z::rcons s z)) => //=. by move: xNs; rewrite !inE map_rcons mem_rcons inE !negb_or andbA andbb. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)