generalization `ball_open` #5111

Job	Run time
rocq-elpi	58s
rocq-core	1m 43s
coq	46s
stdlib	49s
coq-elpi	46s
mathcomp-bigenough	1m 6s
mathcomp-finmap	52s
hierarchy-builder	57s
mathcomp	53s
mathcomp-analysis-single	18m 42s
mathcomp-classical	49s
mathcomp-reals	48s
mathcomp-experimental-reals	29s
mathcomp-reals-stdlib	55s
mathcomp-analysis	15m 37s
mathcomp-analysis-stdlib	16m 57s
	1h 3m 7s

Provide feedback