diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index bbcab3efa56..4b2cedc8be9 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -1945,6 +1945,7 @@ func (ft *factsTable) flowLimit(v *Value) {
 		ft.newLimit(v, a.sub(b, uint(v.Type.Size())*8))
 		ft.detectMod(v)
 		ft.detectSliceLenRelation(v)
+		ft.detectSubRelations(v)
 	case OpNeg64, OpNeg32, OpNeg16, OpNeg8:
 		a := ft.limits[v.Args[0].ID]
 		bitsize := uint(v.Type.Size()) * 8
@@ -2091,6 +2092,48 @@ func (ft *factsTable) detectSliceLenRelation(v *Value) {
 	}
 }
 
+// v must be Sub{64,32,16,8}.
+func (ft *factsTable) detectSubRelations(v *Value) {
+	// v = x-y
+	x := v.Args[0]
+	y := v.Args[1]
+	if x == y {
+		ft.signedMinMax(v, 0, 0)
+		return
+	}
+	xLim := ft.limits[x.ID]
+	yLim := ft.limits[y.ID]
+
+	// Check if we might wrap around. If so, give up.
+	width := uint(v.Type.Size()) * 8
+	if _, ok := safeSub(xLim.min, yLim.max, width); !ok {
+		return // x-y might underflow
+	}
+	if _, ok := safeSub(xLim.max, yLim.min, width); !ok {
+		return // x-y might overflow
+	}
+
+	// Subtracting a positive number only makes
+	// things smaller.
+	if yLim.min >= 0 {
+		ft.update(v.Block, v, x, signed, lt|eq)
+		// TODO: is this worth it?
+		//if yLim.min > 0 {
+		//	ft.update(v.Block, v, x, signed, lt)
+		//}
+	}
+
+	// Subtracting a number from a bigger one
+	// can't go below 0.
+	if ft.orderS.OrderedOrEqual(y, x) {
+		ft.setNonNegative(v)
+		// TODO: is this worth it?
+		//if ft.orderS.Ordered(y, x) {
+		//	ft.signedMin(v, 1)
+		//}
+	}
+}
+
 // x%d has been rewritten to x - (x/d)*d.
 func (ft *factsTable) detectMod(v *Value) {
 	var opDiv, opDivU, opMul, opConst Op
diff --git a/test/prove.go b/test/prove.go
index 365e8ba006e..3f8990615e2 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -679,12 +679,12 @@ func natcmp(x, y []uint) (r int) {
 }
 
 func suffix(s, suffix string) bool {
-	// todo, we're still not able to drop the bound check here in the general case
-	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
+	// Note: issue 76304
+	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix // ERROR "Proved IsSliceInBounds"
 }
 
 func constsuffix(s string) bool {
-	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
+	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed$" "Proved Eq64$"
 }
 
 func atexit(foobar []func()) {
@@ -2639,6 +2639,18 @@ func unsignedRightShiftBounds(v uint, s int) {
 	}
 }
 
+func subLengths1(b []byte, i int) {
+	if i >= 0 && i <= len(b) {
+		_ = b[len(b)-i:] // ERROR "Proved IsSliceInBounds"
+	}
+}
+
+func subLengths2(b []byte, i int) {
+	if i >= 0 && i <= len(b) {
+		_ = b[:len(b)-i] // ERROR "Proved IsSliceInBounds"
+	}
+}
+
 //go:noinline
 func prove(x int) {
 }