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...
z > 1000and try proving a contradiction (because
z <= 1000is decidable — use
destruct (z <=? 1000)or such in Coq).
x + y > 1001and
xy < 1000— say that
exists epsilon, x + y = 1001 + epsilon
xyis smallest when
xyare farthest away from each other, e.g.
y = 1and
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
Last updated: Jan 29 2023 at 01:02 UTC