iterating over subsets by switching one element at a time
Here is how to convert a number from $\binom{n}{k}$ to a subset of $\binom{[n]}{k}$, and vice versa. This is known as inductive counting. I'll use your formula
$$ \binom{[n]}{k} = \binom{[n-1]}{k} + \binom{[n-1]}{k-1} \times \{n\}. $$

Given a code $x \in [0,\binom{n}{k})$, the idea is that the first $\binom{n-1}{k}$ codes will be used to code the $\binom{[n-1]}{k}$ part, and the rest will be used to code a subset in $\binom{[n-1]}{k-1}$ which will be completed to the required subset by adding the element $n$. Here is the relevant quasi-python code:

decode(n, k, code):
  if k == 0:
    return []
  elif code &lt; binom(n-1, k):
    return decode(n-1, k, code)
  elif:
    return decode(n-1, k-1, code - binom(n-1, k)) + [n-1]


Encoding is the reverse process, and mirrors it exactly:

  encode(n, k, S):
    if k == 0:
      return 0
    elif n-1 not in S:
      return encode(n-1, k, S)
    else:
      return encode(n-1, k-1, S[:-1]) + binom(n-1, k)


Using these subroutines, you can compute the successor and predecessor of a given subset. You could also do it directly, for example by "unrolling" the resulting code, but this is a programming question which you should be able to solve for yourself in a couple hours.



The preceding doesn't produce a Gray code at all. You can obtain a Gray code by reversing the second half in your fundamental formula (this is the meaning of the overline). The corresponding decoding function is

decode2(n, k, code):
  if k == 0:
    return []
  elif code &lt; binom(n-1, k):
    return decode2(n-1, k, code)
  elif:
    return decode2(n-1, k-1, binom(n, k) - 1 - code) + [n-1]


I'll leave the encoding function as an exercise. The proof that this forms a Gray code is by induction. You prove a more general claim, stating what are the first and last sets in the ordering for any given $n,k$, and given that you prove by induction that the result is a Gray code. Details left to you.