Email Gateway (Aug 22 2022 at 17:47): Email Gateway (Aug 22 2022 at 17:47):From: Lawrence Paulson <lp15@cam.ac.uk>
This theory is decidable and you could even try to use the sos method, but when I tried it didn't terminate.
I did manage to get a proof using a combination of auto and sledgehammer. However, that was just lucky.
lemma G1:
fixes a b u v x y :: real
assumes "a ≥ 0" and "b ≥ 0" and "u ≥ 0" and "v ≥ 0" and "x ≥ 0" and "y ≥
0"
and "b * v < a * u" and "b * u * y + a * v * y < a * u * x - b * v * x"
and
"¬ v * y < u * x" and "b * (v * y) - b * (u * x) < a * (v * x) + a *
(u * y)"
shows False
using assms
apply (auto simp: algebra_simps)
by (smt mult_left_mono mult_nonneg_nonneg)
Larry Paulson
Last updated: Oct 31 2025 at 08:28 UTC