diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go
index 2f0a44735..bb713a41d 100644
--- a/pkg/slayers/scion.go
+++ b/pkg/slayers/scion.go
@@ -1078,9 +1078,11 @@ func (s *SCION) upperLayerChecksum(upperLayer []byte, csum uint32) uint32 {
 
 // (VerifiedSCION) The following function terminates but Gobra can't
 // deduce that because of limited support of bitwise operations.
-// @ decreases _
+// @ decreases
 func (s *SCION) foldChecksum(csum uint32) (res uint16) {
+	// @ decreases csum
 	for csum > 0xffff {
+		// @ b.FoldChecksumLemma(csum)
 		csum = (csum >> 16) + (csum & 0xffff)
 	}
 	return ^uint16(csum)
diff --git a/verification/utils/bitwise/bitwise-eqs.gobra b/verification/utils/bitwise/bitwise-eqs.gobra
index 2b8b5b18b..205841a92 100644
--- a/verification/utils/bitwise/bitwise-eqs.gobra
+++ b/verification/utils/bitwise/bitwise-eqs.gobra
@@ -68,3 +68,9 @@ ensures 3 & 1 == 1
 ensures 3 & 2 == 2
 decreases
 pure func InfoFieldFirstByteSerializationLemmas() bool
+
+ensures csum > 0xffff ==>
+	let newCsum := (csum >> 16) + (csum & 0xffff) in
+	newCsum < csum
+decreases
+pure func FoldChecksumLemma(csum uint32) struct{}
\ No newline at end of file
diff --git a/verification/utils/bitwise/proofs.dfy b/verification/utils/bitwise/proofs.dfy
index 9d38da8ce..dc0286d4f 100644
--- a/verification/utils/bitwise/proofs.dfy
+++ b/verification/utils/bitwise/proofs.dfy
@@ -162,4 +162,10 @@ lemma FUint32AfterFPutUint32(v: bv32)
 lemma FPutUint32AfterFUint32(b0: bv8, b1: bv8, b2: bv8, b3: bv8)
 	ensures var v := FUint32Spec(b0, b1, b2, b3);
 		FPutUint32Spec(v) == (b0, b1, b2, b3)
+{}
+
+lemma FoldChecksumLemma(csum: bv32)
+	ensures csum > 0xffff ==>
+		var newCsum := (csum >> 16) + (csum & 0xffff);
+		newCsum < csum
 {}
\ No newline at end of file