Theorem: ZetaSum_aux1_3b (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
x : ℝ
⊢ ↑⌊x⌋ + 1 / 2 - x ≤ 1 / 2
Tactic:
ring_nf
State after:
x : ℝ
⊢ 1 / 2 + (↑⌊x⌋ - x) ≤ 1 / 2

State before:
x : ℝ
⊢ 1 / 2 + (↑⌊x⌋ - x) ≤ 1 / 2
Tactic:
exact add_le_of_nonpos_right <| sub_nonpos.mpr (Int.floor_le x)
State after:
no goals