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

State before:
x : ℝ
xr : |x| ≤ 1 / 2
⊢ 1 / 2 < 1
Tactic:
norm_num
State after:
no goals

State before:
x : ℝ
xr : |x| ≤ 1 / 2
⊢ 1 / (1 - 1 / 2) * |x| = 2 * |x|
Tactic:
norm_num
State after:
no goals