fact: Record forest := Forest { sgraph_of_forest :> sgraph ; forest_is_forest :> is_forest [set: sgraph_of_forest] }.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)