RMK theorem for `NNReal`

Stream: mathlib4

[Yoh Tanimoto]

I am trying to get the Riesz-Markov-Kakutani theorem in mathlib : ∫⁻ (x : X), f x ∂(μ Λ) = Λ f, where Λ is a positive linear functional on compactly supported continuous functions on some space X.
The proof I know from Rudin's book shows first the inequality Λ f ≤ ∫⁻ (x : X), (f x) ∂μ Λ, then uses linearity and apply it to -f, getting the equality.

In the current formulation rieszContentAux Λ is NNReal-linear, but there is no Neg there. What should I do? It is possible to write the proof of the reversed inequality, but that will be very long (cf. the Real version https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/RMK/linearRMK.lean, ~600 lines for one direction)

[Yoh Tanimoto]

probably I should define toReal toNNReal for positive linear functionals?
cf. #maths > Riesz representation theorem
@Sébastien Gouëzel @Kalle Kytölä @Yaël Dillies