diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index f70ec0c830..973e3cd4f2 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -931,31 +931,41 @@ func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
 		if d == signed && ft.isNonNegative(c.Args[0]) && ft.isNonNegative(c.Args[1]) {
 			d |= unsigned
 		}
-		switch br {
-		case negative:
-			switch b.Control.Op { // Special cases
-			case OpIsInBounds, OpIsSliceInBounds:
-				// 0 <= a0 < a1 (or 0 <= a0 <= a1)
-				//
-				// On the positive branch, we learn a0 < a1,
-				// both signed and unsigned.
-				//
-				// On the negative branch, we learn (0 > a0 ||
-				// a0 >= a1). In the unsigned domain, this is
-				// simply a0 >= a1 (which is the reverse of the
-				// positive branch, so nothing surprising).
-				// But in the signed domain, we can't express the ||
-				// condition, so check if a0 is non-negative instead,
-				// to be able to learn something.
+		switch b.Control.Op {
+		case OpIsInBounds, OpIsSliceInBounds:
+			// 0 <= a0 < a1 (or 0 <= a0 <= a1)
+			//
+			// On the positive branch, we learn:
+			//   signed: 0 <= a0 < a1 (or 0 <= a0 <= a1)
+			//   unsigned:    a0 < a1 (or a0 <= a1)
+			//
+			// On the negative branch, we learn (0 > a0 ||
+			// a0 >= a1). In the unsigned domain, this is
+			// simply a0 >= a1 (which is the reverse of the
+			// positive branch, so nothing surprising).
+			// But in the signed domain, we can't express the ||
+			// condition, so check if a0 is non-negative instead,
+			// to be able to learn something.
+			switch br {
+			case negative:
 				d = unsigned
 				if ft.isNonNegative(c.Args[0]) {
 					d |= signed
 				}
+				addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
+			case positive:
+				addRestrictions(b, ft, signed, ft.zero, c.Args[0], lt|eq)
+				addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
+			}
+		default:
+			switch br {
+			case negative:
+				addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
+			case positive:
+				addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
 			}
-			addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
-		case positive:
-			addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
 		}
+
 	}
 }
 
diff --git a/test/prove.go b/test/prove.go
index 39b23c5e0a..6e92b9eec2 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -726,6 +726,16 @@ func signHint2(b []byte, n int) {
 	}
 }
 
+// indexGT0 tests whether prove learns int index >= 0 from bounds check.
+func indexGT0(b []byte, n int) {
+	_ = b[n]
+	_ = b[25]
+
+	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
+		b[i] = 123 // ERROR "Proved IsInBounds$"
+	}
+}
+
 // Induction variable in unrolled loop.
 func unrollUpExcl(a []int) int {
 	var i, x int