proposition: Lemma set_infinite_natE (s : nat -> Prop) (INF: ~ set_finite s) n : exists m, s m /\ length (filterP s (List.seq 0 m)) = n.
proof: Proof. assert (IMP: forall findom, exists x, s x /\ ~ In x findom). { unfold set_finite in *; apply NNPP; intro X; clarify_not. eapply INF; eexists; ins; apply NNPP; intro Y; eauto. } apply functional_choice in IMP; destruct IMP as [nin IMP]. assert (exists m, s m /\ n <= length (filterP s (List.seq 0 m))). { induction n; desf. 1: exists (nin nil); split; [apply IMP | lia]. exists (nin (List.seq 0 (S m))); split; [apply IMP|]. rewrite seq_split0 with (a := m). rewrite filterP_app, length_app; ins; desf; ins; lia. specialize (IMP (List.seq 0 (S m))); desf. rewrite in_seq0_iff in IMP0; lia. } desf; rewrite Nat.le_lteq in *; desf; eauto. clear - H0; induction m; ins. replace (List.seq 0 0) with (@nil nat) in H0; ins; lia. replace (S m) with (m + 1) in H0; try lia. rewrite seq_add, filterP_app, length_app in H0; ins. replace (List.seq m 1) with (m :: nil) in H0; ins; desf; ins. 1: rewrite Nat.add_1_r, Nat.lt_succ_r, Nat.le_lteq in *; desf; eauto. rewrite Nat.add_0_r in *; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription