proposition: Lemma Finite_nat_bounded_dec (U : Ensemble nat) (HUdec : forall n : nat, In U n \/ ~ In U n) : (exists n : nat, forall m, In U m -> m < n) -> Finite U.
proof: Proof. intros [n Hn]. eapply Finite_downward_closed_dec. - apply (finite_nat_initial_segment_ens n). - auto. - intros ? ? ? ?. destruct (PeanoNat.Nat.eq_dec x y); [left|right]; auto. - now intros m Hm; red; auto. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)