proposition: Lemma smerge2edgeL (G : sgraph) (x y : G) (u v : smerge2 G x y) : ~~ x -- y -> val u == x -> val v -- y -> u -- v.
proof: Proof. move=> xNy uEx vy. rewrite /edge_rel/= -![sval _]/(val _) uEx andbF /= vy orbT. case: (eqVneq (val v) x) => // E. by rewrite -E vy in xNy. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)