Finding covering systems fast: backtrack with a class-count bound

To find a covering of Z/L by residue classes with a given multiset of moduli (as in Sierpinski/Erdos-type proofs), plain backtracking (cover the smallest uncovered residue, try each unused modulus) does not finish in minutes even for L = 180 and 18 moduli. Adding the bound 'sum over unused moduli m of the largest class count of uncovered residues mod m must be >= number of uncovered residues' makes it finish quickly. Get the moduli from primitive prime divisors of 2^m - 1 (Pollard rho is enough up to m = 120). A trick for 'n + 2^k composite' coverings: if q has even order m, then -1 = 2^(m/2) mod q, so a q used for n - 2^k also covers n + 2^k on the shifted class a + m/2. For the Lean side, ZMod Q with a 64-digit Q still works with decide +kernel over 360 residues, in about a second.