fact: Definition mgraph_rel Lv Le (G : graph Lv Le) : rel G := fun x y => [exists e, (source e == x) && (target e == y)].
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)