prove basic things.

Stream: maths

[kali]

Hello,

I am trying to learn lean and prove basic things.

I want to do the following axiom but I don't understand how to do it.
For any real a and b, a + b is a real.
axiom t: ∀ (a b : ℝ), a + b ∈ ℝ -- error

The following axiom:
Every real a admits a unique opposite -a such that -a + a = a + (-a) = 0.

The following theorem:
For any real a, -(-a) = a
I want to prove it by using the above axiom, substituting a by -a in the equation -a + a = 0 and that the opposite is unique.

Thanks for your help.

[Adam Topaz]

Hello. This zulip is indeed the best place to get help with such questions, but the best place to start is in the #new members stream.

[kali]

Sorry, I reposted in the right section