theorem ENNReal.HolderConjugate.toReal_of_ne_top {p q : ENNReal} (h : p.HolderConjugate q) (hp : p ≠ ⊤) (hq : q ≠ ⊤) : p.toReal.HolderConjugate q.toReal