Intersection of `s₁ ≤` and `≠ t₂`

The intersection of a lower bound and a non-equivalence cannot be simplified.

(s₁ ≤) ∧ (≠ t₂) = (s₁ ≤) ∧ (≁ t₂)

(If there is also an upper bound, then the _range_ might be simplifiable!)