generalization `ball_open` (#1894) #5113

Job	Run time
rocq-core	51s
rocq-elpi	55s
coq-elpi	47s
coq	54s
stdlib	54s
hierarchy-builder	45s
mathcomp-finmap	48s
mathcomp-bigenough	54s
mathcomp	53s
mathcomp-classical	49s
mathcomp-analysis-single	49s
mathcomp-reals	48s
mathcomp-analysis	53s
mathcomp-experimental-reals	1m 0s
mathcomp-reals-stdlib	49s
mathcomp-analysis-stdlib	54s
	13m 43s

Provide feedback