feat(data/real/ennreal): Positivity extension for `ennreal.of_real` (#16955)
feat(data/real/ennreal): Positivity extension for `ennreal.of_real` (#16955)

and three easy lemmas





leanprover-community/mathlib,leanprover-community/mathlib