Lemma `measure_addE` requires extra parameter

[hoheinzollern]

analysis/theories/measure.v

Line 1829 in c8adb03

Lemma measure_addE A : measure_add A = m1 A + m2 A.

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!