represent uniqueness

Stream: new members

[Esteban Estupinan]

Hi all. Please your help. The following proposition needs to be entered in lean order to prove it. Specifically, there is a confusion in representing "one and only one". thanks for your help.
imagen.png

example (m n : ℤ) : ∃ x, m + x = n ∧ ∀ ???? = x :=

[David Renshaw]

example (m n : ℤ) : ∃! x, m + x = n := sorry

[David Renshaw]

docs#exists_unique

[Eric Wieser]

Or m + x = n ↔ x = n - m which not only says there is a unique solution, but says what it is!