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

State before:
z : ℂ
zs : Complex.abs z ≤ 1 / 2
⊢ 1 / 2 < 1
Tactic:
norm_num
State after:
no goals

State before:
z : ℂ
zs : Complex.abs z ≤ 1 / 2
⊢ 1 / (1 - 1 / 2) * Complex.abs z = 2 * Complex.abs z
Tactic:
norm_num
State after:
no goals