analysis
analysis copied to clipboard
use `patch` here?
https://github.com/math-comp/analysis/blob/c518e2a302126cbc96a7527e28cac28aaf443822/theories/lebesgue_integral.v#L3420
i.e., f \_ D
instead of f \* \1_ D
?