Commit 2021-04-06 05:50 dbb2b558

feat(measure_theory/interval_integral): more on integral_comp (#7030) I replace integral_comp_mul_right_of_pos, integral_comp_mul_right_of_neg, and integral_comp_mul_right with a single lemma.