proposition: Lemma nat_Finite_impl_bounded (U : Ensemble nat) : Finite U -> (exists n : nat, forall m, In U m -> m < n).
proof: Proof. intros HU. induction HU. { exists 0. intros ? ?. contradiction. } destruct IHHU as [n0 Hn0]. exists (max n0 (S x)). intros m Hm. destruct Hm. - specialize (Hn0 x0 H0). lia. - destruct H0. lia. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)