proposition: Lemma path_cost_upper_bound: forall (g: LabeledGraph V E DV Z DG) src links upper, 0 <= upper -> (forall e, In e links -> elabel g e <= upper) -> path_cost g (src, links) <= Zlength links * upper.
proof: Proof. intros. induction links. - rewrite (path_cost_zero g). apply Z.mul_nonneg_nonneg; rep_lia. - rewrite path_cost_cons. rewrite Zlength_cons. spec IHlinks. 1: intros; apply H0; right; trivial. specialize (H0 a). spec H0. 1: left; trivial. lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas