fact: Definition add_edge_rel (G:sgraph) (i o : G) := relU (@edge_rel G) (sc [rel x y | [&& x != y, x == i & y == o]]).
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)