proposition: Lemma sum_LE_equiv: forall (g: EdgeListGG) (l: list EType), Permutation (EList g) l -> sum_DE Z.add g 0 = fold_left Z.add (map (elabel g) l) 0.
proof: Proof. unfold sum_LE, DEList; intros. apply fold_left_comm. intros; lia. apply Permutation_map. auto. Qed.
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