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