proposition: Lemma path_cost_glue_one_step: forall (g: LabeledGraph V E DV Z DG) p2m u i, path_cost g (path_glue p2m (u, [(u, i)])) = path_cost g p2m + elabel g (u, i).
proof: Proof. intros. rewrite path_cost_path_glue, one_step_path_Znth; trivial. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas