beginner trouble with "by extra"

Stream: new members

[rzeta0]

I'm having trouble with using by extra as follows:

example {n : ℤ} (hn : n ≥ 10) : n ^ 4 - 2 * n ^ 2 > 3 * n ^ 3 :=
  calc
    n ^ 4 - 2 * n ^ 2 ≥ n^4 := by extra
    _ = n*n^3 := by ring
    _ ≥ (10) * n^3 := by rel [hn]
    _ > 3 * n^3 := by numbers

I want to express the mathematical truth that

$$n^4 - 2n^2 \geq n^4$$

since $n^2$ is aways positive.

(the final by numbers also fails, but that is a separate problem)

[llllvvuu]

Isn't that backwards? $n^4 - 2n^2 \le n^4$

[Heather Macbeth]

These two tactics are specific to the "Mechanics of Proof" textbook (see outline here), so they require a bit of translation to get help with on Zulip.

extra slightly extends the mainstream tactic positivity. You could use it to prove

(n ^ 4 - 2 * n ^ 2) + 2 * n ^ 2 ≥ n ^ 4 - 2 * n ^ 2

but not to prove

n ^ 4 ≥ n ^ 4 - 2 * n ^ 2

That is, it only handles "added extra quantities", not "subtracted extra quantities".

numbers slightly weakens the mainstream tactic norm_num. It proves only purely numeric facts, not facts involving variables, so it will not be able to prove

10 * n ^ 3 > 3 * n ^ 3