constructor
case inl.intro.some.some
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p.IsConjExponent q
case inl.intro.some.some.one_lt
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ 1 < p

case inl.intro.some.some.inv_add_inv_conj
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p⁻¹ + q⁻¹ = 1