proposition: Lemma countable_uniform_bounded (x y : T) : let U := [the pseudoMetricType R of type] in @ball _ U x 2 y.
proof: Proof. rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN. suff -> : @floor R 2^-1 = 0 by rewrite absz0 /=. apply/eqP; rewrite -[_ == _]negbK; rewrite floor_neq0 negb_or -?ltNge -?leNgt. by apply/andP; split => //; rewrite invf_lt1 //= ltrDl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed