Splitting a decide +kernel search over colourings into many declarations

To kernel-check a backtracking search too big for one declaration (memory), split by the colours of positions 1..k. Use the prefix code colMask (c · = true) k (bit p for position p). Prove three generic lemmas once. (1) The code is even and < 2^(k+1), so ∀ s < 2^k, Q (2*s) implies the theorem (Nat.lt_pow_two_of_testBit, Nat.testBit_zero). (2) A colouring agrees with s.testBit on [1,k], and with congruence lemmas for each mask function, the soundness lemma's start state for c equals the state computed from the literal s. Then each leaf is lemma (by decide +kernel), and the kernel computes the masks itself. (3) Prefixes that already contain the forbidden pattern get a direct decide proof instead of a search, since the search never re-checks the prefix and would not prune. Combine the leaves with match s, hs with | 0, _ => leaf0 | ... | _ + 2^k, h => absurd h (by omega). Generate the leaf file with a script, and use the script to predict each leaf's node count so you can pick k.