proposition: Lemma nat_list_max : forall (xs : list nat), { n : nat | forall x, List.In x xs -> x <= n }.
proof: Proof. induction xs as [ | x xs [y H] ]. exists 0. inversion 1. exists (max x y). intros z J. simpl in J. destruct J as [K | K]. subst. auto with arith. auto using max_lt_r. Qed.
imports: Coq.Arith.Arith Coq.Arith.Max Coq.Classes.EquivDec Coq.Lists.List Coq.Structures.Equalities Coq.FSets.FSets Metalib.CoqListFacts Metalib.FSetExtra Metalib.FSetWeakNotin Metalib.LibTactics Lia