proposition: Lemma smerge2edgeD (G : sgraph) (x y : G) (u v : smerge2 G x y) : ~~ x -- y -> u -- v = [|| val u -- val v, (val u == x) && val v -- y | (val v == x) && val u -- y].
proof: Proof. move => n_xy; rewrite [LHS]/edge_rel/= -![sval _]/(val _). case: (eqVneq (val u) x) => [->|uDx]; case: (eqVneq (val v) x) => [->|vDx] //=. - by rewrite sg_irrefl (negbTE n_xy). - by rewrite orbF ![_ -- val _]sgP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)