Extend linear arithmetic rules to deal with equalities

There is a user of Alethe who would like to justify steps that conclude something like this:

(cl (= 0 (+ x 1))
    (not (= 0 (+ y x (- 1))))
    (not (= 0 (+ y (- 2)))))

While I believe this can be done in a more verbose way using several steps, it would be really helpful if there was a way to derive this directly.

Currently, we have a modified version of Carcara (in the branch la-generic-extension) that accepts clauses like this as part of the la_generic rule. This was done by generalizing the operator addition logic of the rule to also deal with equalities, so the whole step would look like this:

(step t1 (cl
    (= 0 (+ x 1))
    (not (= 0 (+ y x (- 1))))
    (not (= 0 (+ y (- 2))))
) :rule la_generic :args ((- 1) 1 (- 1)))

The core of this extension is in this function.

Alternatively, one could see that clause as an implication of equalities, so that step is really proving that ((0 = y + x - 1) \land (0 = y - 2)) \rightarrow (0 = x + 1)

So it might make sense to add support for this as a separate rule, that deals with implication between linear equalities, rather than an extension of la_generic:

(step t1 (cl
    (not (= 0 (+ y x (- 1))))
    (not (= 0 (+ y (- 2))))
    (= 0 (+ x 1))
) :rule <new_rule?> :args (1 (- 1)))

where the procedure to check this would be to negate the n - 1 disequalities, multiply them by the coefficients in the arguments, add them, and check that you arrive at the final equality.