proposition: Lemma Forall_fold_min: forall (f: Z -> Prop) (x: Z) (al: list Z), f x -> Forall f al -> f (fold_right Z.min x al).
proof: Proof. intros. induction H0. simpl. auto. simpl. unfold Z.min at 1. destruct (Z.compare x0 (fold_right Z.min x l)) eqn:?; auto. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext