proposition: Corollary partial_lgraph_spanning_sum_LE: forall (t1 t2 g: UAdjMatGG), is_partial_lgraph t1 t2 -> labeled_spanning_uforest t1 g -> labeled_spanning_uforest t2 g -> sum_DE Z.add t1 0 = sum_DE Z.add t2 0.
proof: Proof. intros. assert (Permutation (EList t1) (EList t2)). apply (partial_lgraph_spanning_equiv t1 t2 g); auto. unfold sum_DE. apply fold_left_comm. intros. lia. unfold DEList. replace (map (elabel t1) (EList t1)) with (map (elabel g) (EList t1)). replace (map (elabel t2) (EList t2)) with (map (elabel g) (EList t2)). apply Permutation_map; auto. apply map_ext_in. intros. symmetry; apply H1. rewrite EList_evalid in H3; auto. apply map_ext_in. intros. symmetry; apply H0. rewrite EList_evalid in H3; 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