by
  nlinarith [sq_nonneg (x - y)]