proposition: Lemma countable_sub: {subset E <= F} -> countable F -> countable E.
proof: Proof. move=> le_EF [f g fgK]; pose f' (x : [psub E]) := f (pincl le_EF x). pose g' x := obind (insub (sT := [the subType _ of [psub E]])) (omap val (g x)). by exists f' g' => x; rewrite /f' /g' fgK /= valK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap reals