squaring a variable in an inequality

Stream: new members

[rzeta0]

I have the following goal state:

x : ℝ
ha : x ≤ -3

I'd like to derive hb: x^2 ≥ 9 but am not succeeding.

I have tried the following but it doesn't work.

have g1 : x^2 ≥ 9 := by rel [ha]

Is the problem that the tactics like rel and linarith only work with linear operations and not non-linear "squared" operations?

[Julian Berman]

rzeta0 said:

Is the problem that the tactics like rel and linarith only work with linear operations and not non-linear "squared" operations?

Precisely, yep. There's a somewhat "trivial" but effective version of the tactic called nlinarith which will help in some non-linear arithmetic cases (luckily like here):

import Mathlib
example {x : ℝ} (h : x ≤ -3) : x^2 ≥ 9 := by nlinarith

[rzeta0]

thanks very helpful