Teach instsimplify that X+Y>=X+Z is the same as Y>=Z if neither side overflows,