https://github.com/math-comp/analysis/blob/a0582da47ba6aa1ab4c08b47c1906488a00f961a/theories/lebesgue_integral_theory/simple_functions.v#L249
analysis/theories/lebesgue_integral_theory/simple_functions.v
Line 249 in a0582da