Simplify loop invariant in ntt_2_layers()

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

mlkem/src/poly.c

@@ -363,7 +363,8 @@ __contract__(
     invariant(start < MLKEM_N + 2 * len)
     invariant(len % 2 == 0)
     invariant(len == 4 || len == 8 || len == 16 || len == 32 || len == 64 || len == 128)
-    invariant(k <= MLKEM_N / 2 && 2 * len * k == start + MLKEM_N)
+    invariant(k <= MLKEM_N / 2)
+    invariant(2 * len * k == start + MLKEM_N)
     invariant(array_abs_bound(r, 0, start, (layer + 2) * MLKEM_Q))
     invariant(array_abs_bound(r, start, MLKEM_N, layer * MLKEM_Q))
   )