proposition: Lemma le_ball (x : M) (e1 e2 : R) : e1 <= e2 -> ball x e1 `<=` ball x e2.
proof: Proof. move=> le12 y. case: comparableP le12 => [lte12 _|//|//|->//]. by rewrite -[e2](subrK e1); apply/ball_triangle/ballxx; rewrite subr_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed