## Stream: new members

### Topic: Proving r^2 >= 0

#### Mii Nguyen (Feb 26 2019 at 03:42):

I'm trying to prove the statement that

lemma r_sq_pos (r : ℝ) (H: 0 ≤ r): 0 ≤ r^2 :=
begin
exact pow_nonneg H _
end


pow_nonneg seems to be what I need but tactic don't accept.
Could someone possibly help me? Thanks a lot.

#### Johan Commelin (Feb 26 2019 at 04:35):

@Mii Nguyen What is the exact error that you get? [Edit: sorry, I was talking nonsense before.]

#### Mii Nguyen (Feb 26 2019 at 04:51):

tactic message is
r : ℝ
H : 0 ≤ r
⊢ 0 ≤ r ^ 2

#### Johan Commelin (Feb 26 2019 at 04:52):

@Mii Nguyen Is there an error message? Do you get red underlined squiggles somewhere? Or are you confused that the tactic state is not saying "no goals"?

#### Johan Commelin (Feb 26 2019 at 04:53):

If that is the confusion, try adding a comma , to the end of your tactic line.

#### Mii Nguyen (Feb 26 2019 at 04:58):

Yes, this is my confusion. It is resolved with ,. Thank you.

Last updated: May 16 2021 at 05:21 UTC