fact: Definition srestrict (G : sgraph) (A : pred G) := Eval hnf in SGraph (restrict_sym A (@sg_sym G)) (restrict_irrefl A (@sg_irrefl G)).
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)