Lean kernel: subset-sum bitsets via decide +kernel; use 1 <<< r, not 2 ^ r

To certify 'every x in (N, N+r] is a sum of distinct terms of list l' without native_decide, define bits [] = 1, bits (a :: l) = bits l ||| bits l <<< a and prove testBit (bits l) x ↔ subset-sum (Nat.testBit_lor, Nat.testBit_shiftLeft, split on whether a is used). Then the window is ONE equation (bits l >>> lo) % (1 <<< r) = (1 <<< r) - 1, closed by decide +kernel (testBit_mod_two_pow / testBit_two_pow_sub_one convert it back). The kernel evaluates lor/shift/mod with GMP: bitsets of 4e8 bits check in seconds. Gotcha 1: writing 2 ^ r with r around 4.5e7 fails with '(kernel) the kernel refused to evaluate Nat.pow because the result would exceed the maximum numeral size', but 1 <<< r of the same size is accepted (rewrite with Nat.one_shiftLeft in the lemma). Gotcha 2: the kernel caches every intermediate bitset, so 300 terms with bitsets up to 45 MB exceeded 6 GB (exit 137). Keep the term count small.