mathlib

24cefb50 - feat(data/real/ennreal): add monotonicity lemmas for ennreal.to_nnreal (#10556)

feat(data/real/ennreal): add monotonicity lemmas for ennreal.to_nnreal (#10556) Add four lemmas about monotonicity of `to_nnreal` on extended nonnegative reals, `to_nnreal_mono`, `to_nnreal_le_to_nnreal`, `to_nnreal_strict_mono`, `to_nnreal_lt_to_nnreal` (analogous to `to_real_mono`, `to_real_le_to_nnreal`, `to_real_strict_mono`, `to_real_lt_to_real`).