I need help proving this lemma:

```
Require Import ZArith.
Require Import Lia.
Require Import PArith.BinPos.
Open Scope Z.
Lemma helper : forall (z x y : Z) (h1 : x * y * z <= 1000000) (h2 : z <= x + y - 1) (h3 : 1 <= x <= 1000000) (h4 : 1 <= y <= 1000000) (h5 : 1 <= z <= 1000000),
z <= 1000.
```

I'm sure it's correct. Here's what Wolfram Alpha has to say about it: Screenshot-from-2022-11-26-15-28-59.png

Thanks in advance, and I will return the favor some day...

informal sketch:

- we can assume
`z > 1000`

and try proving a contradiction (because`z <= 1000`

is decidable — use`destruct (z <=? 1000)`

or such in Coq). - by algebra, we can conclude
`x + y > 1001`

and`xy < 1000`

— say that`exists epsilon, x + y = 1001 + epsilon`

- Using the theory associated with https://en.wikipedia.org/wiki/Inequality_of_arithmetic_and_geometric_means and/or calculus (not sure how to formalize that), we know that
`xy`

is smallest when`xy`

are farthest away from each other, e.g.`y = 1`

and`x = 1000 + epsilon`

(or symmetrically`x = 1`

). But then`xy = 1000 + epsilon`

; since we knew`xy < 1000`

, we get the desired contradiction.

but I've never done reals in Coq, and depending on what's available, one might search for a different sketch or automated solvers or...

simpler approach: install https://github.com/coin-or/Csdp and try `psatz`

?

Last updated: Jun 18 2024 at 22:01 UTC