proposition: Lemma nat_bounded_ens_has_max_dec (U : Ensemble nat) (HUdec : forall n : nat, In U n \/ ~ In U n) (N : nat) : (forall n : nat, In U n -> n < N) -> Inhabited U -> exists n : nat, In U n /\ forall m : nat, In U m -> m <= n.
proof: Proof. intros HN HU. induction N. { destruct HU as [u Hu]. specialize (HN u Hu). lia. } clear HU. specialize (HUdec N) as [HN0|HN0]. - exists N; split; auto. intros m Hm. specialize (HN m Hm). lia. - apply IHN. intros n Hn. specialize (HN n Hn). assert (n <> N). { intros ?; congruence. } lia. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)