proposition: Theorem countable_product f: finite_set (domain f) -> (allf f countable_set) -> countable_set (productb f).
proof: Proof. move=> /NatP fsd alc; apply /countableP. rewrite [X in X <=c _ ]cprod_pr. apply: (@cleT (cprodb (domain f) (fun i =>aleph0))). apply: cprod_increasing; aw; trivial => x xdf. by rewrite !LgV//; move: (alc _ xdf) => /countableP. rewrite cprod_of_same - cpowcr. exact:(cpow_inf1 CIS_aleph0 fsd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)