fact: Definition minimum_spanning_forest (t g: EdgeListGG) := labeled_spanning_uforest t g /\ forall (t': EdgeListGG), labeled_spanning_uforest t' g -> Z.le (sum_DE Z.add t 0) (sum_DE Z.add t' 0).
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph