Generalized CNF for "At Least k, given n variables"

Formula & questionable eyeball proof to convert "at least k" constraints to CNF for easier use with the resolution algorithm.