proposition: Lemma countable_fun_image z f: countable_set z -> countable_set (fun_image z f).
proof: Proof. move /countableP => h; apply /countableP. exact:(cleT (fun_image_smaller z f) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)