proposition: Corollary nat_Finite_bounded_char (U : Ensemble nat) : Finite U <-> exists n : nat, forall m, In U m -> m < n.
proof: Proof. split. 1: apply nat_Finite_impl_bounded. apply Finite_nat_bounded_dec. intros ?. apply classic. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)