https://github.com/math-comp/analysis/blob/c56991ba1e47913a65d7dfa5d36afe6ec72542e4/theories/measure.v#L2913