Initial segments exist

[b-mehta]

There's no statement right now saying

example (k r : ℕ) : 
  ∃ (𝒞 : finset (finset ℕ)), is_init_seg_of_colex 𝒞 r ∧ 𝒞.card = k := sorry

It would be nice to show we have initial segments of colex of any length (in particular in conjunction with #1).
Alternatively, this could have 𝒞 : finset (finset (fin n)):

example {k r n : ℕ} (h : k ≤ choose n r) : 
  ∃ (𝒞 : finset (finset (fin n))), is_init_seg_of_colex 𝒞 r ∧ 𝒞.card = k := sorry

(Could also be a definition instead of a proof of ∃, this would let us evaluate the smallest shadow size in an explicit way compared to #2).

[b-mehta]

Another piece of motivation: we have uniqueness of initial segments but no existence!