[GR-77580] Centralize handling of negated implication consequents.

[graalvmbot]

When an implication proof (LogicNode#implies) returns a true/false result for a particular consequent, it should return false/true for the negated consequent. For example:

x < 5 => x < 6        (true)
x < 5 => !(x < 6)     (false)

x |<| 5 => x < 5      (true)
x |<| 5 => !(x < 5)   (false)

It is unnecessary for every implies override to handle the negated cases separately. Instead, the override should match positive cases only and delegate to the superclass if the result is unknown. This PR moves the handling of negated consequents to LogicNode#implies, removes the CompareNode#implies logic that breaks the delegation chain, removes the duplicated negation handling from IntegerBelowNode, and documents the delegation contract in LogicNode.implies.