fact: Record sgraph := SGraph { svertex : finType ; sedge: rel svertex; sg_sym': symmetric sedge; sg_irrefl': irreflexive sedge}.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)