by
  nlinarith [sq_nonneg (x - y)]
initialize IO.println "INITIALIZER_MUST_NOT_RUN"