proposition: Lemma fold_min_another: forall x al y, fold_right Z.min x (al ++ [y]) = Z.min (fold_right Z.min x al) y.
proof: Proof. intros. revert x; induction al; simpl; intros. apply Z.min_comm. rewrite <- Z.min_assoc. f_equal. apply IHal. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext