proposition: Theorem nat_unbounded_impl_countably_infinite_dec (U : Ensemble nat) (HU : forall n : nat, exists m : nat, In U m /\ n < m) (HUdec : forall n : nat, In U n \/ ~ In U n) : eq_cardinal_ens U (@Full_set nat).
proof: Proof. assert (exists u : nat, In U u /\ (forall n : nat, In U n -> u <= n)) as Hu. { specialize (HU 0) as [m [Hm0 Hm1]]. apply nat_minimal_element_property_dec; auto. exists m. assumption. } assert (exists f : nat -> nat, (forall n : nat, In U n -> In U (f n)) /\ (forall n : nat, In U n -> n < f n) /\ (forall n : nat, In U n -> forall m : nat, In U m -> n < m -> f n <= m)) as Hf. { cut (forall n : nat, { fn : nat | (In U n -> In U fn /\ n < fn /\ forall m : nat, In U m -> n < m -> fn <= m) /\ (~ In U n -> fn = 0) }). { intros F. exists (fun n => proj1_sig (F n)). repeat split; intros n Hn; pose proof (proj1 (proj2_sig (F n)) Hn) as [Hn0 [Hn1 Hn2]]; auto. } intros n. apply constructive_definite_description. destruct (HUdec n) as [Hn0|Hn0]. 2: { exists 0. repeat split; try contradiction. intuition. } destruct (nat_minimal_element_property_dec (fun m => In U m /\ n < m)) as [k [[Hk0 Hk1] Hk2]]. { unfold In. intros m. destruct (Nat.lt_ge_cases n m). 2: { right. intros []. lia. } specialize (HUdec m) as [|]. - left; tauto. - right; intros []; tauto. } { destruct (HU n) as [m Hm]. exists m. assumption. } exists k. repeat split; try tauto. { firstorder. } intros l [Hl _]. specialize (Hl Hn0) as [Hl0 [Hl1 Hl2]]. specialize (Hk2 l (conj Hl0 Hl1)). specialize (Hl2 k Hk0 Hk1). lia. } destruct Hu as [u [Hu0 Hu1]]. destruct Hf as [f [Hf0 [Hf1 Hf2]]]. assert (forall x : nat, In U x -> u <> f x) as Hfu. { intros x Hx. specialize (Hu1 x Hx). specialize (Hf1 x Hx). lia. } assert (injective_ens f U) as Hf_inj. { intros x0 x1 Hx0 Hx1 Hx. destruct (Nat.lt_trichotomy x0 x1) as [Hxx|[Hxx|Hxx]]; auto. - specialize (Hf2 x0 Hx0 x1 Hx1 Hxx). specialize (Hf1 x1 Hx1). lia. - specialize (Hf2 x1 Hx1 x0 Hx0 Hxx). specialize (Hf1 x0 Hx0). lia. } assert (forall x : nat, In U x -> x = u \/ exists y : nat, In U y /\ x = f y) as HU0. { intros x Hx. destruct (Nat.eq_dec x u); auto. right. unshelve epose proof (nat_bounded_ens_has_max_dec (fun y => In U y /\ y < x) _ x) as [y Hy]. - intros k. unfold In. destruct (Nat.lt_ge_cases k x). 2: { right. intros []. lia. } specialize (HUdec k) as [|]. + left; tauto. + right; intros []; tauto. - intros k [Hk0 Hk1]. auto. - exists u. split; auto. specialize (Hu1 x Hx). lia. - exists y. split; try apply Hy. destruct Hy as [[Hy0 Hy1] Hy2]. unfold In at 1 in Hy2. apply Nat.le_antisymm. 2: now apply Hf2; auto. apply Nat.nlt_ge. intros Hfy. specialize (Hy2 (f y) (conj (Hf0 y Hy0) Hfy)). specialize (Hf1 y Hy0). lia. } assert (forall P : (forall x : nat, Prop), P u -> (forall (x : nat) (Hx : In U x), P x -> P (f x)) -> forall (x : nat), In U x -> P x) as HUind. { intros P HP0 HP1 x. apply (Wf_nat.lt_wf_rect x (fun x => In U x -> P x)). clear x. intros x Hind Hx. destruct (HU0 x Hx) as [Hx0|[y [Hy Hy0]]]; subst; auto. } apply eq_cardinal_ens_sym_dec. { left. constructor. apply 0. } { assumption. } apply peano_ensemble_countably_infinite with u f; auto. 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)