theorem sum_mod_range {K : ℕ} (hK : 0 < K) (a : Fin K) : (∑ s ∈ Finset.range K, if ⟨s % K, ⋯⟩ = a then 1 else 0) = 1

theorem sum_mod_range_mul {K : ℕ} (hK : 0 < K) (m : ℕ) (a : Fin K) : (∑ s ∈ Finset.range (K * m), if ⟨s % K, ⋯⟩ = a then 1 else 0) = m