proposition: Lemma path_cost_init: forall l init s, fold_left Z.add l (init + s) = init + (fold_left Z.add l s).
proof: Proof. intros. generalize dependent s. induction l. - intros; simpl. trivial. - intros; simpl. rewrite <- Z.add_assoc. rewrite IHl. lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas