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.)
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