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