proposition: Lemma card_functions_incr_Nat_aux: countable_set (functions_incr_Nat_aux).
proof: Proof. apply: countable_union; rewrite /allf;aw; first by apply: countable_Nat. move => i iN; rewrite LgV//; apply/countableP; rewrite cpow_pr1. rewrite cardinal_Nat (card_card (CS_succ i)). by apply: (cpow_inf1 _ (NS_succ iN)); apply: CIS_aleph0. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)