by
  nlinarith [sq_nonneg (x - y)]
lemma review_extra : True := ⟨⟩