no goals
α : Type ?u.832980
β : Type ?u.832983
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
⊢ p = ⊤ ∨ 0 < ENNReal.toReal p ∧ 1 ≤ ENNReal.toReal p
simpa using ENNReal.trichotomy₂ (Fact.out : 1 ≤ p)