rw [NNReal.div_le_iff' hx', ← hf.map_eq_zero]
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ 2 / (2 - x) ≤ f x
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) = 0