proposition: Theorem fold_min: forall (al: list Z)(i: Z), In i (al) -> List.fold_right Z.min (hd 0 al) al <= i.
proof: Proof. intros. apply fold_min_general, H. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext