Atleast K out of N encoding in SAT solvers

I know that given an at most k out of N tool I can get an at least K out of N by changing it to at most (n-k) out of N.

But I can't seem to wrap my head around how this is true. I might be missing something very trivial

For example, if K=2 and N=6 how is at least 2 out of 6 equivalent to at most 4 out of 6

any help would be appreciated

As you put it, the equivalence just isn't true. So, don't feel bad about not understanding it. To see, let's take an example. Let's say we have booleans only, N=6 and K=2, and the assignment:

True False False False False False

to these 6 variables. The statement At most 2 out of 6 are True is obviously satisfied by this assignment, but At least 4 out of 6 are True is not.

Maybe what you meant is:

at least K out of N is True

is equivalent to

at most N-K out of N is False

which can be further generalized to say:

at least K out of N objects have property P

is equivalent to:

at most N-K out of N objects do not have the property P

Is this what you were trying to express? Hope that's more clear!