The lemma `ball_ler` looks misnamed to me. I guess it should be `le_ball`. _Originally posted by @CohenCyril in https://github.com/math-comp/analysis/pull/313#discussion_r559716012_