proposition: Lemma atom_fresh_for_list : forall (xs : list nat), { n : nat | ~ List.In n xs }.
proof: Proof. intros xs. destruct (nat_list_max xs) as [x H]. exists (S x). intros J. lapply (H (S x)). lia. trivial. 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