proposition: Lemma msf_if_le_msf: forall {E_EqDec : EqDec E eq} (t g: UAdjMatGG), labeled_spanning_uforest t g -> (forall t', minimum_spanning_forest t' g -> sum_DE Z.add t 0 <= sum_DE Z.add t' 0) -> minimum_spanning_forest t g.
proof: Proof. intros. unfold minimum_spanning_forest. split. auto. intros. destruct (exists_msf g) as [msf ?]. apply (Z.le_trans _ (sum_DE Z.add msf 0)). auto. apply H2. auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph