refine Iff.intro ?_ ?_
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ ↔ p⁻¹ + q⁻¹ = 1
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1

case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹