proposition: Lemma acc_pos: forall (g: LabeledGraph V E DV Z DG) l z, (forall e : E, In e l -> 0 <= elabel g e) -> 0 <= z -> 0 <= fold_left Z.add (map (elabel g) l) z.
proof: Proof. intro. induction l; intros; simpl; auto. apply IHl. - intros. apply H. now apply in_cons. - assert (In a (a :: l)) by apply in_eq. specialize (H _ H1). lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas