proposition: Corollary msf_if_le_msf': forall {E_EqDec : EqDec E eq} (t t' g: UAdjMatGG), labeled_spanning_uforest t g -> 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. apply msf_if_le_msf; auto. intros. apply (Z.le_trans _ (sum_DE Z.add t' 0)). auto. apply H0. apply H2. 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