proposition: Lemma add_edge_smallest_vseparator (G : sgraph) (x y : G) (S : {set G}) : x \in S -> y \in S -> smallest (vseparator G) S -> smallest (vseparator (add_edge x y)) S.
proof: Proof. move=> xS yS [sepS smallS]; split => [|U]; first exact: add_edge_vseparator. move/add_edge_vseparator'; exact: smallS. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)