sorry
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
hcp : ∀ (i : Fin n), 0 < c i
hc : ∑ i : Fin n, c i = k
S : Type := (i : Fin n) → { s // Even s.card }
cs : S
i : Fin k
y : Fin (2 * n) := ↑f ⟨↑i, ⋯⟩
y' : Fin n := ⟨↑y, ⋯⟩
ys : { s // Even s.card } := cs y'
⊢ ↑y + n < 2 * n
no goals