Theorem: ENNReal.one_le_conjExponent (ForML/LpHoelder.lean)

State before:
p q : ℝ≥0∞
⊢ 1 ≤ conjExponent p
Tactic:
simp [conjExponent]
State after:
no goals