`ge0_integralZr` is lacking

[affeldt-aist]

analysis/theories/lebesgue_integral.v

Line 2288 in 0105ccc

Lemma ge0_integralZl (k : \bar R) : (forall x, D x -> 0 <= f x) ->