I ended up with the following goal, which, unfortunately, was not solved by tactics in Psatz or Omega.
Require Import Psatz Omega.
Goal forall n n0 n1 n2 n3 n4 n5 n6,
n5 + n4 = n6 + n3 ->
n1 + n0 = n2 + n ->
n5 * n1 + n6 * n2 + n3 * n0 + n * n4 =
n5 * n2 + n1 * n6 + n3 * n + n0 * n4.
intros.
Fail lia.
Fail omega.
Lenz, like me, I tested the entire combination of values up to 30, and it corresponded in all cases, so I believe that the goal is valid.
Is there any other way to solve this goal (preferably as automatically as possible)?
In addition, when omegaand liafail (for real systems of equations)? I was surprised to see that I omegahad not even decided a*b = b*a.
EDIT:
lia Z . ( nat (!)) - ? "" nat... ?
Require Import ZArith.
Open Scope Z.
Lemma help:
forall n n0 n1 n2 n3 n4 n5 n6,
n >= 0 -> n0 >= 0 -> n1 >= 0 ->
n2 >= 0 -> n3 >= 0 -> n4 >= 0 ->
n5 >= 0 -> n6 >= 0 ->
n5 + n4 = n6 + n3 ->
n1 + n0 = n2 + n ->
n5 * n1 + n6 * n2 + n3 * n0 + n * n4 =
n5 * n2 + n1 * n6 + n3 * n + n0 * n4.
intros.
Fail lia.
assert (n5 = n6 + n3 - n4) by lia; subst n5.
assert (n1 = n2 + n - n0) by lia; subst n1.
Fail omega.
lia.
Qed.
Close Scope Z.