proposition: Lemma countable_union s s' : countable s -> countable s' -> countable (s ∪₁ s').
proof: Proof. unfold countable at 1 2; ins; desf; vauto. eapply surjection_countable with (f := fun x => if Nat.odd x then nu (Nat.div2 x) else nu0 (Nat.div2 x)). unfold set_union; ins; desf; eapply enumerates_surjection in IN; eauto; desf. exists (2 * i); rewrite Nat.odd_mul, Nat.odd_2, Nat.div2_double; ins. exists (S (2 * i)); rewrite Nat.odd_add_mul_2 with (n := 1), Nat.div2_succ_double; ins. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt