proposition: Lemma path_cost_zero: forall (g: LabeledGraph V E DV Z DG) src, path_cost g (src, []) = 0.
proof: Proof. intros. unfold path_cost; trivial. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas