## Stream: new members

### Topic: Lean Tutorial

#### James Arthur (May 22 2020 at 17:22):

I am slightly confused on the Lean tutorial. I am at the following

import data.real.basic

example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b :=
begin
sorry
end


and can't seem to get anywhere.

Thanks, James

#### Kevin Buzzard (May 22 2020 at 17:26):

The tactic linarith will solve it, but if you want to find out the name of the function which will do it directly you can try library_search.

#### Patrick Massot (May 22 2020 at 17:56):

Kevin, this is fine when you're cheating in a speed-run against undergrads, but we're trying to teach something here.

#### Patrick Massot (May 22 2020 at 17:57):

James, you should try using le_add_of_nonneg_right

#### Kevin Buzzard (May 22 2020 at 18:02):

It was any%!

Last updated: May 16 2021 at 05:21 UTC