## 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?

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

Thank you @Patrick Massot

#### 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