Consider negation's proof before triggering arith pfs. (#4776)

Consider negation's proof before triggering arith pfs. (#4776)

The current arith proof machinery can prove conflicts which are
explained by assumptions and tightened assumptions.

Previously we verified that the conflict constraint was explained in
terms of assumptions and tightened assumptions, before trying to
save/produce a proof.

We did not verify that the negated constraint was an assumption or
tightened assumption.

This caused us to attempt to prove conflicts around constraints whose
negations where proven by general means (in the case of #4714, by the
equality engine), which the proof machinery was not prepared to handle.

This PR also checks that the negate constraint is an assumption or
tightened assumption, before saving the proof.

Thanks, Gereon, for doing the initial investigation into this!

fixes 4714

Co-authored-by: Gereon Kremer <nafur42@gmail.com>