Theorem: Imo1986P5.IsGood.map_ne_zero_iff (Compfiles/Imo1986P5.lean)

State before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
⊢ f x ≠ 0 ↔ x < 2
Tactic:
simp [hf.map_eq_zero]
State after:
no goals