proposition: Lemma nat_minimal_element_property_dec (U : Ensemble nat) (HUdec : forall n : nat, In U n \/ ~ In U n) (HUinh : Inhabited U) : exists m : nat, In U m /\ forall n : nat, In U n -> m <= n.
proof: Proof. destruct HUinh as [N HN]. revert U HUdec HN. induction N. { intros. exists 0. split; auto. lia. } intros U HUdec HN. destruct (HUdec 0) as [HU0|HU0]. { exists 0. split; auto. lia. } specialize (IHN (compose U S)) as [m [Hm0 Hm1]]; auto. { intros ?. apply HUdec. } destruct (HUdec m) as [HUm|HUm]. { exists m; split; auto; intros n Hn. destruct n; try contradiction. apply Hm1 in Hn. lia. } exists (S m). split; auto. intros n Hn. destruct n; try contradiction. apply le_n_S. apply Hm1. assumption. 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)