Products of consecutive integers are nonnegative

Over ℤ the product t * (t - 1) of two consecutive integers is nonnegative, because no integer lies strictly between t - 1 and t. This is a genuinely integral statement: over ℝ it already fails at t = 1 / 2, and over ℕ it is vacuous.

The unit-shifted form 0 ≤ s * (s - δ) for δ : ℤˣ follows by rescaling, since the only units of ℤ are ±1 and multiplying by one of them permutes the pair.

Main results

• Int.zero_le_mul_sub_one : 0 ≤ t * (t - 1).
• Int.zero_le_mul_sub_units : 0 ≤ s * (s - δ) for a unit δ.

theorem Int.zero_le_mul_sub_one (t : ℤ) : 0 ≤ t * (t - 1)

Two consecutive integers have nonnegative product: no integer lies strictly between t - 1 and t.

theorem Int.zero_le_mul_sub_units (δ : ℤˣ) (s : ℤ) : 0 ≤ s * (s - ↑δ)

The exceptional term of a unit exceptional value is nonnegative: rescaling by the unit turns s * (s - δ) into a product of consecutive integers. Nonnegativity fails for the other odd exceptional values, where already 1 * (1 - ε) < 0 for ε ≥ 3.