Proving r^2 >= 0

Stream: new members

[Mii Nguyen]

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]

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

[Mii Nguyen]

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

[Johan Commelin]

@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]

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

[Mii Nguyen]

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