. simp
  intro hp h
  rw [h]
  rw [add_tsub_cancel_iff_le]
  simp
  exact hp
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⁻¹
case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹