proposition: Theorem fold_min_general: forall (al: list Z)(i: Z), In i (al) -> forall x, List.fold_right Z.min x al <= i.
proof: Proof. induction al; intros. 1: inversion H. destruct H. 1: subst a; simpl; apply Z.le_min_l. simpl. rewrite Z.le_min_r. apply IHal, H. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext