proposition: Lemma smerge2_val_edge (G : sgraph) (x y : G) (u v : smerge2 G x y) : val u != x -> val v != x -> val u -- val v = u -- v.
proof: Proof. move: u v => [u uDy] [v vDy] /= uDx vDx. by rewrite [RHS]/edge_rel/= (negbTE uDx) (negbTE vDx). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)