Merge pull request #1796 from affeldt-aist/lebesgue_integrable_20251212 #1254

Job	Run time
rocq-core	50s
coq	52s
mathcomp-classical	2m 43s
mathcomp-analysis-single	14m 8s
mathcomp-reals	4m 1s
mathcomp-experimental-reals	1m 48s
mathcomp-reals-stdlib	1m 38s
mathcomp-analysis	12m 48s
ssprove	5m 54s
mathcomp-analysis-stdlib	1m 41s
	46m 23s

Provide feedback