rw [NNReal.le_div_iff hx', ← NNReal.le_div_iff' hfx, tsub_le_iff_right, ← hf.map_eq_zero,
 hf.map_add, div_mul_cancel₀ _ hfx, hf.map_two, zero_mul]
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x ≤ 2 / (2 - x)
no goals