proposition: Lemma path_cost_cons: forall (g: LabeledGraph V E DV Z DG) src links a, path_cost g (src, a :: links) = elabel g a + path_cost g (src, links).
proof: Proof. intros. pose proof (path_cost_path_glue g (src, [a]) (src, links)). unfold path_glue in H. simpl in H. rewrite H. f_equal. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas