Lemma `measure_addE` requires extra parameter

[hoheinzollern]

https://github.com/math-comp/analysis/blob/c8adb03b2de691e9ed7def8bbd1028720ef918e4/theories/measure.v#L1829

The version using \+ would be more useful, e.g.:

Lemma measure_addE : measure_add = m1 \+ m2.
Proof. by apply: funext=>A; rewrite /measure_add/= /msum 2!big_ord_recl/= big_ord0 adde0. Qed.

But it breaks lemmas in kernel.v

[affeldt-aist]

NB: was discussed during this meeting https://github.com/math-comp/analysis/wiki/2024-10-10-Meeting

[hoheinzollern]

I looked at all instances, and, at least with the current code, the original version of measure_addE works more seamlessly than the proposed alternative.

[affeldt-aist]

Thanks for answering the question!