fact: Definition add_edges2_rel := [rel u v : G | u -- v || (u != v) && ((u \in U) && (v \in V) || (u \in V) && (v \in U))].
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)