https://github.com/math-comp/analysis/blob/3cd35520dc1d14ef272e2c6a25f41a94582ab041/theories/lebesgue_integral_theory/lebesgue_integral_approximation.v#L45 to enhance discoverability