analysis
analysis copied to clipboard
Renaming
https://github.com/math-comp/analysis/blob/1ab682517f25e7f661e3b6dee2453778a535260f/theories/lebesgue_integral_theory/lebesgue_integrable.v#L705-L706
integrable_ltNy seems more appropriate