proposition: Lemma add_edge_proper_separation' (G : sgraph) (V1 V2 : {set G}) x y : proper_separation (add_edge x y) V1 V2 -> proper_separation G V1 V2.
proof: Proof. move => [sepV properV]; split => //. exact: add_edge_separation' sepV. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)