fixes #1178 (ge0_integralZr)

[affeldt-aist]

Motivation for this change

fixes #1178

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[t6s]

The changes look good and ready to be merged.

Two questions that are irrelevant to my approval of this PR:

• Are there any places ge0_integralZr can be used to simplify proofs? Maybe in hoelder.v
• Why is this section called "semilinearity"? It looks different from the definition of semilinearity found in other places like https://ncatlab.org/nlab/show/semilinear+map

[affeldt-aist]

Why is this section called "semilinearity"? It looks different from the definition of semilinearity found in other places like https://ncatlab.org/nlab/show/semilinear+map

The textbook I was using calls semilinearity of the integral the combination of the properties of ge0_integralZl_EFin and ge0_integralD (however when considered over the set of simple functions), hence the name of the section. The definition you are pointing at is indeed more general.

[affeldt-aist]

Are there any places ge0_integralZr can be used to simplify proofs? Maybe in hoelder.v

Thanks for insisting on this point.
In the last commit, I used ge0_integralZr instead of ge0_integralZl where it looked like superfluous commutativity lemmas were used, leading to a bit shorter proofs. I have also another example in a forthcoming PR.