theorem Real.negMulLog_strictMonoOn : StrictMonoOn negMulLog (Set.Icc 0 (exp (-1)))

theorem Real.negMulLog_strictAntiOn : StrictAntiOn negMulLog (Set.Ici (exp (-1)))

theorem Real.negMulLog_le_rexp_neg_one {x : ℝ} (hx : 0 ≤ x) : x.negMulLog ≤ exp (-1)