Squares of half-integers in ordered fields

An integer cast into a linearly ordered field and translated by one half has square at least one quarter. This bound applies coordinatewise to vectors whose coordinates are half-integers.

theorem Int.quarter_le_cast_add_half_sq {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (z : ℤ) : 1 / 4 ≤ (↑z + 1 / 2) ^ 2

The square of an integer translated by one half is at least one quarter.