proposition: Lemma exists_Zmin: forall {A:Type} (l: list A) (f: A -> Z), l <> nil -> exists a, In a l /\ (forall b, In b l -> f a <= f b).
proof: Proof. induction l; intros. contradiction. destruct l. exists a. split. left; auto. intros. destruct H0. subst b. lia. contradiction. assert (exists a : A, In a (a0 :: l) /\ (forall b : A, In b (a0 :: l) -> f a <= f b)). apply IHl. unfold not; intros. inversion H0. destruct H0 as [a' [? ?]]. destruct (Z.le_ge_cases (f a) (f a')). exists a. split. left; auto. intros. destruct H3. subst a; lia. apply H1 in H3. lia. exists a'. split. right; auto. intros. destruct H3. subst b; lia. apply H1 in H3; lia. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver