Theorem: near_one_avoids_zero (Ray/Misc/Bounds.lean)

State before:
z : ℂ
⊢ Complex.abs (z - 1) < 1 → z ≠ 0
Tactic:
intro h
State after:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ z ≠ 0

State before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ z ≠ 0
Tactic:
exact Complex.slitPlane_ne_zero (mem_slitPlane_of_near_one h)
State after:
no goals