proposition: Lemma surjection_countable (f : nat -> A) (s : A -> Prop) (SUR: forall a (IN: s a), exists i, f i = a) : countable s.
proof: Proof. tertium_non_datur (set_finite s); eauto using finite_countable. assert (N: forall i, exists k, i < k /\ s (f k) /\ ~ In (f k) (mk_list (S i) f) /\ forall j, j < k -> s (f j) -> In (f j) (mk_list (S i) f)). { assert (M: forall i, exists a, s a /\ forall j, j <= i -> f j <> a). { ins; apply NNPP; intro X; apply H. exists (mk_list (S i) f); intros; apply in_mk_list_iff. eapply not_ex_all_not with (n:=x) in X; clarify_not; eauto with arith. } intros; specialize (M i); desc. specialize_full SUR; eauto; desf. destruct (le_lt_dec i0 i); [by edestruct M0; eauto|]. revert M M0; rewrite (le_plus_minus (S i) i0); auto with arith. generalize (i0 - S i) as n; intros. exists (S i + findP (fun x => s x /\ ~ In x (mk_list (S i) f)) (mk_list (S n) (fun x => (f (S i + x))))). forward eapply findP_spec with (cond := fun x => s x /\ ~ In x (mk_list (S i) f)) (d := f 0) (l := mk_list (S n) (fun x => (f (S i + x)))) as K; desc; eauto. by apply in_mk_list_iff; eauto. split; try done; rewrite in_mk_list_iff; intro X; desf. by symmetry in X0; eapply M0 in X0; eauto with arith. rewrite nth_mk_list in *; desf. by rewrite in_mk_list_iff in *; destruct K1; eauto with arith. splits; auto with arith; intros; rewrite in_mk_list_iff. destruct (le_lt_dec j i). by exists j; auto with arith. specialize (K0 (j - S i)). rewrite nth_mk_list in K0; desf; [lia|]. rewrite le_plus_minus_r, in_mk_list_iff in K0; auto with arith. apply NNPP; intro; eapply K0; desf; lia. } apply choice in N; destruct N as [g N]. right. assert (MID: forall i, exists k, fexp g k 0 <= i < fexp g (S k) 0). { induction i; ins; unfold fcompose in *; desf. - exists 0; split; ins; apply N. - destruct (eqP (g (fexp g k 0)) (S i)) as [EQ|NEQ]; [exists (S k) |exists k; lia]. split; ins; unfold fcompose; rewrite EQ; ins; apply N. } tertium_non_datur (s (f 0)). { exists (fun x => f (fexp g x 0)); left; splits; ins. by destruct i; ins; apply N. { destruct (lt_eq_lt_dec i j) as [[LT|]|LT]; ins. 1-2: apply lt_funI with (f:=g) (d:=0) in LT; try (by intros; apply N). 1-2: exfalso. - destruct j; ins; unfold fcompose in *; try lia. eapply N with (x := fexp g j 0); rewrite <- EQ. apply N; ins; rewrite EQ; apply N. - destruct i; ins; unfold fcompose in *; try lia. eapply N with (x := fexp g i 0); rewrite EQ. apply N; ins; rewrite <- EQ; apply N. } forward eapply exists_min with (cond := fun k => f k = a) as X; desf; auto. specialize (MID n); desc. rewrite Nat.le_lteq in *; desf; eauto. apply N in MID0; ins. apply in_mk_list_iff with (n := S _) in MID0. exfalso; desc; symmetry in MID1; eapply X0 in MID1; ins; lia. } { exists (fun x => f (g (fexp g x 0))); left; splits; ins. by apply N. { destruct (lt_eq_lt_dec i j) as [[LT|]|LT]; ins. 1-2: apply lt_funI with (f:=g) (d:=g 0) in LT; try (by intros; apply N). 1-2: rewrite !fexpS in *; exfalso. 1: eapply N with (x := fexp g j 0); rewrite <- EQ. 2: eapply N with (x := fexp g i 0); rewrite EQ. 1-2: apply N; ins; apply N. } forward eapply exists_min with (cond := fun k => f k = a) as X; desf; auto. specialize (MID n); desc. rewrite Nat.le_lteq in *; desf; eauto. 2: by destruct k; ins; exists k; ins. apply N in MID0; ins. apply in_mk_list_iff with (n := S _) in MID0. exfalso; desc; symmetry in MID1; eapply X0 in MID1; ins; lia. } Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt