by
  have h : 0 ≤ (y - x) ^ 2 := sq_nonneg (y - x)
  nlinarith