feat(data/real/ennreal): trichotomy lemmas (#11014)
If there is a case split one performs frequently, it can be useful to provide the case split and the standard data-wrangling one performs after the case split together. I do this here for the `ennreal` case-split lemma
```lean
protected lemma trichotomy (p : ℝ≥0∞) : p = 0 ∨ p = ∞ ∨ 0 < p.to_real :=
```
and a couple of variants.
