proposition: Lemma path_cost_app_cons: forall (g: LabeledGraph V E DV Z DG) path e, path_cost g (fst path, snd path +:: e) = path_cost g path + elabel g e.
proof: Proof. intros. replace (fst path, snd path +:: e) with (path_glue path (fst e, [e])). rewrite path_cost_path_glue. rewrite one_step_path_Znth; trivial. unfold path_glue. simpl. trivial. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas