Hi there, does anyone have any idea how I might go about proving this goal (and similar types of goals)?

This specific example can be seen to be true if you examine all of the combinations of cases for a > 0, a < 0, b > 0, b < 0. Also plotting the equation on a graphing calculator such as Desmos shows it to be true.

```
Goal forall a b : R, a <> 0 /\ b <> 0 ->
Rsqr a * 1484.9 + Rsqr b * 406.1 >= a * b * 25.8.
Proof.
intros.
destruct H as [HA HB].
Admitted.
```

The usual way is to rewrite your polynomial as a weighted sum of squares. Finding the proper squares by hand can be a bit tedious. So, better use the `nra`

tactic from the standard library. (You need to do `unfold Rsqr`

beforehand.)

the `nra`

tactic seems to be exactly what I was after. It worked a charm. Thanks so much!

Last updated: Jan 29 2023 at 04:05 UTC