theorem work_unit_bound (x y : ℝ) : 0 ≤ x ^ 2 := by
  exact sq_nonneg x