refine (mul_eq_zero.1 ?_).resolve_right hfx
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
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) * f x = 0