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