proposition: Lemma peano_ensemble_countably_infinite {X : Type} (U : Ensemble X) (o : X) (succ : X -> X) : In U o -> (forall x : X, In U x -> In U (succ x)) -> injective_ens succ U -> (forall x : X, In U x -> o <> succ x) -> (forall P : Ensemble X, P o -> (forall x, In U x -> P x -> P (succ x)) -> forall x, In U x -> P x) -> eq_cardinal_ens (@Full_set nat) U.
proof: Proof. intros HUo HUsucc Hsucc_inj Hsucc_o HUind. right. pose (g := fix g (n : nat) : { n : X | In U n } := match n with | O => exist U o HUo | S n => exist U (succ (proj1_sig (g n))) (HUsucc (proj1_sig (g n)) (proj2_sig (g n))) end). exists (fun n => proj1_sig (g n)). split; [|split]. - intros x Hx. clear Hx. induction x. { simpl. assumption. } simpl. apply HUsucc, IHx. - intros x0 x1 Hx0 Hx1 Hx. clear Hx0 Hx1. revert x1 Hx. induction x0; intros x1 Hx. { simpl in Hx. destruct x1. { reflexivity. } simpl in Hx. apply Hsucc_o in Hx; try contradiction. apply proj2_sig. } simpl in Hx. destruct x1. { simpl in Hx. symmetry in Hx. apply Hsucc_o in Hx; try contradiction. apply proj2_sig. } simpl in Hx. apply Hsucc_inj in Hx; try now apply proj2_sig. apply IHx0 in Hx. congruence. - red. apply HUind. + exists 0. split; constructor. + intros x Hx [y [Hy Hy0]]. subst. exists (S y); split; [constructor|]. simpl. reflexivity. 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)