https://github.com/math-comp/analysis/blob/3cd35520dc1d14ef272e2c6a25f41a94582ab041/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v#L368
analysis/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
Line 368 in 3cd3552