This is the most basic patch to handle fixing issue #57666.
D133919 proposes to handle much more than this in a single patch, but I've used 10 regression tests just to make sure this part is doing what I expected and nothing more, and it already shows even more potential TODO items.
The more general proofs from D133919 are correct, but we should enable this in smaller steps to reduce risk:
https://alive2.llvm.org/ce/z/RrVEyX
You could also match other predicates i.e ((x?1:4)&(y?1:4))<2
Also it seems we already have some logic for match some other predicates in this case (although I can't find it):
https://godbolt.org/z/hjzMGKqKz
although it seems to have an off by-1 issue (see ugt and ugt3)