diff --git a/boot0.s b/boot0.s
index dc01ff5..96284e3 100644
--- a/boot0.s
+++ b/boot0.s
@@ -127,25 +127,8 @@ STAGE2_GPT_ENTRY_ADDR  equ 0x1a
   and eax, 127 ; Test size is a multiple of 128
   jnz .panic
   ; Use the (n & (n - 1)) == 0 trick to test if the entry size is a power of 2. Since we already
-  ; know it's a nonzero multiple of 128, if size is a power of 2 then size = 128 * 2^n holds
-  ; (proof below because it felt correct to me but it didn't feel obvious enough to use without
-  ; proving). Therefore we don't need to bother dividing by 128 first (shr 7), which saves a couple
-  ; of bytes.
-  ; - Let s = 128 * a, s = 2^b for integers a >= 1, b >= 0
-  ; - Lemma: b >= 7
-  ;   - Assume b < 7
-  ;   - s = 2^b
-  ;   - s < 2^7
-  ;   - s < 128
-  ;   - s = 128 * a, a >= 1
-  ;   - s/128 >= 1
-  ;   - s >= 128
-  ;   - Contradiction: s < 128 and s >= 128 cannot both hold
-  ; - 2^7 * a = 2^b
-  ; - a = 2^(b-7)
-  ; - s = 128 * 2^(b-7)
-  ; - Therefore s = 128 * 2^n where n = b - 7.
-  ; - n >= 0 because b >= 7.
+  ; know it's a nonzero multiple of 128, if size is a power of 2 then size = 128 * 2^n holds.
+  ; Therefore we don't need to bother dividing by 128 first (shr 7), which saves a couple of bytes.
   mov eax, ebx
   mov ecx, ebx
   dec ecx