proposition: Corollary partial_lgraph_spanning_mst: forall (t1 t2 g: UAdjMatGG), is_partial_lgraph t1 t2 -> labeled_spanning_uforest t1 g -> minimum_spanning_forest t2 g -> minimum_spanning_forest t1 g.
proof: Proof. intros. split. auto. intros. apply (Z.le_trans _ (sum_DE Z.add t2 0) _ ). apply Z.eq_le_incl. apply (partial_lgraph_spanning_sum_LE t1 t2 g); auto. apply H1. apply H1; 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