Zulip Chat Archive

Stream: new members

Topic: Proving r^2 >= 0


view this post on Zulip 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.

view this post on Zulip 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.]

view this post on Zulip Mii Nguyen (Feb 26 2019 at 04:51):

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

view this post on Zulip 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"?

view this post on Zulip Johan Commelin (Feb 26 2019 at 04:53):

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

view this post on Zulip 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