# Zulip Chat Archive

## Stream: new members

### Topic: proving pi >= 0

#### Mii Nguyen (Feb 27 2019 at 09:57):

I'm trying to prove 0 ≤ r^2 * pi. Here is my work

lemma pi_r_sq_pos (r : ℝ) (H: 0 ≤ r): 0 ≤ r^2 * pi := have r^2 ≥ 0, from pow_nonneg H 2, have pi > 0, from pi_pos, begin apply mul_nonneg, end

I have to prove that `pi ≥ 0`

instead of `pi > 0`

, but I still stuck in it.

Would someone help me with this? Thank you.

#### Patrick Massot (Feb 27 2019 at 09:59):

`apply mul_nonneg ; linarith`

#### Mii Nguyen (Feb 27 2019 at 10:00):

what is the role of `linarith`

in this case? @Patrick Massot

#### Patrick Massot (Feb 27 2019 at 10:01):

The role of `linarith`

is to blast away stupid equality and inequality problems

#### Patrick Massot (Feb 27 2019 at 10:01):

But you can also be explicit of course:

lemma pi_r_sq_pos (r : ℝ) (H: 0 ≤ r): 0 ≤ r^2 * pi := have r^2 ≥ 0, from pow_nonneg H 2, have pi > 0, from pi_pos, mul_nonneg ‹r^2 ≥ 0› (le_of_lt ‹0 < pi›)

#### Patrick Massot (Feb 27 2019 at 10:02):

But in this case, the mathlib style is to be concise (because the result is trivial and wouldn't be even stated on paper):

lemma pi_r_sq_pos (r : ℝ) (H: 0 ≤ r): 0 ≤ r^2 * pi := mul_nonneg (pow_nonneg H 2) (le_of_lt pi_pos)

#### Mii Nguyen (Feb 27 2019 at 10:17):

Would you explain the different of `‹ ›`

and `( )`

? The first is for , say, exact argument and the second is for function? @Patrick Massot

#### Mii Nguyen (Feb 27 2019 at 10:18):

I can find the informations of it in which chapter of the book?

#### Patrick Massot (Feb 27 2019 at 10:18):

https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#additional-syntax

#### Mii Nguyen (Feb 27 2019 at 10:19):

Thank you @Patrick Massot

#### Patrick Massot (Feb 27 2019 at 10:19):

#### Kevin Buzzard (Feb 27 2019 at 14:11):

`le_of_lt`

is a proof that if `a < b`

then `a <= b`

; this is the answer to your original question, and it's in Patrick's code.

#### Kevin Buzzard (Feb 27 2019 at 14:12):

You can guess it because you want to prove `_ <= _`

which is called `le`

, and it's the conclusion, so `le_of`

, and then you write `le_of`

and hit things like ctrl-space until VS Code tells you the things it knows which have "le_of" in, and then you find it.

Last updated: May 10 2021 at 00:31 UTC