proposition: Lemma add_edge_separation' (G : sgraph) (V1 V2 : {set G}) x y: separation (add_edge x y) V1 V2 -> separation G V1 V2.
proof: Proof. move=> [covV sepV]; split => // u v Hu Hv. by apply: contraFF (sepV _ _ Hu Hv); rewrite [in X in _ -> X]/edge_rel/= => ->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)