cmd/compile: teach prove about subtract idioms

cmd/compile: teach prove about subtract idioms

For v = x-y:
    if y >= 0 then v <= x
    if y <= x then v >= 0

(With appropriate guards against overflow/underflow.)

Fixes #76304

Change-Id: I8f8f1254156c347fa97802bd057a8379676720ae
Reviewed-on: https://go-review.googlesource.com/c/go/+/720740
Reviewed-by: Mark Freeman <markfreeman@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Jorropo <jorropo.pgm@gmail.com>
Reviewed-by: Keith Randall <khr@google.com>