proposition: Lemma lt_size_infinite A (s : A -> Prop) (INF : ~ set_finite s) i : lt_size i s.
proof: Proof. assert (C: forall l, exists x, s x /\ ~ In x l). { ins; apply NNPP; intro X. apply INF; exists l; ins; apply NNPP; eauto. } apply choice in C; desc. set (go := fix go n := match n with | 0 => f nil :: nil | S n => f (go n) :: go n end). exists (go i); splits; induction i; ins; desf; eauto; try apply C; try lia. apply nodup_cons; split; ins; apply C. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt