import data.real
open real

example (x y : ℝ) : x - y = x + - y :=
by inst_simp