proposition: Lemma can_countable : cancel f g -> countable E.
proof: Proof. pose p := choice.pickle \o f; pose u n := omap g (choice.unpickle n). move=> can_fg; apply (@Countable _ E p u) => x. by rewrite {}/u {}/p /= choice.pickleK /= can_fg. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap reals