Theorem: ZetaSum_aux1_3a (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
x : ℝ
⊢ -(1 / 2) < ↑⌊x⌋ + 1 / 2 - x
Tactic:
norm_num [← add_assoc]
State after:
x : ℝ
⊢ x < 1 / 2 + ↑⌊x⌋ + 1 / 2

State before:
x : ℝ
⊢ x < 1 / 2 + ↑⌊x⌋ + 1 / 2
Tactic:
linarith [sub_pos_of_lt (Int.lt_floor_add_one x)]
State after:
no goals