## Stream: maths

### Topic: proof basics

#### Nicholas McConnell (Feb 13 2020 at 18:06):

In proving the sum of two odd natural numbers is even, I got to this goal:

2 * k + 1 + (2 * l + 1) = 2 * k + 2 * l + 2 * 1


but am unsure how to go further. "ring" didn't work, and "simp" only got me to 1 + (1 + (2 * k + 2 * l)) = 2 + (2 * k + 2 * l), on which I can't seem to apply add_assoc. I also tried saying "import tactic" at the beginning and that didn't work.

#### Rob Lewis (Feb 13 2020 at 18:08):

ring will solve this. Do you have mathlib installed? If so, I think there's something wrong with your configuration, because import tactic should work.

#### Nicholas McConnell (Feb 13 2020 at 18:12):

I don't think I have mathlib; what's the best way to get it?

#### Rob Lewis (Feb 13 2020 at 18:13):

https://github.com/leanprover-community/mathlib#installation

#### Nicholas McConnell (Feb 13 2020 at 19:33):

Alright, thank you

Last updated: May 09 2021 at 11:09 UTC