Theorem interval_integral.integral_pos_iff_support_of_nonneg_ae'

fix(measure_theory/interval_integral): generalize some lemmas (#7944) …

feat(measure_theory): integral of a non-negative function is >0 iff μ(support f) > 0 (#4410) …