proposition: Lemma one_step_path_Znth: forall (g: LabeledGraph V E DV Z DG) s e, path_cost g (s, e :: nil) = elabel g e.
proof: Proof. intros. unfold path_cost; simpl. apply Z.add_0_l. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas