feat(measure_theory/integral/interval_integral): add an alternative definition (#10380)
feat(measure_theory/integral/interval_integral): add an alternative definition (#10380)

Prove that `∫ x in a..b, f x ∂μ = sgn a b • ∫ x in Ι a b, f x ∂μ`,
where `sgn a b = if a ≤ b then 1 else -1`.





leanprover-community/mathlib,leanprover-community/mathlib